Numerical meaning of binary classification

For a finite value, normality means its magnitude reaches 2 ^ minNormalExponent. Subnormals have positive magnitude below that threshold. These equivalences hold for every descriptor, including arbitrary valid biases and finite encodings with normal all-ones exponents.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.abs_toRat_eq_fields {fmt : FloatFormat} {x : Model fmt} {d : Numerics.Dyadic} (hx : x.toDyadic? = some d) : |d.toRat| = if x.expField = 0 then ↑x.fracField * 2 ^ fmt.minSubnormalExponent else (2 ^ fmt.fracWidth + ↑x.fracField) * 2 ^ (↑x.expField - ↑fmt.exponentBias - ↑fmt.fracWidth)

The exact magnitude of any finite word, expressed in its stored magnitude fields.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNormal_iff_le_abs_toRat {fmt : FloatFormat} {x : Model fmt} {d : Numerics.Dyadic} (hx : x.toDyadic? = some d) : x.isNormal = true ↔ 2 ^ fmt.minNormalExponent ≤ |d.toRat|

A decoded finite value is normal exactly when its magnitude reaches the normal threshold.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isZero_iff_toRat_eq_zero {fmt : FloatFormat} {x : Model fmt} {d : Numerics.Dyadic} (hx : x.toDyadic? = some d) : x.isZero = true ↔ d.toRat = 0

Zero classification of a decoded value is exactly numerical zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isSubnormal_iff_abs_toRat {fmt : FloatFormat} {x : Model fmt} {d : Numerics.Dyadic} (hx : x.toDyadic? = some d) : x.isSubnormal = true ↔ 0 < |d.toRat| ∧ |d.toRat| < 2 ^ fmt.minNormalExponent

Subnormal classification is precisely positive magnitude below the normal threshold.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNormal_iff_exists_toDyadic {fmt : FloatFormat} (x : Model fmt) : x.isNormal = true ↔ ∃ (d : Numerics.Dyadic), x.toDyadic? = some d ∧ 2 ^ fmt.minNormalExponent ≤ |d.toRat|

Normality depends on the exact finite denotation, with NaNs and infinities excluded.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isSubnormal_iff_exists_toDyadic {fmt : FloatFormat} (x : Model fmt) : x.isSubnormal = true ↔ ∃ (d : Numerics.Dyadic), x.toDyadic? = some d ∧ 0 < |d.toRat| ∧ |d.toRat| < 2 ^ fmt.minNormalExponent

A subnormal is finite, with magnitude strictly between zero and the normal threshold.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNormal_iff_le_abs_toReal {fmt : FloatFormat} (x : Model fmt) : x.isNormal = true ↔ x.isFinite = true ∧ 2 ^ fmt.minNormalExponent ≤ |x.toReal|

Real-valued normality uses the declared bias, independently of encoding policy.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isSubnormal_iff_abs_toReal {fmt : FloatFormat} (x : Model fmt) : x.isSubnormal = true ↔ x.isFinite = true ∧ 0 < |x.toReal| ∧ |x.toReal| < 2 ^ fmt.minNormalExponent

Real-valued subnormality is strict positive magnitude below the normal threshold.