Least-quantum cohorts of inexact square roots

The comparison is between the actual rounded root and every valid representation of that rounded value. It does not assume that the mathematical root is rational.

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtPair_minimum_or_full (f : Format) (mode : RoundingMode) {x : ℚ} (hx : 0 ≤ x) : (sqrtPair f mode x).2 = f.minQuantum ∨ f.payloadBound ≤ (sqrtPair f mode x).1

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtPair_quantum_minimal (f : Format) (mode : RoundingMode) {x : ℚ} (hx : 0 ≤ x) (d : ℕ) (r : ℤ) (hd : d < f.coefficientBound) (hr : f.minQuantum ≤ r) (hvalue : ↑(sqrtPair f mode x).1 * 10 ^ (sqrtPair f mode x).2 = ↑d * 10 ^ r) : (sqrtPair f mode x).2 ≤ r

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtMagnitude_inexact_quantum_minimal (f : Format) (mode : RoundingMode) {x : ℚ} (hx : 0 ≤ x) (preferred : ℤ) (hinexact : (sqrtMagnitude f mode x preferred).status.inexact = true) (c : ℕ) (q : ℤ) (hout : (sqrtMagnitude f mode x preferred).value = Datum.finite false c q) (d : ℕ) (r : ℤ) (hv : Datum.Valid f (Datum.finite false d r)) (hvalue : ↑c * 10 ^ q = ↑d * 10 ^ r) : q ≤ r

An inexact finite root has the least quantum in its valid cohort, even when the exact root is irrational.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.sqrt_inexact_quantum_minimal (f : Format) (mode : RoundingMode) (s : Bool) (a : ℕ) (b : ℤ) (hinexact : (sqrt f mode (Datum.finite s a b)).status.inexact = true) (c : ℕ) (q : ℤ) (hout : (sqrt f mode (Datum.finite s a b)).value = Datum.finite false c q) (d : ℕ) (r : ℤ) (hv : Datum.Valid f (Datum.finite false d r)) (hvalue : ↑c * 10 ^ q = ↑d * 10 ^ r) : q ≤ r

Every inexact finite result of the public square root uses the least quantum in its cohort.