Adjacency of the public decimal neighbor operations

The quantified bounds compare the delivered result with every valid finite datum, including other cohorts and either sign of zero. The endpoint theorems cover infinite results separately.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.nextUp_finite_adjacent (f : Format) (s : Bool) (c : ℕ) (q : ℤ) (hx : Datum.Valid f (Datum.finite s c q)) (v : ℚ) (hout : (nextUp f (Datum.finite s c q)).value.toRat? = some v) : Datum.finiteValue s c q < v ∧ ∀ (t : Bool) (d : ℕ) (r : ℤ), Datum.Valid f (Datum.finite t d r) → Datum.finiteValue s c q < Datum.finiteValue t d r → v ≤ Datum.finiteValue t d r

The finite successor is strictly greater, and no valid finite value lies between them.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.nextUp_adjacent (f : Format) (x : Datum) (hx : Datum.Valid f x) (a b : ℚ) (ha : x.toRat? = some a) (hb : (nextUp f x).value.toRat? = some b) : a < b ∧ ∀ (y : Datum) (v : ℚ), Datum.Valid f y → y.toRat? = some v → a < v → b ≤ v

Public successor adjacency expressed entirely in exact numerical values.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.nextDown_adjacent (f : Format) (x : Datum) (hx : Datum.Valid f x) (a b : ℚ) (ha : x.toRat? = some a) (hb : (nextDown f x).value.toRat? = some b) : b < a ∧ ∀ (y : Datum) (v : ℚ), Datum.Valid f y → y.toRat? = some v → v < a → v ≤ b

Negation transfers successor adjacency to the public predecessor operation.