Decimal square-root value, range, and error

Carry normalization preserves the rounded root, and preferred-cohort selection preserves its value. The numerical bound compares the returned rational datum with the mathematical real square root. Inexactness is tested by an exact squaring equality.

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtRound_le_coefficientBound (f : Format) (mode : RoundingMode) {x : ℚ} (hx : 0 ≤ x) : mode.sqrtRound (x / 10 ^ (2 * sqrtQuantum f x)) ≤ f.coefficientBound

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtPair_coefficient_lt (f : Format) (mode : RoundingMode) {x : ℚ} (hx : 0 ≤ x) : (sqrtPair f mode x).1 < f.coefficientBound

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtPair_quantum_ge_min (f : Format) (mode : RoundingMode) (x : ℚ) : f.minQuantum ≤ (sqrtPair f mode x).2

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtPair_value (f : Format) (mode : RoundingMode) (x : ℚ) : ↑(sqrtPair f mode x).1 * 10 ^ (sqrtPair f mode x).2 = ↑(mode.sqrtRound (x / 10 ^ (2 * sqrtQuantum f x))) * 10 ^ sqrtQuantum f x

Decimal carry normalization does not change the rounded numerical root.

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtMagnitude_valid (f : Format) (mode : RoundingMode) {x : ℚ} (hx : 0 ≤ x) (preferred : ℤ) : Datum.Valid f (sqrtMagnitude f mode x preferred).value

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.sqrt_valid (f : Format) (mode : RoundingMode) (x : Datum) : Datum.Valid f (sqrt f mode x).value

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtMagnitude_overflow_iff (f : Format) (mode : RoundingMode) (x : ℚ) (preferred : ℤ) : (sqrtMagnitude f mode x preferred).status.overflow = true ↔ f.maxQuantum < (sqrtPair f mode x).2

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtMagnitude_value (f : Format) (mode : RoundingMode) (x : ℚ) (preferred : ℤ) (hq : (sqrtPair f mode x).2 ≤ f.maxQuantum) : (sqrtMagnitude f mode x preferred).value.toRat? = some (↑(mode.sqrtRound (x / 10 ^ (2 * sqrtQuantum f x))) * 10 ^ sqrtQuantum f x)

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrt_scaled (x : ℚ) (q : ℤ) : √↑(x / 10 ^ (2 * q)) * 10 ^ q = √↑x

Scaling by a decimal quantum commutes with the nonnegative mathematical square root.

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtMagnitude_error_le_half (f : Format) (mode : RoundingMode) (hm : mode = RoundingMode.nearestEven ∨ mode = RoundingMode.nearestAway) {x : ℚ} (hx : 0 ≤ x) (preferred : ℤ) (hfinite : (sqrtMagnitude f mode x preferred).status.overflow = false) : ∃ (value : ℚ), (sqrtMagnitude f mode x preferred).value.toRat? = some value ∧ |↑value - √↑x| ≤ 10 ^ sqrtQuantum f x / 2

The actual returned datum is within half a grid unit of the mathematical root.

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtMagnitude_inexact_iff (f : Format) (mode : RoundingMode) {x : ℚ} (hx : 0 ≤ x) (value : ℚ) (preferred : ℤ) (hq : (sqrtPair f mode x).2 ≤ f.maxQuantum) (hv : (sqrtMagnitude f mode x preferred).value.toRat? = some value) : (sqrtMagnitude f mode x preferred).status.inexact = true ↔ ↑value ≠ √↑x

Squared equality tests real numerical exactness, including irrational roots.