Boundary behavior of adjacent-value operations

These theorems describe nextUp and nextDown at NaNs, zeros, infinities, and saturating finite endpoints. They also extend the exact rank-step results from Adjacent.Proof.Core to one-sided rank inequalities that remain valid at fixed endpoints.

Exceptional values and boundaries

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.nextUp_of_isNaN {fmt : FloatFormat} (x : Model fmt) (hx : x.isNaN = true) : x.nextUp = x.quietNaN

On a NaN, nextUp returns the format's quietNaN result.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.nextDown_of_isNaN {fmt : FloatFormat} (x : Model fmt) (hx : x.isNaN = true) : x.nextDown = x.quietNaN

On a NaN, nextDown returns the format's quietNaN result.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.nextUp_of_isInf_of_signBit_eq_false {fmt : FloatFormat} (x : Model fmt) (hinf : x.isInf = true) (hsign : x.signBit = false) : x.nextUp = x

Positive infinity is the fixed upper endpoint of nextUp.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.nextDown_of_isInf_of_signBit_eq_true {fmt : FloatFormat} (x : Model fmt) (hinf : x.isInf = true) (hsign : x.signBit = true) : x.nextDown = x

Negative infinity is the fixed lower endpoint of nextDown.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.nextUp_of_isZero {fmt : FloatFormat} (x : Model fmt) (hx : x.isZero = true) : x.nextUp = posMinSubnormal fmt

Both signed zeros step upward to the least positive subnormal.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.nextDown_of_isZero {fmt : FloatFormat} (x : Model fmt) (hx : x.isZero = true) : x.nextDown = negMinSubnormal fmt

Both signed zeros step downward to the negative subnormal of least magnitude.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.nextUp_negMinSubnormal_of_not_supportsSignedZero (fmt : FloatFormat) (hfmt : fmt.supportsSignedZero = false) : (negMinSubnormal fmt).nextUp = posZero fmt

An unsigned-zero format steps directly from its negative subnormal of least magnitude to zero, skipping the reserved sign-mask NaN word.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.nextUp_posMaxFinite_of_not_supportsInfinity (fmt : FloatFormat) (hfmt : fmt.supportsInfinity = false) : (posMaxFinite fmt).nextUp = posMaxFinite fmt

A format without infinity saturates nextUp at its largest finite value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.nextDown_negMaxFinite_of_not_supportsInfinity (fmt : FloatFormat) (hfmt : fmt.supportsInfinity = false) : (negMaxFinite fmt).nextDown = negMaxFinite fmt

A format without infinity saturates nextDown at its most negative finite value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.nextUp_posInf_of_supportsInfinity (fmt : FloatFormat) (hfmt : fmt.supportsInfinity = true) : (posInf fmt).nextUp = posInf fmt

A represented positive infinity is fixed by nextUp.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.nextDown_negInf_of_supportsInfinity (fmt : FloatFormat) (hfmt : fmt.supportsInfinity = true) : (negInf fmt).nextDown = negInf fmt

A represented negative infinity is fixed by nextDown.

Rank inequalities including saturating endpoints

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.adjacencyRank_le_nextUp {fmt : FloatFormat} (x : Model fmt) (hnan : x.isNaN = false) : x.adjacencyRank ≤ x.nextUp.adjacencyRank

For every non-NaN value, nextUp never decreases the adjacency rank.

Ordinary values advance exactly one rank. Positive infinity and the largest finite value of a format without infinity are fixed points, so the inequality becomes equality at those endpoints.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.adjacencyRank_nextDown_le {fmt : FloatFormat} (x : Model fmt) (hnan : x.isNaN = false) : x.nextDown.adjacencyRank ≤ x.adjacencyRank

For every non-NaN value, nextDown never increases the adjacency rank.

Ordinary values retreat exactly one rank. Negative infinity and the most negative finite value of a format without infinity are fixed points, so the inequality becomes equality at those endpoints.