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)
89def float32ExactRootKLow =
90 (lambda unrestricted k : Nat .
91 (lambda unrestricted n : Nat .
92 (lambda unrestricted d : Nat .
93 (lambda unrestricted scale : Nat .
94 (let unrestricted target = (nat-multiply n (specPower scale k)) in
95 (let unrestricted bits = (nat-add (specBitLength scale) (specBitLength (nat-add (nat-divide n d) 1))) in
96 (app
97 (nat-eliminate
98 (lambda unrestricted current : Nat . (pi unrestricted low : Nat . (pi unrestricted high : Nat . Nat)))
99 (lambda unrestricted low : Nat . (lambda unrestricted high : Nat . low))
100 (lambda unrestricted predecessor : Nat .
101 (lambda unrestricted induction : (pi unrestricted low : Nat . (pi unrestricted high : Nat . Nat)) .
102 (lambda unrestricted low : Nat . (lambda unrestricted high : Nat .
103 (specSelect (nat-less-than (nat-add low 1) high)
104 (specSelect (nat-less-than target (nat-multiply (specPower (nat-divide (nat-add low high) 2) k) d))
105 (induction low (nat-divide (nat-add low high) 2))
106 (induction (nat-divide (nat-add low high) 2) high))
107 low)))))
108 (nat-add bits 2))
109 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.