Neighbor range, status and cohort guarantees

Normalization preserves the input value and exposes its smallest quantum. Both coefficient steps return a normalized representation, including signed zero and the finite endpoints. NaN propagation is the only source of a flag.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.neighbor_normalize (f : Format) (s : Bool) (c : ℕ) (q : ℤ) (hvalid : Datum.Valid f (Datum.finite s c q)) (hc : c ≠ 0) : ∃ (d : ℕ) (r : ℤ), roundedPair f RoundingMode.nearestEven false (↑c * 10 ^ q) = (d, r) ∧ d < f.coefficientBound ∧ 0 < d ∧ f.minQuantum ≤ r ∧ r ≤ f.maxQuantum ∧ (r = f.minQuantum ∨ f.payloadBound ≤ d) ∧ ↑d * 10 ^ r = ↑c * 10 ^ q

Exact input normalization supplies the hypotheses of the grid-step proofs.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.nextUp_valid (f : Format) (x : Datum) (hx : Datum.Valid f x) : Datum.Valid f (nextUp f x).value

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.nextDown_valid (f : Format) (x : Datum) (hx : Datum.Valid f x) : Datum.Valid f (nextDown f x).value

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.nextUp_status (f : Format) (x : Datum) : (nextUp f x).status = { invalid := x.isSignaling }

Neighbor steps raise invalid exactly for signaling NaNs and leave all other flags clear.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.nextDown_status (f : Format) (x : Datum) : (nextDown f x).status = { invalid := x.isSignaling }

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.nextUp_full (f : Format) (x : Datum) (hx : Datum.Valid f x) (s : Bool) (c : ℕ) (q : ℤ) (hout : (nextUp f x).value = Datum.finite s c q) : q = f.minQuantum ∨ f.payloadBound ≤ c

Every finite successor has a full leading digit unless it is on the smallest grid.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.nextUp_quantum_minimal (f : Format) (x : Datum) (hx : Datum.Valid f x) (s : Bool) (c : ℕ) (q : ℤ) (hout : (nextUp f x).value = Datum.finite s c q) (d : ℕ) (r : ℤ) (hd : Datum.Valid f (Datum.finite s d r)) (he : ↑c * 10 ^ q = ↑d * 10 ^ r) : q ≤ r

The actual successor's quantum is minimal among all valid equal-magnitude cohorts.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.nextDown_quantum_minimal (f : Format) (x : Datum) (hx : Datum.Valid f x) (s : Bool) (c : ℕ) (q : ℤ) (hout : (nextDown f x).value = Datum.finite s c q) (d : ℕ) (r : ℤ) (hd : Datum.Valid f (Datum.finite s d r)) (he : ↑c * 10 ^ q = ↑d * 10 ^ r) : q ≤ r