Correctness of exact IEEE decoding

Binary arithmetic proofs need an exact value that is cheaper and more concrete than a real number. toDyadic? decodes every finite encoding to that value and rejects exceptional encodings. Conventional IEEE descriptors reuse the established unpacked model; configurable descriptors follow their declared bias and exceptional-value policy.

The central theorem proves that executable field decoding agrees with Lean's logical floating model. Later lemmas recover finiteness, sign, zero, and sign-toggle facts from successful decoding. This direction is deliberate: optimized kernels may inspect fields, while their proofs can immediately move to one canonical exact dyadic semantics.

Complete-format decoding

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.toDyadic? {fmt : FloatFormat} (x : Model fmt) : Option Numerics.Dyadic

Decode a finite Model into an exact dyadic under its complete format descriptor.

The conventional IEEE case delegates to the established decoder. Other encodings use their declared exponent bias and exceptional-value policy directly.

def FloatLib.Floats.Formats.BinaryInterchange.Model.toRat? {fmt : FloatFormat} (x : Model fmt) : Option ℚ

Exact rational value of a finite executable float; returns none for NaN or infinity.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ieeeToDyadic?_eq_unpackedToDyadic?_toModel {fmt : FloatFormat} (x : Model fmt) : x.ieeeToDyadic? = unpackedToDyadic? x.toModel

The IEEE field decoder agrees with Lean's logical IEEE model.

The theorem is width-generic. Both sides use the conventional IEEE interpretation of the layout; the descriptor's custom bias and exceptional-value policy are handled separately by toDyadic?.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toModel_eq_finite_of_ieeeToDyadic?_eq_some {fmt : FloatFormat} (x : Model fmt) (sign : Bool) (mantissa : ℕ) (exponent : ℤ) (hmantissa : mantissa ≠ 0) (hdecode : x.ieeeToDyadic? = some { negative := sign, significand := mantissa, exponent := exponent }) : x.toModel = Float.Model.UnpackedFloat.finite (modelSign sign) mantissa exponent ⋯

A nonzero successful dyadic decode determines the corresponding finite logical model value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toModel_eq_zero_of_ieeeToDyadic?_eq_some {fmt : FloatFormat} (x : Model fmt) (sign : Bool) (exponent : ℤ) (hdecode : x.ieeeToDyadic? = some { negative := sign, significand := 0, exponent := exponent }) : x.toModel = Float.Model.UnpackedFloat.zero (modelSign sign)

A zero dyadic decode determines the corresponding signed model zero.

Decoding and finiteness

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_eq_false_of_ieeeToDyadic?_some {fmt : FloatFormat} {x : Model fmt} {d : Numerics.Dyadic} (hx : x.ieeeToDyadic? = some d) : IEEE.isNaN x = false

A successful dyadic decode rules out NaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isInf_eq_false_of_ieeeToDyadic?_some {fmt : FloatFormat} {x : Model fmt} {d : Numerics.Dyadic} (hx : x.ieeeToDyadic? = some d) : IEEE.isInf x = false

A successful dyadic decode rules out infinity.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ieeeToDyadic?_toggleSign_of_ieeeToDyadic?_some {fmt : FloatFormat} (x : Model fmt) {d : Numerics.Dyadic} (hx : x.ieeeToDyadic? = some d) : x.toggleSign.ieeeToDyadic? = some { negative := !d.negative, significand := d.significand, exponent := d.exponent }

IEEE decoding preserves magnitude and exponent when the storage sign bit is toggled.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.sign_eq_signBit_of_ieeeToDyadic?_some {fmt : FloatFormat} {x : Model fmt} {d : Numerics.Dyadic} (hx : x.ieeeToDyadic? = some d) : d.negative = x.signBit

IEEE dyadic decoding preserves the stored sign bit.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isZero_eq_true_of_ieeeToDyadic?_some_of_mant_eq_zero {fmt : FloatFormat} {x : Model fmt} {d : Numerics.Dyadic} (hx : x.ieeeToDyadic? = some d) (hmant : d.significand = 0) : IEEE.isZero x = true

A decoded dyadic has zero mantissa only when the source is an IEEE signed zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_eq_true_of_ieeeToDyadic?_some {fmt : FloatFormat} {x : Model fmt} {d : Numerics.Dyadic} (hx : x.ieeeToDyadic? = some d) : IEEE.isFinite x = true

A successful dyadic decode certifies that the source bit pattern is finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.exists_ieeeToDyadic?_of_not_isNaN_not_isInf {fmt : FloatFormat} {x : Model fmt} (hnan : IEEE.isNaN x = false) (hinf : IEEE.isInf x = false) : ∃ (d : Numerics.Dyadic), x.ieeeToDyadic? = some d

Every bit pattern that is neither NaN nor infinity has an exact dyadic decode.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.exists_ieeeToDyadic?_of_isFinite {fmt : FloatFormat} {x : Model fmt} (hx : IEEE.isFinite x = true) : ∃ (d : Numerics.Dyadic), x.ieeeToDyadic? = some d

Every bit pattern classified as finite by IEEE rules has an exact dyadic decode.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ieeeToDyadic?_isSome_eq_isFinite {fmt : FloatFormat} (x : Model fmt) : x.ieeeToDyadic?.isSome = IEEE.isFinite x

IEEE dyadic decoding succeeds exactly on bit patterns classified as finite by IEEE rules.