Real meaning of square-root exponent selection

If a positive radicand has leading binary exponent L, its square root has leading exponent L / 2, using integer floor division. Scaling the radicand by 2^(-2Q) therefore scales its real square root by 2^(-Q). These facts connect the exact integer rounder to the report's normal and subnormal quantum formula.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.sqrt_floorLog2_bounds (numerator denominator : ℕ) (hn : numerator ≠ 0) (hd : denominator ≠ 0) : have exponent := Numerics.RationalBinary.floorLog2 numerator denominator / 2; BinaryInterchange.Model.bpow exponent ≤ √(↑numerator / ↑denominator) ∧ √(↑numerator / ↑denominator) < BinaryInterchange.Model.bpow (exponent + 1)

Floor division by two gives the leading exponent of the actual positive square root.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.sqrt_scaled_ratio (numerator denominator : ℕ) (quantum : ℤ) : have scaled := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (-2 * quantum); √(↑scaled.1 / ↑scaled.2) = √(↑numerator / ↑denominator) * BinaryInterchange.Model.bpow (-quantum)

Squaring the exponent scale preserves the exact real square root, including irrational roots.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.nonnegative_rat_eq_ratio (radicand : ℚ) (h : 0 ≤ radicand) : ↑radicand.num.natAbs / ↑radicand.den = ↑radicand

A nonnegative rational is represented by the numerator magnitude used by the root kernel.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.sqrt_scaled_radicand (format : Format) (radicand : ℚ) (h : 0 ≤ radicand) : have quantum := sqrtQuantum format radicand.num.natAbs radicand.den; have scaled := Numerics.RationalBinary.scaleByPowerOfTwo radicand.num.natAbs radicand.den (-2 * quantum); √(↑scaled.1 / ↑scaled.2) = √↑radicand * BinaryInterchange.Model.bpow (-quantum)

The reference significand is the actual nonnegative root scaled by the chosen binary quantum.