Coefficient range for decimal square root

Halving the base-ten logarithm of the squared scaled value determines the square-root grid. The proofs use integer logarithm bounds, without approximating the square root.

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtScaleShift_upper (p : ℕ) {x : ℚ} (hx : 0 ≤ x) : x < 10 ^ (2 * (p + sqrtScaleShift p x))

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtQuantum_ge_min (f : Format) (x : ℚ) : f.minQuantum ≤ sqrtQuantum f x

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtScaleShift_le_of_lt {p k : ℕ} (hp : 0 < p) {x : ℚ} (hx : 0 ≤ x) (h : x < 10 ^ (2 * (p + k))) : sqrtScaleShift p x ≤ k

A fitting square bounds the grid shift without computing its root.

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

Every valid representation of an exact root is on a grid no finer than the selected grid.

theorem FloatLib.Floats.Formats.DecimalInterchange.div_sqrtQuantum_lt (f : Format) {x : ℚ} (hx : 0 ≤ x) : x / 10 ^ (2 * sqrtQuantum f x) < ↑f.coefficientBound ^ 2

The square of the scaled coefficient is strictly below the squared coefficient bound.

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtScaleShift_lower {p : ℕ} (hp : 0 < p) {x : ℚ} (hx : 0 ≤ x) (hk : 0 < sqrtScaleShift p x) : 10 ^ (2 * (p + sqrtScaleShift p x - 1)) ≤ x

A nonzero square-root grid shift retains a full leading digit before rounding.

theorem FloatLib.Floats.Formats.DecimalInterchange.payloadBound_sq_le_div_sqrtQuantum (f : Format) {x : ℚ} (hx : 0 ≤ x) (hq : f.minQuantum < sqrtQuantum f x) : ↑f.payloadBound ^ 2 ≤ x / 10 ^ (2 * sqrtQuantum f x)

Above the subnormal grid, the scaled radicand is at least the square of a full leading digit.