Exact square-root bounds for P3109

Integer square root after integer division gives the floor of the real square root of the rational quotient. Cross multiplication of squared nonnegative thresholds preserves its order exactly. These facts justify rounding even when the square root is irrational.

The precision bound proves that the rounded candidate fits the existing P3109 encoder for every valid descriptor, including precision one and subnormal results.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.sqrtFloor_sq_le (numerator denominator : ℕ) (hd : 0 < denominator) : sqrtFloor numerator denominator ^ 2 * denominator ≤ numerator

The square of the lower integer candidate does not exceed the rational radicand.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.lt_succ_sqrtFloor_sq (numerator denominator : ℕ) (hd : 0 < denominator) : numerator < (sqrtFloor numerator denominator + 1) ^ 2 * denominator

The next candidate's square is strictly above the exact radicand.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.sqrtFloor_real_bounds (numerator denominator : ℕ) (hd : 0 < denominator) : ↑(sqrtFloor numerator denominator) ≤ √(↑numerator / ↑denominator) ∧ √(↑numerator / ↑denominator) < ↑(sqrtFloor numerator denominator) + 1

Integer square root of the quotient brackets the actual real square root.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.floor_real_sqrt (numerator denominator : ℕ) (hd : 0 < denominator) : ⌊√(↑numerator / ↑denominator)⌋₊ = sqrtFloor numerator denominator

The executable lower candidate is the natural floor of the real square root.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.sqrt_lt_threshold_iff (numerator denominator scale threshold : ℕ) (hd : 0 < denominator) (hs : 0 < scale) : √(↑numerator / ↑denominator) < ↑threshold / ↑scale ↔ numerator * scale ^ 2 < denominator * threshold ^ 2

Squaring a nonnegative rational threshold preserves strict comparison with the root.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.sqrt_eq_threshold_iff (numerator denominator scale threshold : ℕ) (hd : 0 < denominator) (hs : 0 < scale) : √(↑numerator / ↑denominator) = ↑threshold / ↑scale ↔ numerator * scale ^ 2 = denominator * threshold ^ 2

A rational threshold equals the real root exactly when its square equals the radicand.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.compareSqrt_eq_real (numerator denominator scale threshold : ℕ) (hd : 0 < denominator) (hs : 0 < scale) : compareSqrt numerator denominator scale threshold = compare (√(↑numerator / ↑denominator)) (↑threshold / ↑scale)

The integer comparator agrees with comparison of the real root.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.sqrtFloor_lt_precision (format : Format) (numerator denominator : ℕ) (hn : numerator ≠ 0) (hd : denominator ≠ 0) : have quantum := sqrtQuantum format numerator denominator; have scaled := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (-2 * quantum); sqrtFloor scaled.1 scaled.2 < 2 ^ format.precision

The lower root candidate is strictly below the descriptor's significand limit.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.roundSqrtRatToPrecision_fitsPrecisionGrid (format : Format) (mode : RoundingMode) (radicand : ℚ) : format.FitsPrecisionGrid (roundSqrtRatToPrecision format mode radicand)

Every mode's rounded square root fits the direct encoder's precision grid.