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