Exact semantic classification of binary data

The field-based classifier refines the complete exact interpretation for every descriptor. Finite classes depend on numerical zero and the normal threshold, retaining the sign of zero. Infinity signs and NaN signaling status come from the same exact interpretation.

This entry point also exports all ten predicate characterizations, real/rational threshold theorems, the finite-class partition, and canonical stored-field reconstruction.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.classify_of_toDyadic {fmt : FloatFormat} {x : Model fmt} {d : Numerics.Dyadic} (hx : x.toDyadic? = some d) : x.classify = if d.toRat = 0 then if d.negative = true then Numerics.IEEEClass.negativeZero else Numerics.IEEEClass.positiveZero else if |d.toRat| < 2 ^ fmt.minNormalExponent then if d.negative = true then Numerics.IEEEClass.negativeSubnormal else Numerics.IEEEClass.positiveSubnormal else if d.negative = true then Numerics.IEEEClass.negativeNormal else Numerics.IEEEClass.positiveNormal

Finite classification agrees with exact numerical zero, magnitude, and the decoded sign.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.classify_eq_match_exactValue {fmt : FloatFormat} (x : Model fmt) : x.classify = match x.exactValue with | ExactValue.nan sign signaling payload => if signaling = true then Numerics.IEEEClass.signalingNaN else Numerics.IEEEClass.quietNaN | ExactValue.infinity sign => if sign = true then Numerics.IEEEClass.negativeInfinity else Numerics.IEEEClass.positiveInfinity | ExactValue.finite d => if d.toRat = 0 then if d.negative = true then Numerics.IEEEClass.negativeZero else Numerics.IEEEClass.positiveZero else if |d.toRat| < 2 ^ fmt.minNormalExponent then if d.negative = true then Numerics.IEEEClass.negativeSubnormal else Numerics.IEEEClass.positiveSubnormal else if d.negative = true then Numerics.IEEEClass.negativeNormal else Numerics.IEEEClass.positiveNormal

Classification is determined by the complete exact value and the declared normal threshold. The NaN sign and payload do not affect its signaling/quiet class.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.classify_eq_of_exactValue_eq {fmt : FloatFormat} {x y : Model fmt} (h : x.exactValue = y.exactValue) : x.classify = y.classify

Equal complete exact values have equal classes, without any IEEE-policy restriction.