Total ordering by magnitude

Magnitude comparison is a total preorder on complete data: mutual comparison identifies the absolute data, including NaN signaling status and payload. It agrees with absolute numerical comparison on finite operands. In signed-zero formats, including every IEEE encoding, it is exactly totalOrder (abs x) (abs y), as specified by IEEE 754-2019 §5.7.2.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.dyadic_toRat_clearSign (d : Numerics.Dyadic) : { negative := false, significand := d.significand, exponent := d.exponent }.toRat = |d.toRat|

Clearing a dyadic's sign computes the absolute value of its exact rational denotation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrderMag_finite_iff (a b : Numerics.Dyadic) : (finite a).totalOrderMag (finite b) = true ↔ |a.toRat| < |b.toRat| ∨ |a.toRat| = |b.toRat| ∧ a.exponent ≤ b.exponent

Finite magnitude order compares absolute numerical values, then their exponents.

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

A strict increase in absolute numerical value gives magnitude ordering.

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

A strict decrease in absolute numerical value fails magnitude ordering.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrderMag_nan_iff (s t q r : Bool) (p n : ℕ) : (nan s q p).totalOrderMag (nan t r n) = true ↔ q = true ∧ r = false ∨ q = r ∧ p ≤ n

NaN magnitudes place signaling before quiet, with increasing payloads within each class.

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

Magnitude comparison uses the same exact order for every binary descriptor.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrderMag_eq_totalOrder_abs {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.supportsSignedZero = true) : x.totalOrderMag y = x.abs.totalOrder y.abs

IEEE's definition using encoded absolute value holds for every signed-zero format.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrderMag_eq_totalOrder_abs_of_ieee {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.encoding = FloatFormat.Encoding.ieee) : x.totalOrderMag y = x.abs.totalOrder y.abs

The encoded-absolute-value definition holds for every IEEE encoding, with arbitrary bias.

@[simp]

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

Magnitude order is reflexive on every binary datum.

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

Magnitude order is total, including NaN magnitudes.

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

Magnitude order is transitive for every descriptor.

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

Mutual magnitude comparison identifies absolute complete data, including NaN metadata.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrderMag_both_iff_abs_eq {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.supportsSignedZero = true) : x.totalOrderMag y = true ∧ y.totalOrderMag x = true ↔ x.abs = y.abs

For signed-zero formats, mutual magnitude comparison identifies absolute encoded words.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrderMag_iff_of_toDyadic? {fmt : FloatFormat} {x y : Model fmt} {a b : Numerics.Dyadic} (hx : x.toDyadic? = some a) (hy : y.toDyadic? = some b) : x.totalOrderMag y = true ↔ |a.toRat| < |b.toRat| ∨ |a.toRat| = |b.toRat| ∧ a.exponent ≤ b.exponent

The full finite magnitude rule is uniform in format width, bias, and encoding policy.

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

Strict increase in absolute real value gives magnitude ordering for finite operands.

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

Strict decrease in absolute real value fails magnitude ordering for finite operands.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrderMag_zero {fmt : FloatFormat} {x y : Model fmt} (hx : x.isZero = true) (hy : y.isZero = true) : x.totalOrderMag y = true

All zero signs have the same magnitude.

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

A NaN magnitude is strictly above every numerical magnitude, regardless of its sign.

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

Every numerical magnitude precedes every NaN magnitude.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrderMag_nan_iff {fmt : FloatFormat} {x y : Model fmt} (hx : x.isNaN = true) (hy : y.isNaN = true) : x.totalOrderMag y = true ↔ x.isSNaN = true ∧ y.isSNaN = false ∨ x.isSNaN = y.isSNaN ∧ x.fracField ≤ y.fracField

NaN magnitude order ignores signs and compares signaling class before payload.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrderMag_nan_both_iff {fmt : FloatFormat} {x y : Model fmt} (hx : x.isNaN = true) (hy : y.isNaN = true) : x.totalOrderMag y = true ∧ y.totalOrderMag x = true ↔ x.isSNaN = y.isSNaN ∧ x.fracField = y.fracField

Magnitude equality of NaNs retains both signaling class and complete fraction payload.