Exact representable square roots

On a finer decimal grid, a representable root has an integer coefficient. Squaring that integer identifies the scaled radicand exactly, so every rounding mode recovers the same root. No test for irrationality is needed.

theorem FloatLib.Floats.Formats.DecimalInterchange.scaled_decimal_sq (c : ℕ) {q r : ℤ} (hqr : r ≤ q) : (↑c * 10 ^ q) ^ 2 / 10 ^ (2 * r) = ↑(c * 10 ^ (q - r).toNat) ^ 2

Refining a root's decimal grid produces an exact integer square after scaling.

theorem FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.sqrtRound_exact_value (mode : RoundingMode) (c : ℕ) {q r : ℤ} (hqr : r ≤ q) : ↑(mode.sqrtRound ((↑c * 10 ^ q) ^ 2 / 10 ^ (2 * r))) * 10 ^ r = ↑c * 10 ^ q

Recovering a representable root on any finer grid preserves its exact value.

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtRound_lt_coefficientBound_of_valid (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q : ℤ) (hvalid : Datum.Valid f (Datum.finite s c q)) : mode.sqrtRound ((↑c * 10 ^ q) ^ 2 / 10 ^ (2 * sqrtQuantum f ((↑c * 10 ^ q) ^ 2))) < f.coefficientBound

The coefficient of an exact representable root cannot require a carry.

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtPair_quantum_le_of_valid (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q : ℤ) (hvalid : Datum.Valid f (Datum.finite s c q)) : (sqrtPair f mode ((↑c * 10 ^ q) ^ 2)).2 ≤ q

An exact root's normalized grid is no coarser than any valid representation of that root.

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtPair_exact_value (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q : ℤ) (hvalid : Datum.Valid f (Datum.finite s c q)) : ↑(sqrtPair f mode ((↑c * 10 ^ q) ^ 2)).1 * 10 ^ (sqrtPair f mode ((↑c * 10 ^ q) ^ 2)).2 = ↑c * 10 ^ q

All five modes recover every representable nonnegative root exactly.

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtMagnitude_exact_status (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q preferred : ℤ) (hvalid : Datum.Valid f (Datum.finite s c q)) : (sqrtMagnitude f mode ((↑c * 10 ^ q) ^ 2) preferred).status = { }

Exact representable roots raise none of the five default exception flags.

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtMagnitude_exact (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q preferred : ℤ) (hvalid : Datum.Valid f (Datum.finite s c q)) : (sqrtMagnitude f mode ((↑c * 10 ^ q) ^ 2) preferred).value.toRat? = some (↑c * 10 ^ q)

Exact square-root projection returns the nonnegative root, regardless of its representation.