Correctness of P3109 neighboring values

The exact numerical ordering of non-NaN values is a consecutive integer interval. The upper and lower neighbor operations move by one in that interval, returning NaN precisely when the requested neighbor does not exist. Infinite endpoints obey the same order as finite values.

def FloatLib.Floats.Formats.P3109.Format.firstOrderIndex (format : Format) : ℤ

Index of the least numerical datum; unsigned formats begin at zero.

def FloatLib.Floats.Formats.P3109.Format.lastOrderIndex (format : Format) : ℤ

Index of the greatest numerical datum, whether finite or infinite.

theorem FloatLib.Floats.Formats.P3109.Format.orderIndex_bounds (format : Format) (bits : ℕ) (hbits : bits < format.modulus) (hnan : bits ≠ format.nanBits) : format.firstOrderIndex ≤ format.orderIndex bits ∧ format.orderIndex bits ≤ format.lastOrderIndex

Every non-NaN code lies in the numerical index interval.

theorem FloatLib.Floats.ExecFloat.P3109.toNatBits_lt_modulus {format : Formats.P3109.Format} (value : P3109 format) : value.toNatBits < format.modulus

Every executable code fits the declared descriptor width.

def FloatLib.Floats.ExecFloat.P3109.orderIndex {format : Formats.P3109.Format} (value : P3109 format) : ℤ

Numerical-order index of an executable value, used only after excluding NaN.

theorem FloatLib.Floats.ExecFloat.P3109.isNaN_iff_decode {format : Formats.P3109.Format} (value : P3109 format) : value.isNaN = true ↔ value.decode = Numerics.NumericalValue.exceptional Numerics.ExceptionalValue.nan

The executable NaN predicate agrees with exact decoding.

theorem FloatLib.Floats.ExecFloat.P3109.less_of_isNaN_left {format : Formats.P3109.Format} (left right : P3109 format) (hleft : left.isNaN = true) : left.less right = false

A NaN left operand is unordered under the public strict comparison.

theorem FloatLib.Floats.ExecFloat.P3109.less_of_isNaN_right {format : Formats.P3109.Format} (left right : P3109 format) (hright : right.isNaN = true) : left.less right = false

A NaN right operand is unordered under the public strict comparison.

theorem FloatLib.Floats.ExecFloat.P3109.less_iff_orderIndex {format : Formats.P3109.Format} (left right : P3109 format) : left.less right = true ↔ left.isNaN = false ∧ right.isNaN = false ∧ left.orderIndex < right.orderIndex

Public strict comparison agrees with integer-index order, with NaN excluded explicitly.

theorem FloatLib.Floats.ExecFloat.P3109.orderIndex_bounds {format : Formats.P3109.Format} (value : P3109 format) (hnan : value.isNaN = false) : format.firstOrderIndex ≤ value.orderIndex ∧ value.orderIndex ≤ format.lastOrderIndex

Non-NaN executable values lie between the numerical index endpoints.

@[simp]

theorem FloatLib.Floats.ExecFloat.P3109.toNatBits_zero {format : Formats.P3109.Format} : zero.toNatBits = 0

The public zero constructor has code zero.

@[simp]

theorem FloatLib.Floats.ExecFloat.P3109.toNatBits_nan {format : Formats.P3109.Format} : nan.toNatBits = format.nanBits

The public NaN constructor has the descriptor's unique NaN code.

theorem FloatLib.Floats.ExecFloat.P3109.nextGreaterThan_orderIndex {format : Formats.P3109.Format} (value : P3109 format) (hnan : value.isNaN = false) (hindex : value.orderIndex < format.lastOrderIndex) : value.nextGreaterThan.isNaN = false ∧ value.nextGreaterThan.orderIndex = value.orderIndex + 1

Below the greatest datum, the upper neighbor exists and advances the order index by one.

theorem FloatLib.Floats.ExecFloat.P3109.nextLessThan_orderIndex {format : Formats.P3109.Format} (value : P3109 format) (hnan : value.isNaN = false) (hindex : format.firstOrderIndex < value.orderIndex) : value.nextLessThan.isNaN = false ∧ value.nextLessThan.orderIndex = value.orderIndex - 1

Above the least datum, the lower neighbor exists and retreats by one in numerical order.

theorem FloatLib.Floats.ExecFloat.P3109.nextGreaterThan_eq_nan_of_last {format : Formats.P3109.Format} (value : P3109 format) (hindex : value.orderIndex = format.lastOrderIndex) : value.nextGreaterThan = nan

The greatest numerical datum has no upper neighbor, in either finite or extended formats.

theorem FloatLib.Floats.ExecFloat.P3109.nextLessThan_eq_nan_of_first {format : Formats.P3109.Format} (value : P3109 format) (hindex : value.orderIndex = format.firstOrderIndex) : value.nextLessThan = nan

The least numerical datum has no lower neighbor, in either finite or extended formats.

theorem FloatLib.Floats.ExecFloat.P3109.less_nextGreaterThan {format : Formats.P3109.Format} (value candidate : P3109 format) (h : value.less candidate = true) : value.less value.nextGreaterThan = true

Whenever a greater value exists, the upper neighbor is strictly greater than the input.

theorem FloatLib.Floats.ExecFloat.P3109.not_less_nextGreaterThan {format : Formats.P3109.Format} (value candidate : P3109 format) (h : value.less candidate = true) : candidate.less value.nextGreaterThan = false

No value greater than the input is smaller than its upper neighbor.

theorem FloatLib.Floats.ExecFloat.P3109.nextLessThan_less {format : Formats.P3109.Format} (value candidate : P3109 format) (h : candidate.less value = true) : value.nextLessThan.less value = true

Whenever a lesser value exists, the lower neighbor is strictly smaller than the input.

theorem FloatLib.Floats.ExecFloat.P3109.not_nextLessThan_less {format : Formats.P3109.Format} (value candidate : P3109 format) (h : candidate.less value = true) : value.nextLessThan.less candidate = false

No value smaller than the input is greater than its lower neighbor.

theorem FloatLib.Floats.ExecFloat.P3109.nextGreaterThan_isNaN_iff {format : Formats.P3109.Format} (value : P3109 format) : value.nextGreaterThan.isNaN = true ↔ ¬∃ (candidate : P3109 format), value.less candidate = true

The upper-neighbor result is NaN exactly when the numerical order has no greater datum.

theorem FloatLib.Floats.ExecFloat.P3109.nextLessThan_isNaN_iff {format : Formats.P3109.Format} (value : P3109 format) : value.nextLessThan.isNaN = true ↔ ¬∃ (candidate : P3109 format), candidate.less value = true

The lower-neighbor result is NaN exactly when the numerical order has no lesser datum.