Complete-format decoding and classification

The exact dyadic decoder determines finiteness, sign, and zero status for arithmetic proofs. Successful decoding is equivalent to finiteness, and the decoded dyadic recovers the encoding's sign and zero status. The same statements cover IEEE encodings, finite-only encodings, and finite encodings with an unsigned-zero policy.

NaN selection is handled here as classification rather than arithmetic. That keeps exceptional control flow out of the exact finite kernels and gives unary, binary, and ternary operations one shared account of when chooseNaN can return none.

Complete-format decoding theorems

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

Exact decoding succeeds precisely for values that are finite under the complete format.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.exists_toDyadic?_of_isFinite {fmt : FloatFormat} {x : Model fmt} (hfinite : x.isFinite = true) : ∃ (d : Numerics.Dyadic), x.toDyadic? = some d

Every finite value has an exact dyadic decoding.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.finiteDyadic {fmt : FloatFormat} (x : Model fmt) (hfinite : x.isFinite = true) : Numerics.Dyadic

Extract the exact dyadic represented by a value already proved finite.

Complete binary descriptors make this operation total: toDyadic? succeeds exactly on finite encodings. The proof argument is erased, and extraction requires no default dyadic.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.finiteDyadic_eq_of_toDyadic {fmt : FloatFormat} {x : Model fmt} {exact : Numerics.Dyadic} (hfinite : x.isFinite = true) (hdecode : x.toDyadic? = some exact) : x.finiteDyadic hfinite = exact

Proof-guided finite extraction returns the dyadic produced by exact decoding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toDyadic?_ieee_eq_model (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (x : Model fmt) : x.toDyadic? = unpackedToDyadic? x.toModel

For a conventional IEEE descriptor, policy-aware decoding agrees with Lean's model.

Complete-format classification

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_eq_true_of_isZero_eq_true {fmt : FloatFormat} (x : Model fmt) (hx : x.isZero = true) : x.isFinite = true

Every value denoting zero is finite under the same complete format.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_eq_false_of_isFinite_eq_true {fmt : FloatFormat} (x : Model fmt) (hx : x.isFinite = true) : x.isNaN = false

Finite values are not NaNs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_eq_true_of_isNaN_eq_false_of_isInf_eq_false {fmt : FloatFormat} (x : Model fmt) (hnan : x.isNaN = false) (hinf : x.isInf = false) : x.isFinite = true

A non-NaN, non-infinite bit pattern is finite.

NaN-selection classification

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.chooseNaN1_eq_none_iff {fmt : FloatFormat} (x : Model fmt) : x.chooseNaN1 = none ↔ x.isNaN = false

Unary NaN selection returns none exactly when its operand is not a NaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.chooseNaN2_eq_none_iff {fmt : FloatFormat} (x y : Model fmt) : x.chooseNaN2 y = none ↔ x.isNaN = false ∧ y.isNaN = false

Binary NaN selection returns none exactly when neither operand is a NaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.chooseNaN3_eq_none_iff {fmt : FloatFormat} (x y z : Model fmt) : x.chooseNaN3 y z = none ↔ x.isNaN = false ∧ y.isNaN = false ∧ z.isNaN = false

Ternary NaN selection returns none exactly when none of its operands is a NaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_eq_false_of_encoding_finite {fmt : FloatFormat} (hfmt : fmt.encoding = FloatFormat.Encoding.finite) (x : Model fmt) : x.isNaN = false

A finite-only encoding contains no NaN bit pattern.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_eq_true_of_encoding_finite {fmt : FloatFormat} (hfmt : fmt.encoding = FloatFormat.Encoding.finite) (x : Model fmt) : x.isFinite = true

Every bit pattern of a finite-only encoding denotes a finite value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isInf_eq_false_of_encoding_ne_ieee {fmt : FloatFormat} (hfmt : fmt.encoding ≠ FloatFormat.Encoding.ieee) (x : Model fmt) : x.isInf = false

Every non-IEEE encoding in this library excludes infinity.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isZero_eq_true_iff_of_encoding_finiteUnsignedZero {fmt : FloatFormat} (hfmt : fmt.encoding = FloatFormat.Encoding.finiteUnsignedZero) (x : Model fmt) : x.isZero = true ↔ x.bits = 0

In FNUZ, a value is zero exactly when all stored bits are zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.signMask_isNaN_of_encoding_finiteUnsignedZero {fmt : FloatFormat} (hfmt : fmt.encoding = FloatFormat.Encoding.finiteUnsignedZero) : (ofBits fmt.signMask).isNaN = true

In FNUZ, the would-be negative-zero word is NaN rather than a second zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_eq_false_of_isNaN {fmt : FloatFormat} {x : Model fmt} (hx : x.isNaN = true) : x.isFinite = false

A NaN bit pattern is not finite under the same format descriptor.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toDyadic?_eq_none_of_isNaN {fmt : FloatFormat} {x : Model fmt} (hx : x.isNaN = true) : x.toDyadic? = none

A NaN bit pattern cannot be decoded as a finite dyadic.

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

Successful exact decoding excludes the format's NaN encodings.

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

Successful exact decoding characterizes a finite stored value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isSNaN_eq_false_of_toDyadic?_some {fmt : FloatFormat} {x : Model fmt} {d : Numerics.Dyadic} (hx : x.toDyadic? = some d) : x.isSNaN = false

Successful exact decoding excludes signaling NaNs.

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

Successful exact decoding excludes infinity.

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

Complete-format dyadic decoding preserves the stored sign bit.

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

A complete-format dyadic decode has zero mantissa only for a policy zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toDyadic?_eq_zero_of_isZero_eq_true {fmt : FloatFormat} (x : Model fmt) (hx : x.isZero = true) : x.toDyadic? = some { negative := x.signBit, significand := 0, exponent := 0 }

A zero value decodes to the zero dyadic, preserving its meaningful sign bit.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isZero_eq_beq_zero_of_toDyadic?_some {fmt : FloatFormat} {x : Model fmt} {d : Numerics.Dyadic} (hx : x.toDyadic? = some d) : x.isZero = (d.significand == 0)

For an exactly decoded finite value, zero classification is the significand-zero test.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isZero_zero (fmt : FloatFormat) (sign : Bool) : (zero fmt sign).isZero = true

The policy-aware zero constructor always denotes zero.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_zero (fmt : FloatFormat) (sign : Bool) : (zero fmt sign).isNaN = false

The policy-aware zero constructor is never a NaN.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toDyadic?_zero (fmt : FloatFormat) (sign : Bool) : (zero fmt sign).toDyadic? = some { negative := (zero fmt sign).signBit, significand := 0, exponent := 0 }

The policy-aware zero constructor decodes to the exact zero dyadic.