Uniqueness of finite binary representations

The decoded exponent is the canonical exponent of every nonzero finite value. This connects numerical conversion theorems to representation round trips; signed zero is handled separately because real numbers forget its sign.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.cexp_toDyadic? {fmt : FloatFormat} {x : Model fmt} {d : Numerics.Dyadic} (hd : x.toDyadic? = some d) (hm : d.significand ≠ 0) : Flocq.cexp Numerics.binaryRadix (fexpOf fmt) d.toReal = d.exponent

A nonzero decoded dyadic already uses the format's canonical exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toDyadic?_exponent_eq_of_toReal_eq {fmt : FloatFormat} {x y : Model fmt} {dx dy : Numerics.Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) (hx0 : dx.significand ≠ 0) (hy0 : dy.significand ≠ 0) (hvalue : x.toReal = y.toReal) : dx.exponent = dy.exponent

Equal nonzero numerical values have the same canonical decoded exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Dyadic.toReal_eq_zero_iff (d : Numerics.Dyadic) : d.toReal = 0 ↔ d.significand = 0

A dyadic denotes zero exactly when its unsigned coefficient is zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.eq_of_toReal_eq_of_nonzero {fmt : FloatFormat} {x y : Model fmt} (hx : x.isFinite = true) (hy : y.isFinite = true) (hvalue : x.toReal = y.toReal) (hzero : x.toReal ≠ 0) : x = y

Equal nonzero finite real values determine the complete binary word.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicWithRounding_toDyadic?_of_nonzero {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (mode : IEEERoundingMode) {x : Model fmt} {d : Numerics.Dyadic} (hd : x.toDyadic? = some d) (hm : d.significand ≠ 0) : roundDyadicWithRounding fmt mode d = x

In a conventional IEEE format, rounding a decoded nonzero value restores its word.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicWithRounding_zero (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (mode : IEEERoundingMode) (negative : Bool) (exponent : ℤ) : roundDyadicWithRounding fmt mode { negative := negative, significand := 0, exponent := exponent } = zero fmt negative

In a conventional IEEE format, rounding an exact zero preserves its sign.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicWithRounding_toDyadic? {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (mode : IEEERoundingMode) {x : Model fmt} {d : Numerics.Dyadic} (hd : x.toDyadic? = some d) : roundDyadicWithRounding fmt mode d = x

In a conventional IEEE format, rounding a decoded finite dyadic restores its complete word.