Range guarantees for the selected decimal grid

The input's exact coefficient on the selected grid is less than 10 ^ precision. Whenever it is coarser than the subnormal grid, it also retains a full leading digit. These bounds justify the later single-digit carry and overflow decisions.

theorem FloatLib.Floats.Formats.DecimalInterchange.roundingQuantum_zero (f : Format) : roundingQuantum f 0 = f.minQuantum

Zero has no significant digits and therefore uses the least quantum.

theorem FloatLib.Floats.Formats.DecimalInterchange.roundingQuantum_eq (f : Format) (x : ℚ) : roundingQuantum f x = f.minQuantum + ↑(scaleShift f.precision (x / 10 ^ f.minQuantum))

The zero shortcut agrees with the digit-count formula for every rational magnitude.

theorem FloatLib.Floats.Formats.DecimalInterchange.scaleShift_upper (p : ℕ) {x : ℚ} (hx : 0 ≤ x) : x < 10 ^ (p + scaleShift p x)

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

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

Any coarser grid which fits the coefficient bound is above the selected grid.

theorem FloatLib.Floats.Formats.DecimalInterchange.roundingQuantum_ge_min (f : Format) (x : ℚ) : f.minQuantum ≤ roundingQuantum f x

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

The exact scaled magnitude fits strictly below the coefficient bound.

theorem FloatLib.Floats.Formats.DecimalInterchange.roundingQuantum_le (f : Format) {x : ℚ} (hx : 0 ≤ x) {q : ℤ} (hq : f.minQuantum ≤ q) (hfit : x < ↑f.coefficientBound * 10 ^ q) : roundingQuantum f x ≤ q

The selected quantum is the smallest quantum with a fitting exact coefficient.

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

Above the subnormal grid, the exact scaled coefficient has a full leading digit.