Correctness of rational integer-root certificates

Integer division followed by integer root brackets the real root of a nonnegative rational. The shared Newton kernel supplies the exact floor root without repeated power checks. Uniqueness of the integer part identifies its result with the comparison search. The root's binade follows from the radicand's binary logarithm and Euclidean division. These facts preserve the complete encoded result for every descriptor.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.rootBinade_bounds (radicand : ℚ) (degree : ℕ) (target : ℝ) (hrad : 0 < radicand) (hdegree : degree ≠ 0) (htarget : 0 ≤ target) (hroot : target ^ degree = ↑radicand) : Flocq.bpow Numerics.binaryRadix (rootBinade radicand degree) ≤ target ∧ target < Flocq.bpow Numerics.binaryRadix (rootBinade radicand degree + 1)

Dividing the radicand's floor binary logarithm locates every positive-degree root's binade.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.rootBinade_eq_binade (fmt : FloatFormat) (radicand : ℚ) (degree : ℕ) (target : ℝ) (hrad : 0 < radicand) (hdegree : degree ≠ 0) (htarget : 0 ≤ target) (hroot : target ^ degree = ↑radicand) (hlower : Flocq.bpow Numerics.binaryRadix (lowerExponent fmt) ≤ target) (hupper : target < Flocq.bpow Numerics.binaryRadix (upperExponent fmt)) : rootBinade radicand degree = binade fmt (Posit.Model.RootRounding.compareRoot radicand degree)

The computed root binade agrees with the bounded search throughout the finite interval.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.rootScale_real (radicand : ℚ) (degree : ℕ) (exponent : ℤ) (hrad : 0 ≤ radicand) : ↑(rootScale radicand degree exponent).1 / ↑(rootScale radicand degree exponent).2 = ↑radicand / Flocq.bpow Numerics.binaryRadix exponent ^ degree

Raw integer scaling preserves the exact radicand without rational normalization.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.rootScale_den_pos (radicand : ℚ) (degree : ℕ) (exponent : ℤ) : 0 < (rootScale radicand degree exponent).2

Scaling preserves the positive denominator required by integer root comparisons.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.cmp_integerPower_eq_root (numerator denominator degree candidate : ℕ) (target : ℝ) (hden : 0 < denominator) (hdegree : degree ≠ 0) (htarget : 0 ≤ target) (hroot : target ^ degree = ↑numerator / ↑denominator) : cmp numerator (candidate ^ degree * denominator) = cmp target ↑candidate

Integer cross-multiplication compares an exact nonnegative root with an integer.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.cmp_halfIntegerPower_eq_root (numerator denominator degree candidate : ℕ) (target : ℝ) (hden : 0 < denominator) (hdegree : degree ≠ 0) (htarget : 0 ≤ target) (hroot : target ^ degree = ↑numerator / ↑denominator) : cmp (numerator <<< degree) ((2 * candidate + 1) ^ degree * denominator) = cmp target (↑candidate + 1 / 2)

Doubling the candidate compares the exact root with a half-integer using only integers.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.sqrtQuotient_bounds (numerator denominator : ℕ) (hd : 0 < denominator) : ↑(numerator / denominator).sqrt ≤ √(↑numerator / ↑denominator) ∧ √(↑numerator / ↑denominator) < ↑(numerator / denominator).sqrt + 1

Integer square root of an integer quotient brackets the square root of the exact quotient.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.sqrtMantissa_bounds (radicand : ℚ) (exponent : ℤ) (hrad : 0 ≤ radicand) : ↑(sqrtMantissa radicand exponent) ≤ √↑radicand / Flocq.bpow Numerics.binaryRadix exponent ∧ √↑radicand / Flocq.bpow Numerics.binaryRadix exponent < ↑(sqrtMantissa radicand exponent) + 1

