Numerical and exceptional-value rules for binary total order

The order laws follow from the order on complete exact data. The numerical theorems connect the predicate to dyadic, real, and extended-real comparisons. The exceptional-value rules state the IEEE sign and signaling-class priorities and FloatLib's implementation-defined payload direction explicitly.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrder_eq_exactValue {fmt : FloatFormat} (x y : Model fmt) : x.totalOrder y = x.exactValue.totalOrder y.exactValue

The model predicate is precisely the shared order on complete decoded data.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrder_refl {fmt : FloatFormat} (x : Model fmt) : x.totalOrder x = true

All binary words precede themselves, including signaling NaNs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrder_total {fmt : FloatFormat} (x y : Model fmt) : x.totalOrder y = true ∨ y.totalOrder x = true

Totality is independent of field width, bias, and exceptional-value policy.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrder_trans {fmt : FloatFormat} {x y z : Model fmt} (hxy : x.totalOrder y = true) (hyz : y.totalOrder z = true) : x.totalOrder z = true

Binary total ordering is transitive for every descriptor.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrder_both_iff_exactValue_eq {fmt : FloatFormat} (x y : Model fmt) : x.totalOrder y = true ∧ y.totalOrder x = true ↔ x.exactValue = y.exactValue

Mutual ordering identifies the complete decoded data for every descriptor.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrder_antisymm {fmt : FloatFormat} {x y : Model fmt} (hxy : x.totalOrder y = true) (hyx : y.totalOrder x = true) : x = y

Complete decoded data determine their binary word, so total order is antisymmetric.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrder_both_iff {fmt : FloatFormat} (x y : Model fmt) : x.totalOrder y = true ∧ y.totalOrder x = true ↔ x = y

Mutual comparison holds exactly for bitwise-identical operands.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrder_iff_of_toDyadic? {fmt : FloatFormat} {x y : Model fmt} {a b : Numerics.Dyadic} (hx : x.toDyadic? = some a) (hy : y.toDyadic? = some b) : x.totalOrder y = true ↔ a.toRat < b.toRat ∨ a.toRat = b.toRat ∧ (a.negative = true ∧ b.negative = false ∨ a.negative = b.negative ∧ if a.negative = true then b.exponent ≤ a.exponent else a.exponent ≤ b.exponent)

Successful finite decoding transports the complete signed numerical ordering rule.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrder_of_toReal_lt {fmt : FloatFormat} {x y : Model fmt} (hx : x.isFinite = true) (hy : y.isFinite = true) (h : x.toReal < y.toReal) : x.totalOrder y = true

Strict numerical increase of finite binary values implies total ordering.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrder_eq_false_of_toReal_gt {fmt : FloatFormat} {x y : Model fmt} (hx : x.isFinite = true) (hy : y.isFinite = true) (h : y.toReal < x.toReal) : x.totalOrder y = false

Strict numerical decrease of finite binary values fails total ordering.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrder_of_compare_eq_lt {fmt : FloatFormat} {x y : Model fmt} (h : x.compare y = some Ordering.lt) : x.totalOrder y = true

The existing numerical comparator's strict order is respected, including infinities.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrder_eq_false_of_compare_eq_gt {fmt : FloatFormat} {x y : Model fmt} (h : x.compare y = some Ordering.gt) : x.totalOrder y = false

The existing numerical comparator's reversed strict order fails total ordering.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrder_of_toEReal_lt {fmt : FloatFormat} {x y : Model fmt} {a b : EReal} (hx : x.toEReal? = some a) (hy : y.toEReal? = some b) (h : a < b) : x.totalOrder y = true

Total order extends extended-real strict order on non-NaNs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrder_eq_false_of_toEReal_gt {fmt : FloatFormat} {x y : Model fmt} {a b : EReal} (hx : x.toEReal? = some a) (hy : y.toEReal? = some b) (h : b < a) : x.totalOrder y = false

Extended-real strict decrease fails total order on non-NaNs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrder_zero_iff {fmt : FloatFormat} {x y : Model fmt} (hx : x.isZero = true) (hy : y.isZero = true) : x.totalOrder y = (x.signBit || !y.signBit)

Zeros are ordered by their stored signs.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrder_negZero_posZero {fmt : FloatFormat} (hfmt : fmt.supportsSignedZero = true) : (zero fmt true).totalOrder (zero fmt false) = true

In a signed-zero format, negative zero precedes positive zero.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrder_posZero_negZero {fmt : FloatFormat} (hfmt : fmt.supportsSignedZero = true) : (zero fmt false).totalOrder (zero fmt true) = false

In a signed-zero format, positive zero does not precede negative zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrder_nan_number {fmt : FloatFormat} {x y : Model fmt} (hx : x.isNaN = true) (hy : y.isNaN = false) : x.totalOrder y = x.signBit

A NaN precedes a number exactly when its sign bit is negative.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrder_number_nan {fmt : FloatFormat} {x y : Model fmt} (hx : x.isNaN = false) (hy : y.isNaN = true) : x.totalOrder y = !y.signBit

A number precedes a NaN exactly when that NaN has positive sign.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrder_nan_iff {fmt : FloatFormat} {x y : Model fmt} (hx : x.isNaN = true) (hy : y.isNaN = true) : x.totalOrder y = true ↔ x.signBit = true ∧ y.signBit = false ∨ x.signBit = y.signBit ∧ if x.signBit = true then x.isSNaN = false ∧ y.isSNaN = true ∨ x.isSNaN = y.isSNaN ∧ y.fracField ≤ x.fracField else x.isSNaN = true ∧ y.isSNaN = false ∨ x.isSNaN = y.isSNaN ∧ x.fracField ≤ y.fracField

Complete sign, signaling-class, and payload rule for two binary NaNs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrder_posNaN_payload {fmt : FloatFormat} {x y : Model fmt} (hx : x.isNaN = true) (hy : y.isNaN = true) (hsx : x.signBit = false) (hsy : y.signBit = false) (hclass : x.isSNaN = y.isSNaN) : x.totalOrder y = true ↔ x.fracField ≤ y.fracField

Positive NaNs in the same NaN class are ordered by increasing fraction payload.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrder_negNaN_payload {fmt : FloatFormat} {x y : Model fmt} (hx : x.isNaN = true) (hy : y.isNaN = true) (hsx : x.signBit = true) (hsy : y.signBit = true) (hclass : x.isSNaN = y.isSNaN) : x.totalOrder y = true ↔ y.fracField ≤ x.fracField

Negative NaNs in the same NaN class are ordered by decreasing fraction payload.