Correctness of binary square root

Lean's unpacked floating-point square root computes an integer square root and records whether the discarded real fraction is below or above one half. This module proves that certificate correct, connects the positive finite executable path to Lean's unpacked square-root model, proves that the square root of a finite nonnegative value never overflows, and concludes that the result for a conventional IEEE descriptor is one nearest-even rounding of the exact real square root.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.accuracyRepresents_natSqrt (n : ℕ) : have root := n.sqrt; have remainder := n - root * root; have accuracy := if remainder = 0 then Float.Model.UnpackedFloat.Accuracy.exact else Float.Model.UnpackedFloat.Accuracy.inexact (if remainder ≤ root then Ordering.lt else Ordering.gt); accuracyRepresents root accuracy √↑n

The residual classification produced from an integer square root locates the exact real square root in the unit interval beginning at Nat.sqrt n, with the correct half-way comparison.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_ofModel_sqrt_finite_eq_roundAt (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (mantissa : ℕ) (exponent : ℤ) (hmantissa : mantissa ≠ 0) (hfinite : (ofModel fmt (Float.Model.UnpackedFloat.sqrt fmt.toModel (Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.positive mantissa exponent ⋯))).isFinite = true) : (ofModel fmt (Float.Model.UnpackedFloat.sqrt fmt.toModel (Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.positive mantissa exponent ⋯))).toReal = roundAt fmt √(↑mantissa * Flocq.bpow Numerics.binaryRadix exponent)

Lean's positive finite model square root has the same real value as independent nearest-even rounding of the exact real square root whenever the packed result is finite.

Square root never overflows

The largest finite value of every IEEE descriptor exceeds one, so its square root is below it and the rounded result stays inside the finite range. The proof first shows that packing a model value whose biased exponent is in range yields a finite word, then that roundWithAccuracy of a certified real below 2^maxNormal packs to such a value, and so does one in the top binade below the overflow threshold.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_ofModel_finite_of_noOverflow (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Float.Model.UnpackedFloat.Sign) (mantissa : ℕ) (exponent : ℤ) (hm : mantissa ≠ 0) (hnoOverflow : ¬2 ^ fmt.toModel.exponentBits ≤ (exponent + ↑fmt.toModel.exponentBias + ↑fmt.toModel.mantissaBitsWithoutImplicit).toNat + 1) : (ofModel fmt (Float.Model.UnpackedFloat.finite sign mantissa exponent ⋯)).isFinite = true

Packing a finite model value whose biased exponent stays below the all-ones pattern yields a finite word. This is the converse of noOverflow_of_isFinite_ofModel_finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_ofModel_roundWithAccuracy_of_lt_bpow (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Float.Model.UnpackedFloat.Sign) (mantissa : ℕ) (exponent : ℤ) (accuracy : Float.Model.UnpackedFloat.Accuracy) (value : ℝ) (hmantissa : mantissa ≠ 0) (haccuracy : accuracyRepresents mantissa accuracy value) (hle : exponent ≤ fmt.toModel.targetExponent (Float.Model.totalExponent mantissa exponent)) (hbound : value * Flocq.bpow Numerics.binaryRadix exponent < Flocq.bpow Numerics.binaryRadix (Int.ofNat fmt.ieeeMaxNormalExponent)) : (ofModel fmt (Float.Model.UnpackedFloat.roundWithAccuracy fmt.toModel sign mantissa exponent accuracy)).isFinite = true

Rounding a positive certified real whose magnitude is below 2^maxNormal never overflows, so the packed result is finite. The exponent premise is the documented precondition of roundWithAccuracy: normalization may discard low bits but never shifts left.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_ofModel_roundWithAccuracy_of_lt_overflow (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Float.Model.UnpackedFloat.Sign) (mantissa : ℕ) (exponent : ℤ) (accuracy : Float.Model.UnpackedFloat.Accuracy) (value : ℝ) (hmantissa : mantissa ≠ 0) (haccuracy : accuracyRepresents mantissa accuracy value) (hle : exponent ≤ fmt.toModel.targetExponent (Float.Model.totalExponent mantissa exponent)) (hbound : value * Flocq.bpow Numerics.binaryRadix exponent < Flocq.bpow Numerics.binaryRadix (Int.ofNat fmt.ieeeMaxNormalExponent + 1) - Flocq.bpow Numerics.binaryRadix (Int.ofNat fmt.ieeeMaxNormalExponent - ↑fmt.fracWidth - 1)) : (ofModel fmt (Float.Model.UnpackedFloat.roundWithAccuracy fmt.toModel sign mantissa exponent accuracy)).isFinite = true

Rounding a positive certified real below the overflow threshold 2^(maxNormal + 1) - 2^(maxNormal - fracWidth - 1) never overflows, so the packed result is finite. Below 2^maxNormal this is isFinite_ofModel_roundWithAccuracy_of_lt_bpow. In the top binade the bound keeps the rounded mantissa below 2^(fracWidth + 1), so no carry reaches the next binade.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_modelSqrt_of_lt_bpow (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (mantissa : ℕ) (exponent : ℤ) (hmantissa : mantissa ≠ 0) (hbound : ↑mantissa * Flocq.bpow Numerics.binaryRadix exponent < Flocq.bpow Numerics.binaryRadix (2 * Int.ofNat fmt.ieeeMaxNormalExponent)) : (ofModel fmt (Float.Model.UnpackedFloat.sqrt fmt.toModel (Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.positive mantissa exponent ⋯))).isFinite = true

Lean's positive finite model square root packs to a finite word whenever the radicand is below 2^(2 * maxNormal), which every finite IEEE value is.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_sqrt_of_isFinite {fmt : FloatFormat} (x : Model fmt) (hfmt : fmt.isIEEE = true) (hfinite : x.isFinite = true) (hdomain : x.isZero = true ∨ x.signBit = false) : isFinite x.sqrt = true

The square root of a finite nonnegative value, including either signed zero, is finite for every conventional IEEE descriptor. The largest finite value exceeds one, so its square root lies below it and rounding cannot reach infinity.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isZero_or_signBit_eq_false_of_toReal_nonneg {fmt : FloatFormat} (x : Model fmt) (hfinite : x.isFinite = true) (hnonneg : 0 ≤ x.toReal) : x.isZero = true ∨ x.signBit = false

A finite value with a nonnegative real interpretation satisfies the domain condition of toReal_sqrt_eq_roundAt: it is a zero of either sign, or its sign bit is clear.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_sqrt_eq_roundAt {fmt : FloatFormat} (x : Model fmt) (hfmt : fmt.isIEEE = true) (hfinite : x.isFinite = true) (hdomain : x.isZero = true ∨ x.signBit = false) : toReal x.sqrt = roundAt fmt √x.toReal

Generic executable square root performs one nearest-even rounding of the exact real square root on every finite, nonnegative conventional IEEE input. The domain condition includes both signed zeros. Alone among the arithmetic operations, it assumes no finiteness of the result: isFinite_sqrt_of_isFinite shows that square root cannot overflow.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_sqrt_nonneg {fmt : FloatFormat} (mode : IEEERoundingMode) {x : Model fmt} (hfinite : x.isFinite = true) (hzero : x.isZero = false) (hsign : x.signBit = false) : 0 ≤ toReal (x.sqrt mode)

The square root of a positive finite value is nonnegative in every rounding direction and for every descriptor.