Total-order laws and IEEE decimal tie rules

Key injectivity establishes antisymmetry for full datums. The finite and NaN theorems identify the numerical, cohort, sign and payload ordering rules; the order laws alone would not establish agreement with those rules.

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.orderKey_injective : Function.Injective orderKey

The ordering key loses no datum information, including NaN payloads or zero quanta.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.totalOrder_self (x : Datum) : x.totalOrder x = true

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.totalOrder_trans {x y z : Datum} (hxy : x.totalOrder y = true) (hyz : y.totalOrder z = true) : x.totalOrder z = true

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.totalOrder_total (x y : Datum) : x.totalOrder y = true ∨ y.totalOrder x = true

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.totalOrder_antisymm_iff (x y : Datum) : x.totalOrder y = true ∧ y.totalOrder x = true ↔ x = y

Both directions hold precisely when the complete datums are identical.

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.totalOrder_positive_finite_iff (c d : ℕ) (q r : ℤ) : (finite false c q).totalOrder (finite false d r) = true ↔ finiteValue false c q < finiteValue false d r ∨ finiteValue false c q = finiteValue false d r ∧ q ≤ r

On positive finite datums, numerical value precedes increasing quantum.

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.totalOrder_negative_finite_iff (c d : ℕ) (q r : ℤ) : (finite true c q).totalOrder (finite true d r) = true ↔ finiteValue true c q < finiteValue true d r ∨ finiteValue true c q = finiteValue true d r ∧ r ≤ q

On negative finite datums, increasing numerical value precedes decreasing quantum.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.totalOrder_negative_positive (c d : ℕ) (q r : ℤ) : (finite true c q).totalOrder (finite false d r) = true

Negative finite datums precede positive ones, including the two zero signs.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.totalOrder_positive_negative (c d : ℕ) (q r : ℤ) : (finite false c q).totalOrder (finite true d r) = false

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.totalOrder_zero_iff (s : Bool) (q r : ℤ) : (finite s 0 q).totalOrder (finite s 0 r) = true ↔ if s = true then r ≤ q else q ≤ r

The quantum tie rule applies to signed zero as well as nonzero cohorts.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.totalOrder_positive_signaling_quiet (p k : ℕ) : (nan false true p).totalOrder (nan false false k) = true

Positive signaling NaNs precede quiet NaNs regardless of payload.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.totalOrder_negative_quiet_signaling (p k : ℕ) : (nan true false p).totalOrder (nan true true k) = true

Negative quiet NaNs precede signaling NaNs regardless of payload.

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.totalOrder_nan_payload_iff (s t : Bool) (p k : ℕ) : (nan s t p).totalOrder (nan s t k) = true ↔ if s = true then k ≤ p else p ≤ k

This implementation's equal-kind NaN payload order reverses with the sign. IEEE 754-2019 §5.10(d)(5)(iii) permits this choice.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.totalOrder_negative_positive_nan (t u : Bool) (p k : ℕ) : (nan true t p).totalOrder (nan false u k) = true

Every negative NaN precedes every positive NaN, irrespective of kind or payload.

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.totalOrder_negative_nan_numeric (t : Bool) (p : ℕ) (x : Datum) (hx : x.isNaN = false) : (nan true t p).totalOrder x = true

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.totalOrder_numeric_positive_nan (t : Bool) (p : ℕ) (x : Datum) (hx : x.isNaN = false) : x.totalOrder (nan false t p) = true

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.totalOrder_negative_infinity_finite (s : Bool) (c : ℕ) (q : ℤ) : (infinity true).totalOrder (finite s c q) = true

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.totalOrder_finite_positive_infinity (s : Bool) (c : ℕ) (q : ℤ) : (finite s c q).totalOrder (infinity false) = true

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.totalOrderMag_self (x : Datum) : x.totalOrderMag x = true

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.totalOrderMag_trans {x y z : Datum} (hxy : x.totalOrderMag y = true) (hyz : y.totalOrderMag z = true) : x.totalOrderMag z = true

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.totalOrderMag_total (x y : Datum) : x.totalOrderMag y = true ∨ y.totalOrderMag x = true

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.totalOrderMag_antisymm_iff (x y : Datum) : x.totalOrderMag y = true ∧ y.totalOrderMag x = true ↔ x.abs = y.abs

Magnitude ordering identifies precisely datums differing at most in sign.