floor((n / d)^(1 / k) S): the largest r with r^k d <= n S^k, by bisection.
The root is below S (n / d + 1), so its bit length is at most the sum of
theirs -- the bound and the fuel; the target n S^k itself can run past
specBitLength's reach (S = 2^96, k = 32 is 3,073 bits)
113def float32ExactRootKLow =
114 (lambda unrestricted k : Nat .
115 (lambda unrestricted n : Nat .
116 (lambda unrestricted d : Nat .
117 (lambda unrestricted scale : Nat .
118 (let unrestricted target = (nat-multiply n (specPower scale k)) in
119 (let unrestricted bits = (nat-add (specBitLength scale) (specBitLength (nat-add (nat-divide n d) 1))) in
120 (app
121 (nat-eliminate
122 (lambda unrestricted current : Nat . (pi unrestricted low : Nat . (pi unrestricted high : Nat . Nat)))
123 (lambda unrestricted low : Nat . (lambda unrestricted high : Nat . low))
124 (lambda unrestricted predecessor : Nat .
125 (lambda unrestricted induction : (pi unrestricted low : Nat . (pi unrestricted high : Nat . Nat)) .
126 (lambda unrestricted low : Nat . (lambda unrestricted high : Nat .
127 (specSelect (nat-less-than (nat-add low 1) high)
128 (specSelect (nat-less-than target (nat-multiply (specPower (nat-divide (nat-add low high) 2) k) d))
129 (induction low (nat-divide (nat-add low high) 2))
130 (induction (nat-divide (nat-add low high) 2) high))
131 low)))))
132 (nat-add bits 2))
133 zero (specPow2 bits))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.