Binary classification predicates

The finite classes partition every descriptor's finite values. In particular, subnormal fields remain finite under every exceptional-value policy, whereas zero fields alone do not imply zero in FNUZ. The finite hypothesis in isZero_iff_fields_of_isFinite excludes its NaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isZero_iff_fields_of_isFinite {fmt : FloatFormat} {x : Model fmt} (hx : x.isFinite = true) : x.isZero = true ↔ x.expField = 0 ∧ x.fracField = 0

For a finite value, zero means that both magnitude fields vanish.

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

Every subnormal field pattern is finite, including under the FNUZ policy.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNormal_iff_fields {fmt : FloatFormat} (x : Model fmt) : x.isNormal = true ↔ x.isFinite = true ∧ x.expField ≠ 0

The normal predicate uses the descriptor's finiteness policy and nonzero exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNormal_iff {fmt : FloatFormat} (x : Model fmt) : x.isNormal = true ↔ x.isFinite = true ∧ x.isZero = false ∧ x.isSubnormal = false

Normal values are exactly the finite values that are neither zero nor subnormal.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_eq_zero_or_subnormal_or_normal {fmt : FloatFormat} (x : Model fmt) : x.isFinite = (x.isZero || x.isSubnormal || x.isNormal)

Finiteness is the union of zero, subnormal, and normal classification.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isSubnormal_eq_false_of_isZero {fmt : FloatFormat} {x : Model fmt} (hx : x.isZero = true) : x.isSubnormal = false

Zero and subnormal classification are disjoint.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isQNaN_eq_nan_and_not_signaling {fmt : FloatFormat} (x : Model fmt) : x.isQNaN = (x.isNaN && !x.isSNaN)

Signaling and quiet NaNs partition NaNs under every supported encoding policy.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_of_isSNaN {fmt : FloatFormat} {x : Model fmt} (hx : x.isSNaN = true) : x.isNaN = true

Every signaling NaN is a NaN. Non-IEEE policies have no signaling NaNs.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isCanonical_eq_true {fmt : FloatFormat} (x : Model fmt) : x.isCanonical = true

Every exact-width binary datum is canonical, including every NaN payload.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isCanonical_iff_fields_roundtrip {fmt : FloatFormat} (x : Model fmt) : x.isCanonical = true ↔ ofFields fmt x.signBit x.expField x.fracField = x

Canonical classification agrees with exact reconstruction of all stored fields. This reconstruction preserves signaling bits and payloads as well as finite data.