Classification refinement for configured binary values

Every storage codec preserves classification and canonicality. The ten class characterizations and the exact numerical threshold theorems are transported from the descriptor model, with no assumptions on storage width, bias, or exceptional-value policy beyond a valid descriptor.

theorem FloatLib.Floats.ExecFloat.Binary.classify_eq_model {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : classify x = (toModel x).classify

Configured classification is the descriptor-model classification.

theorem FloatLib.Floats.ExecFloat.Binary.isNormal_eq_model {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : isNormal x = (toModel x).isNormal

Configured normality is the descriptor-model normality predicate.

theorem FloatLib.Floats.ExecFloat.Binary.isCanonical_eq_model {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : isCanonical x = (toModel x).isCanonical

Configured canonicality concerns the exact interchange word decoded by the codec.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.classify_ofModel {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : Formats.BinaryInterchange.Model format) : classify (ofModel x) = x.classify

Packing any descriptor model preserves its class.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.isNormal_ofModel {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : Formats.BinaryInterchange.Model format) : isNormal (ofModel x) = x.isNormal

Packing a descriptor model preserves its normality.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.isCanonical_ofModel {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : Formats.BinaryInterchange.Model format) : isCanonical (ofModel x) = x.isCanonical

Packing a descriptor model preserves its canonicality.

theorem FloatLib.Floats.ExecFloat.Binary.classify_eq_iff {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (c : Numerics.IEEEClass) : classify x = c ↔ match c with | Numerics.IEEEClass.signalingNaN => isSignalingNaN x = true | Numerics.IEEEClass.quietNaN => isQuietNaN x = true | Numerics.IEEEClass.negativeInfinity => isInfinite x = true ∧ signBit x = true | Numerics.IEEEClass.positiveInfinity => isInfinite x = true ∧ signBit x = false | Numerics.IEEEClass.negativeZero => isZero x = true ∧ signBit x = true | Numerics.IEEEClass.positiveZero => isZero x = true ∧ signBit x = false | Numerics.IEEEClass.negativeSubnormal => isSubnormal x = true ∧ signBit x = true | Numerics.IEEEClass.positiveSubnormal => isSubnormal x = true ∧ signBit x = false | Numerics.IEEEClass.negativeNormal => isNormal x = true ∧ signBit x = true | Numerics.IEEEClass.positiveNormal => isNormal x = true ∧ signBit x = false

All ten configured classification results agree with the existing configured predicates.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.classify_eq_signalingNaN_iff {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : classify x = Numerics.IEEEClass.signalingNaN ↔ isSignalingNaN x = true

The signaling class is exactly the configured signaling predicate.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.classify_eq_quietNaN_iff {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : classify x = Numerics.IEEEClass.quietNaN ↔ isQuietNaN x = true

The quiet class is exactly the configured quiet-NaN predicate.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.classify_eq_negativeInfinity_iff {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : classify x = Numerics.IEEEClass.negativeInfinity ↔ isInfinite x = true ∧ signBit x = true

Negative infinity retains its stored negative sign.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.classify_eq_positiveInfinity_iff {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : classify x = Numerics.IEEEClass.positiveInfinity ↔ isInfinite x = true ∧ signBit x = false

Positive infinity retains its stored positive sign.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.classify_eq_negativeZero_iff {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : classify x = Numerics.IEEEClass.negativeZero ↔ isZero x = true ∧ signBit x = true

Negative zero is a zero with a negative stored sign under the configured policy.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.classify_eq_positiveZero_iff {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : classify x = Numerics.IEEEClass.positiveZero ↔ isZero x = true ∧ signBit x = false

Positive zero is a zero with a positive stored sign.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.classify_eq_negativeSubnormal_iff {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : classify x = Numerics.IEEEClass.negativeSubnormal ↔ isSubnormal x = true ∧ signBit x = true

Negative subnormal classification agrees with the configured predicates.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.classify_eq_positiveSubnormal_iff {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : classify x = Numerics.IEEEClass.positiveSubnormal ↔ isSubnormal x = true ∧ signBit x = false

Positive subnormal classification agrees with the configured predicates.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.classify_eq_negativeNormal_iff {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : classify x = Numerics.IEEEClass.negativeNormal ↔ isNormal x = true ∧ signBit x = true

Negative normal classification uses the configured policy and negative sign.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.classify_eq_positiveNormal_iff {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : classify x = Numerics.IEEEClass.positiveNormal ↔ isNormal x = true ∧ signBit x = false

Positive normal classification uses the configured policy and positive sign.

theorem FloatLib.Floats.ExecFloat.Binary.isNormal_iff {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : isNormal x = true ↔ isFinite x = true ∧ isZero x = false ∧ isSubnormal x = false

Normality excludes zeros, subnormals, infinities, and NaNs for every storage codec.

theorem FloatLib.Floats.ExecFloat.Binary.isFinite_eq_zero_or_subnormal_or_normal {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : isFinite x = (isZero x || isSubnormal x || isNormal x)

Configured finiteness is the union of the three finite classes.

theorem FloatLib.Floats.ExecFloat.Binary.isNormal_iff_exactValue {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : isNormal x = true ↔ ∃ (d : Numerics.Dyadic), exactValue x = Formats.BinaryInterchange.Model.ExactValue.finite d ∧ 2 ^ format.minNormalExponent ≤ |d.toRat|

Configured normality is an exact finite magnitude at or above the normal threshold.

theorem FloatLib.Floats.ExecFloat.Binary.isSubnormal_iff_exactValue {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : isSubnormal x = true ↔ ∃ (d : Numerics.Dyadic), exactValue x = Formats.BinaryInterchange.Model.ExactValue.finite d ∧ 0 < |d.toRat| ∧ |d.toRat| < 2 ^ format.minNormalExponent

Configured subnormality is an exact positive magnitude below the normal threshold.

theorem FloatLib.Floats.ExecFloat.Binary.classify_eq_match_exactValue {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : classify x = match exactValue x with | Formats.BinaryInterchange.Model.ExactValue.nan sign signaling payload => if signaling = true then Numerics.IEEEClass.signalingNaN else Numerics.IEEEClass.quietNaN | Formats.BinaryInterchange.Model.ExactValue.infinity sign => if sign = true then Numerics.IEEEClass.negativeInfinity else Numerics.IEEEClass.positiveInfinity | Formats.BinaryInterchange.Model.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 ^ format.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

Every configured class is determined by its exact value and the descriptor threshold.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.isCanonical_eq_true {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : isCanonical x = true

Every configured implicit-leading-bit binary word is canonical.

theorem FloatLib.Floats.ExecFloat.Binary.isCanonical_iff_word_roundtrip {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : isCanonical x = true ↔ ofNatBits (toNatBits x) = x

Canonicality agrees with lossless reconstruction from the full interchange word.