Configured total-order refinement

Packing and decoding preserve both predicates exactly. Order laws and numerical, zero, and NaN rules are transported from the descriptor model, independently of the chosen runtime carrier. Mutual magnitude comparison identifies absolute exact values, including NaN metadata; opposite signs can tie.

theorem FloatLib.Floats.ExecFloat.Binary.totalOrder_eq_model {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x y : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : totalOrder x y = (toModel x).totalOrder (toModel y)

Configured total ordering is exactly the descriptor-model predicate.

theorem FloatLib.Floats.ExecFloat.Binary.totalOrderMag_eq_model {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x y : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : totalOrderMag x y = (toModel x).totalOrderMag (toModel y)

Configured magnitude ordering is exactly the descriptor-model predicate.

theorem FloatLib.Floats.ExecFloat.Binary.totalOrder_eq_exactValue {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x y : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : totalOrder x y = (exactValue x).totalOrder (exactValue y)

The configured predicate uses the shared complete exact-value order.

theorem FloatLib.Floats.ExecFloat.Binary.totalOrderMag_eq_exactValue {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x y : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : totalOrderMag x y = (exactValue x).totalOrderMag (exactValue y)

The configured magnitude predicate uses the shared exact magnitude order.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.totalOrder_ofModel {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x y : Formats.BinaryInterchange.Model format) : totalOrder (ofModel x) (ofModel y) = x.totalOrder y

Packing two models preserves their total-order comparison.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.totalOrderMag_ofModel {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x y : Formats.BinaryInterchange.Model format) : totalOrderMag (ofModel x) (ofModel y) = x.totalOrderMag y

Packing two models preserves their magnitude comparison.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.totalOrder_refl {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : totalOrder x x = true

Every configured datum precedes itself, including signaling NaNs.

theorem FloatLib.Floats.ExecFloat.Binary.totalOrder_total {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x y : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : totalOrder x y = true ∨ totalOrder y x = true

Configured total ordering compares every pair of values.

theorem FloatLib.Floats.ExecFloat.Binary.totalOrder_trans {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] {x y z : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)} (hxy : totalOrder x y = true) (hyz : totalOrder y z = true) : totalOrder x z = true

Configured total ordering is transitive.

theorem FloatLib.Floats.ExecFloat.Binary.totalOrder_antisymm {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] {x y : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)} (hxy : totalOrder x y = true) (hyx : totalOrder y x = true) : x = y

Mutual total ordering identifies the configured value, including its complete encoding.

theorem FloatLib.Floats.ExecFloat.Binary.totalOrder_both_iff {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x y : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : totalOrder x y = true ∧ totalOrder y x = true ↔ x = y

Mutual total comparison is equivalent to equality for every configured storage plan.

theorem FloatLib.Floats.ExecFloat.Binary.totalOrder_of_compare_eq_lt {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] {x y : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)} (h : (toModel x).compare (toModel y) = some Ordering.lt) : totalOrder x y = true

Strict model numerical comparison is respected by configured total order.

theorem FloatLib.Floats.ExecFloat.Binary.totalOrder_eq_false_of_compare_eq_gt {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] {x y : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)} (h : (toModel x).compare (toModel y) = some Ordering.gt) : totalOrder x y = false

Reversed strict numerical comparison fails configured total order.

theorem FloatLib.Floats.ExecFloat.Binary.totalOrder_zero_iff {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] {x y : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)} (hx : isZero x = true) (hy : isZero y = true) : totalOrder x y = (signBit x || !signBit y)

Configured zero ordering depends only on the stored sign flags.

theorem FloatLib.Floats.ExecFloat.Binary.totalOrder_nan_iff {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] {x y : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)} (hx : isNaN x = true) (hy : isNaN y = true) : totalOrder x y = true ↔ signBit x = true ∧ signBit y = false ∨ signBit x = signBit y ∧ if signBit x = true then isSignalingNaN x = false ∧ isSignalingNaN y = true ∨ isSignalingNaN x = isSignalingNaN y ∧ (toModel y).fracField ≤ (toModel x).fracField else isSignalingNaN x = true ∧ isSignalingNaN y = false ∨ isSignalingNaN x = isSignalingNaN y ∧ (toModel x).fracField ≤ (toModel y).fracField

The configured NaN rule preserves sign, signaling class, and full fraction payload.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.totalOrderMag_refl {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : totalOrderMag x x = true

Magnitude comparison is reflexive on every configured value.

theorem FloatLib.Floats.ExecFloat.Binary.totalOrderMag_total {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x y : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : totalOrderMag x y = true ∨ totalOrderMag y x = true

Magnitude comparison is total on configured values, including NaNs.

theorem FloatLib.Floats.ExecFloat.Binary.totalOrderMag_trans {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] {x y z : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)} (hxy : totalOrderMag x y = true) (hyz : totalOrderMag y z = true) : totalOrderMag x z = true

Configured magnitude comparison is transitive.

theorem FloatLib.Floats.ExecFloat.Binary.totalOrderMag_both_iff_exactValue_abs_eq {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x y : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : totalOrderMag x y = true ∧ totalOrderMag y x = true ↔ (exactValue x).abs = (exactValue y).abs

Mutual configured magnitude comparison identifies absolute exact data.

theorem FloatLib.Floats.ExecFloat.Binary.totalOrderMag_eq_totalOrder_model_abs {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x y : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (hformat : format.supportsSignedZero = true) : totalOrderMag x y = (toModel x).abs.totalOrder (toModel y).abs

In a signed-zero format, magnitude ordering agrees with model absolute-value ordering.

theorem FloatLib.Floats.ExecFloat.Binary.totalOrderMag_zero {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] {x y : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)} (hx : isZero x = true) (hy : isZero y = true) : totalOrderMag x y = true

All configured zeros tie under magnitude comparison.

theorem FloatLib.Floats.ExecFloat.Binary.totalOrderMag_nan_iff {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] {x y : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)} (hx : isNaN x = true) (hy : isNaN y = true) : totalOrderMag x y = true ↔ isSignalingNaN x = true ∧ isSignalingNaN y = false ∨ isSignalingNaN x = isSignalingNaN y ∧ (toModel x).fracField ≤ (toModel y).fracField

Configured NaN magnitudes compare signaling class, then increasing fraction payload.