Target scaling commutes with the nonnegative square root.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.rootMantissa_eq_truncatedMantissa (fmt : FloatFormat) (radicand : ℚ) (degree : ℕ) (target : ℝ) (exponent : ℤ) (hrad : 0 ≤ radicand) (hdegree : degree ≠ 0) (htarget : 0 ≤ target) (hroot : target ^ degree = ↑radicand) (hupper : target / Flocq.bpow Numerics.binaryRadix exponent < 2 ^ (fmt.fracWidth + 3)) : rootMantissa fmt radicand degree exponent = truncatedMantissa fmt (Posit.Model.RootRounding.compareRoot radicand degree) exponent

The exact integer root agrees with the comparison search throughout its finite interval.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.rootAccuracy_eq_accuracyAt (radicand : ℚ) (degree : ℕ) (exponent : ℤ) (mantissa : ℕ) (target : ℝ) (hrad : 0 ≤ radicand) (hdegree : degree ≠ 0) (htarget : 0 ≤ target) (hroot : target ^ degree = ↑radicand) : rootAccuracy radicand degree exponent mantissa = accuracyAt (fun (candidate : ℚ) => Posit.Model.RootRounding.compareRoot radicand degree (candidate * powerOfTwo exponent)) mantissa

Integer comparisons preserve the complete exactness and midpoint classification.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.rootCertificateAt_eq (fmt : FloatFormat) (radicand : ℚ) (degree : ℕ) (exponent : ℤ) : rootCertificateAt fmt radicand degree exponent = { mantissa := rootMantissa fmt radicand degree exponent, exponent := exponent, accuracy := rootAccuracy radicand degree exponent (rootMantissa fmt radicand degree exponent) }

Sharing the scaled ratio preserves every field of the accuracy certificate.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.rootCertificate_eq_certificate (fmt : FloatFormat) (radicand : ℚ) (degree : ℕ) (target : ℝ) (hrad : 0 < radicand) (hdegree : degree ≠ 0) (htarget : 0 ≤ target) (hroot : target ^ degree = ↑radicand) (hlower : Flocq.bpow Numerics.binaryRadix (lowerExponent fmt) ≤ target) (hupper : target < Flocq.bpow Numerics.binaryRadix (upperExponent fmt)) : rootCertificate fmt radicand degree = certificate fmt (Posit.Model.RootRounding.compareRoot radicand degree)

Integer-root construction preserves every field of the reference accuracy certificate.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.sqrtCertificate_eq_certificate (fmt : FloatFormat) (radicand : ℚ) (hrad : 0 ≤ radicand) (hlower : Flocq.bpow Numerics.binaryRadix (lowerExponent fmt) ≤ √↑radicand) (hupper : √↑radicand < Flocq.bpow Numerics.binaryRadix (upperExponent fmt)) : sqrtCertificate fmt radicand = certificate fmt (Posit.Model.RootRounding.compareRoot radicand 2)

The integer-square-root certificate equals the comparison certificate throughout its range.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.rootRat_eq_root (fmt : FloatFormat) (sign : Bool) (radicand : ℚ) (degree : ℕ) : rootRat fmt sign radicand degree = root fmt sign radicand degree

Integer binade classification and exact roots preserve every reference result bit.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.sqrtRat_eq_root (fmt : FloatFormat) (sign : Bool) (radicand : ℚ) (_hrad : 0 ≤ radicand) : sqrtRat fmt sign radicand = root fmt sign radicand 2

The optimized square root preserves every result bit for any complete descriptor.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.toReal_sqrtRat_eq_roundAt (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Bool) (radicand : ℚ) (hrad : 0 ≤ radicand) (hfinite : (sqrtRat fmt sign radicand).isFinite = true) : (sqrtRat fmt sign radicand).toReal = roundAt fmt (if sign = true then -√↑radicand else √↑radicand)

The optimized rational square root rounds the exact real square root once.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.rootWithSqrt_eq_root (fmt : FloatFormat) (sign : Bool) (radicand : ℚ) (degree : ℕ) (_hrad : 0 ≤ radicand) : rootWithSqrt fmt sign radicand degree = root fmt sign radicand degree

Selecting the square-root specialization preserves the complete general-root result.