Decimal grid gaps

A least-quantum representation is either on the subnormal grid or has a full leading digit. Every finer-grid representation is below that leading digit; every coarser-grid representation occupies an integer point on the current grid. These two facts exclude all representable values between consecutive coefficients.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.neighbor_finer_lt (f : Format) (d : ℕ) (q r : ℤ) (hd : d < f.coefficientBound) (hr : r < q) : ↑d * 10 ^ r < ↑f.payloadBound * 10 ^ q

A bounded finer-grid coefficient lies below the next grid's full leading digit.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.neighbor_integer_gap (c d : ℕ) (q r : ℤ) (hqr : q ≤ r) (hlt : ↑c * 10 ^ q < ↑d * 10 ^ r) : ↑(c + 1) * 10 ^ q ≤ ↑d * 10 ^ r

Coarser decimal grids contain only integer points of every finer grid.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.neighbor_gap (f : Format) (c d : ℕ) (q r : ℤ) (hfull : q = f.minQuantum ∨ f.payloadBound ≤ c) (hd : d < f.coefficientBound) (hr : f.minQuantum ≤ r) (hlt : ↑c * 10 ^ q < ↑d * 10 ^ r) : ↑(c + 1) * 10 ^ q ≤ ↑d * 10 ^ r

No valid decimal value occurs between a normalized coefficient and its successor.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.neighbor_quantum_minimal (f : Format) (c d : ℕ) (q r : ℤ) (hfull : q = f.minQuantum ∨ f.payloadBound ≤ c) (hd : d < f.coefficientBound) (hr : f.minQuantum ≤ r) (he : ↑c * 10 ^ q = ↑d * 10 ^ r) : q ≤ r

Any normalized pair is the least-quantum member of its entire valid cohort.