Complete exact data determine binary encodings

Finite decoding is injective because subnormal significands lie below the implicit leading bit, whereas normal significands include it. Within either class the exact dyadic recovers the fields. For exceptional values, the encoding policy and the stored sign and fraction complete the reconstruction. This injectivity transfers antisymmetry from complete exact data to words.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.eq_of_signBit_expField_fracField_eq {fmt : FloatFormat} {x y : Model fmt} (hsign : x.signBit = y.signBit) (hexponent : x.expField = y.expField) (hfraction : x.fracField = y.fracField) : x = y

Equality of all interchange fields determines the stored word.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.eq_of_toDyadic?_eq_some {fmt : FloatFormat} {x y : Model fmt} {d : Numerics.Dyadic} (hx : x.toDyadic? = some d) (hy : y.toDyadic? = some d) : x = y

Two words decoding to the same complete dyadic have identical encodings.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.exactValue_eq_nan_of_isNaN {fmt : FloatFormat} {x : Model fmt} (hx : x.isNaN = true) : x.exactValue = ExactValue.nan x.signBit x.isSNaN x.fracField

Classification as NaN exposes all the exact metadata used by total ordering.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.exactValue_eq_infinity_of_isInf {fmt : FloatFormat} {x : Model fmt} (hx : x.isInf = true) : x.exactValue = ExactValue.infinity x.signBit

Infinity decoding retains exactly its sign.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.exactValue_injective {fmt : FloatFormat} : Function.Injective exactValue

Complete exact interpretation is injective for every binary format descriptor.