The ten binary classes

classify_eq_iff characterizes every result by the existing descriptor predicates. The signed numerical classes retain the stored sign; the two NaN classes deliberately ignore sign and payload. The result type is shared with decimal classification.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.classify_eq_iff {fmt : FloatFormat} (x : Model fmt) (c : Numerics.IEEEClass) : x.classify = c ↔ match c with | Numerics.IEEEClass.signalingNaN => x.isSNaN = true | Numerics.IEEEClass.quietNaN => x.isQNaN = true | Numerics.IEEEClass.negativeInfinity => x.isInf = true ∧ x.signBit = true | Numerics.IEEEClass.positiveInfinity => x.isInf = true ∧ x.signBit = false | Numerics.IEEEClass.negativeZero => x.isZero = true ∧ x.signBit = true | Numerics.IEEEClass.positiveZero => x.isZero = true ∧ x.signBit = false | Numerics.IEEEClass.negativeSubnormal => x.isSubnormal = true ∧ x.signBit = true | Numerics.IEEEClass.positiveSubnormal => x.isSubnormal = true ∧ x.signBit = false | Numerics.IEEEClass.negativeNormal => x.isNormal = true ∧ x.signBit = true | Numerics.IEEEClass.positiveNormal => x.isNormal = true ∧ x.signBit = false

Complete characterization of all ten mutually exclusive classification results.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.classify_eq_signalingNaN_iff {fmt : FloatFormat} (x : Model fmt) : x.classify = Numerics.IEEEClass.signalingNaN ↔ x.isSNaN = true

Classification as signaling NaN is exactly the existing signaling predicate.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.classify_eq_quietNaN_iff {fmt : FloatFormat} (x : Model fmt) : x.classify = Numerics.IEEEClass.quietNaN ↔ x.isQNaN = true

Classification as quiet NaN is exactly the existing quiet-NaN predicate.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.classify_eq_negativeInfinity_iff {fmt : FloatFormat} (x : Model fmt) : x.classify = Numerics.IEEEClass.negativeInfinity ↔ x.isInf = true ∧ x.signBit = true

Negative infinity is infinity with the sign bit set.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.classify_eq_positiveInfinity_iff {fmt : FloatFormat} (x : Model fmt) : x.classify = Numerics.IEEEClass.positiveInfinity ↔ x.isInf = true ∧ x.signBit = false

Positive infinity is infinity with the sign bit clear.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.classify_eq_negativeZero_iff {fmt : FloatFormat} (x : Model fmt) : x.classify = Numerics.IEEEClass.negativeZero ↔ x.isZero = true ∧ x.signBit = true

Negative zero is a policy zero with the sign bit set; FNUZ has no such value.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.classify_eq_positiveZero_iff {fmt : FloatFormat} (x : Model fmt) : x.classify = Numerics.IEEEClass.positiveZero ↔ x.isZero = true ∧ x.signBit = false

Positive zero is a policy zero with the sign bit clear.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.classify_eq_negativeSubnormal_iff {fmt : FloatFormat} (x : Model fmt) : x.classify = Numerics.IEEEClass.negativeSubnormal ↔ x.isSubnormal = true ∧ x.signBit = true

Negative subnormal classification retains the stored negative sign.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.classify_eq_positiveSubnormal_iff {fmt : FloatFormat} (x : Model fmt) : x.classify = Numerics.IEEEClass.positiveSubnormal ↔ x.isSubnormal = true ∧ x.signBit = false

Positive subnormal classification retains the stored positive sign.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.classify_eq_negativeNormal_iff {fmt : FloatFormat} (x : Model fmt) : x.classify = Numerics.IEEEClass.negativeNormal ↔ x.isNormal = true ∧ x.signBit = true

Negative normal classification uses policy-aware normality and the stored negative sign.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.classify_eq_positiveNormal_iff {fmt : FloatFormat} (x : Model fmt) : x.classify = Numerics.IEEEClass.positiveNormal ↔ x.isNormal = true ∧ x.signBit = false

Positive normal classification uses policy-aware normality and the stored positive sign.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_iff_classify {fmt : FloatFormat} (x : Model fmt) : x.isNaN = true ↔ x.classify = Numerics.IEEEClass.signalingNaN ∨ x.classify = Numerics.IEEEClass.quietNaN

The two NaN classes exhaust precisely the NaN encodings.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_iff_classify {fmt : FloatFormat} (x : Model fmt) : x.isFinite = true ↔ x.classify = Numerics.IEEEClass.negativeZero ∨ x.classify = Numerics.IEEEClass.positiveZero ∨ x.classify = Numerics.IEEEClass.negativeSubnormal ∨ x.classify = Numerics.IEEEClass.positiveSubnormal ∨ x.classify = Numerics.IEEEClass.negativeNormal ∨ x.classify = Numerics.IEEEClass.positiveNormal

The finite classes exhaust precisely zero, subnormal, and normal encodings.