Successor and predecessor on a normalized decimal grid

The downward step immediately below a radix power is expressed on the finer grid. Its upward grid step recovers the original value, so the same grid-gap theorem establishes adjacency in both directions.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.neighborAbove_valid (f : Format) (c : ℕ) (q : ℤ) (hqmin : f.minQuantum ≤ q) (hqmax : q ≤ f.maxQuantum) : Datum.Valid f (neighborAbove f c q)

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.neighborAbove_finite (f : Format) (c d : ℕ) (q r : ℤ) (s : Bool) (hc : c < f.coefficientBound) (hout : neighborAbove f c q = Datum.finite s d r) : s = false ∧ ↑d * 10 ^ r = ↑(c + 1) * 10 ^ q

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.neighborAbove_full (f : Format) (c d : ℕ) (q r : ℤ) (s : Bool) (hfull : q = f.minQuantum ∨ f.payloadBound ≤ c) (hout : neighborAbove f c q = Datum.finite s d r) : r = f.minQuantum ∨ f.payloadBound ≤ d

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.neighborBelow_spec (f : Format) (c : ℕ) (q : ℤ) (hc : c < f.coefficientBound) (hcpos : 0 < c) (hqmin : f.minQuantum ≤ q) (hqmax : q ≤ f.maxQuantum) (hfull : q = f.minQuantum ∨ f.payloadBound ≤ c) : ∃ (d : ℕ) (r : ℤ), neighborBelow f c q = Datum.finite false d r ∧ Datum.Valid f (Datum.finite false d r) ∧ (r = f.minQuantum ∨ f.payloadBound ≤ d) ∧ ↑(d + 1) * 10 ^ r = ↑c * 10 ^ q

The predecessor of a normalized positive input is valid, normalized, and one upward grid step below the input. It may be zero.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.neighbor_le_max (f : Format) (d : ℕ) (r : ℤ) (hd : d < f.coefficientBound) (hr : r ≤ f.maxQuantum) : ↑d * 10 ^ r ≤ ↑(f.coefficientBound - 1) * 10 ^ f.maxQuantum

Upper bound on every finite magnitude, including all nonminimal cohorts.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.neighborAbove_infinity (f : Format) (c : ℕ) (q : ℤ) (hc : c < f.coefficientBound) (hq : q ≤ f.maxQuantum) (hout : neighborAbove f c q = Datum.infinity false) : c = f.coefficientBound - 1 ∧ q = f.maxQuantum

An infinite successor requires the greatest finite magnitude.