Adjacent decimal values

IEEE 754-2019 §5.3.1 requires the nearest strictly greater or smaller value, selecting the least quantum in its cohort. Normalizing the input to its finest grid makes this a coefficient step. At a power of ten, the downward step uses the finer grid. No rounding direction is consulted.

The adjacency and output-validity guarantees assume x.Valid f, as stated in Neighbors.Proof and Neighbors.Adjacency. A raw Datum does not carry its format; callers must establish this invariant before using these neighbor operations. The normalization step need not preserve an out-of-format input.

Crossing the finite range or reaching a subnormal raises no exception. Only signaling NaNs raise invalid; NaN propagation otherwise follows the arithmetic payload policy.

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.neighborAbove (f : Format) (c : ℕ) (q : ℤ) : Datum

Positive successor of a finite value already on its least quantum.

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.neighborBelow (f : Format) (c : ℕ) (q : ℤ) : Datum

Positive predecessor, using the finer grid immediately below a radix power.

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.nextUp (f : Format) : Datum → Outcome

For a valid non-NaN operand, the least representable value strictly greater than it, except that positive infinity is unchanged.

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.nextDown (f : Format) (x : Datum) : Outcome

For a valid non-NaN operand, the greatest representable value strictly smaller than it, except that negative infinity is unchanged.