Total ordering of complete exact representations

The key used by ExactValue.totalOrder is injective, so its order is antisymmetric on complete data, not just on numerical denotations. Finite comparison agrees with rational order and breaks numerical ties by sign and exponent. Separate theorems give the NaN class and payload rules. Magnitude order is a total preorder: mutual comparison identifies complete data after clearing their signs, including NaN class and payload.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.dyadic_eq_of_toRat_eq_of_negative_eq_of_exponent_eq {a b : Numerics.Dyadic} (hvalue : a.toRat = b.toRat) (hsign : a.negative = b.negative) (hexponent : a.exponent = b.exponent) : a = b

At a fixed sign and exponent, the exact rational determines the complete dyadic.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrderKey_injective : Function.Injective totalOrderKey

Equality of ordering coordinates preserves every field of a complete exact value.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrder_eq_true_iff (x y : ExactValue) : x.totalOrder y = true ↔ x.totalOrderKey ≤ y.totalOrderKey

The executable Boolean is precisely the mathematical order on exact coordinates.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrder_refl (x : ExactValue) : x.totalOrder x = true

Every complete datum precedes itself, including signaling NaNs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrder_total (x y : ExactValue) : x.totalOrder y = true ∨ y.totalOrder x = true

Any two complete data are comparable.

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

Exact total ordering is transitive, including all exceptional-value classes.

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

Mutual ordering identifies the complete datum, including NaN sign, class, and payload.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrder_both_iff (x y : ExactValue) : x.totalOrder y = true ∧ y.totalOrder x = true ↔ x = y

Mutual comparison is exactly equality of complete representations.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrder_finite_iff (a b : Numerics.Dyadic) : (finite a).totalOrder (finite b) = 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)

Finite total order agrees with numerical order. Ties place negative signs first, then order exponents upward for positive values and downward for negative values.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrder_finite_of_lt {a b : Numerics.Dyadic} (h : a.toRat < b.toRat) : (finite a).totalOrder (finite b) = true

Strict numerical increase always gives total ordering.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrder_finite_eq_false_of_gt {a b : Numerics.Dyadic} (h : b.toRat < a.toRat) : (finite a).totalOrder (finite b) = false

Strict numerical decrease always fails total ordering.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrder_finite_of_value_eq {a b : Numerics.Dyadic} (hvalue : a.toRat = b.toRat) (hsign : a.negative = b.negative) : (finite a).totalOrder (finite b) = true ↔ if a.negative = true then b.exponent ≤ a.exponent else a.exponent ≤ b.exponent

For equal numerical values of the same sign, exponents break the tie.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrder_negZero_posZero (exponent : ℤ) : (finite { negative := true, significand := 0, exponent := exponent }).totalOrder (finite { negative := false, significand := 0, exponent := exponent }) = true

Negative zero precedes positive zero.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrder_posZero_negZero (exponent : ℤ) : (finite { negative := false, significand := 0, exponent := exponent }).totalOrder (finite { negative := true, significand := 0, exponent := exponent }) = false

Positive zero does not precede negative zero.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrder_negInf_finite (d : Numerics.Dyadic) : (infinity true).totalOrder (finite d) = true

Every finite value lies strictly above negative infinity.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrder_finite_negInf (d : Numerics.Dyadic) : (finite d).totalOrder (infinity true) = false

A finite value cannot precede negative infinity.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrder_finite_posInf (d : Numerics.Dyadic) : (finite d).totalOrder (infinity false) = true

Every finite value lies strictly below positive infinity.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrder_posInf_finite (d : Numerics.Dyadic) : (infinity false).totalOrder (finite d) = false

Positive infinity cannot precede a finite value.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrder_infinity (s t : Bool) : (infinity s).totalOrder (infinity t) = (s || !t)

Signed infinities follow their numerical order.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrder_nan_finite (s q : Bool) (p : ℕ) (d : Numerics.Dyadic) : (nan s q p).totalOrder (finite d) = s

A NaN precedes every finite number exactly when the NaN has negative sign.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrder_finite_nan (d : Numerics.Dyadic) (s q : Bool) (p : ℕ) : (finite d).totalOrder (nan s q p) = !s

Every finite number precedes a NaN exactly when that NaN has positive sign.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrder_nan_infinity (s q : Bool) (p : ℕ) (t : Bool) : (nan s q p).totalOrder (infinity t) = s

NaN placement relative to infinity depends only on the NaN sign.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrder_infinity_nan (t s q : Bool) (p : ℕ) : (infinity t).totalOrder (nan s q p) = !s

Infinity precedes precisely the positive NaNs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrder_nan_iff (s t q r : Bool) (p n : ℕ) : (nan s q p).totalOrder (nan t r n) = true ↔ s = true ∧ t = false ∨ s = t ∧ if s = true then q = false ∧ r = true ∨ q = r ∧ n ≤ p else q = true ∧ r = false ∨ q = r ∧ p ≤ n

Complete NaN rule: sign first, then signaling before quiet for positive NaNs and the reverse for negative NaNs, then FloatLib's ascending/descending payload convention.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrder_posNaN_payload (q : Bool) (p n : ℕ) : (nan false q p).totalOrder (nan false q n) = true ↔ p ≤ n

Positive NaN payloads increase within either NaN class.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrder_negNaN_payload (q : Bool) (p n : ℕ) : (nan true q p).totalOrder (nan true q n) = true ↔ n ≤ p

Negative NaN payloads decrease within either NaN class.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.abs_abs (x : ExactValue) : x.abs.abs = x.abs

Clearing a sign twice is the same as clearing it once.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrderMag_refl (x : ExactValue) : x.totalOrderMag x = true

Magnitude order is reflexive even on NaNs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrderMag_total (x y : ExactValue) : x.totalOrderMag y = true ∨ y.totalOrderMag x = true

Every pair of magnitudes is comparable.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrderMag_trans {x y z : ExactValue} (hxy : x.totalOrderMag y = true) (hyz : y.totalOrderMag z = true) : x.totalOrderMag z = true

Magnitude ordering is transitive.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrderMag_both_iff (x y : ExactValue) : x.totalOrderMag y = true ∧ y.totalOrderMag x = true ↔ x.abs = y.abs

Mutual magnitude ordering identifies absolute data, retaining NaN class and payload.