Packing special values in Lean's float model

These packing identities preserve the sign of zero and infinity in Lean's IEEE model. They apply to arbitrary field widths; descriptor-level classification additionally requires the relevant encoding support. In particular, negZero is a NaN word under FNUZ, and posInf and negInf need not denote infinities under finite-only policies.

The shared lemmas let operation proofs handle zero and overflow results without unfolding their exponent and significand fields.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.unpack_pack_infinity (spec : Float.Model.Format) (sign : Float.Model.UnpackedFloat.Sign) : Float.Model.UnpackedFloat.unpack spec (Float.Model.UnpackedFloat.pack spec (Float.Model.UnpackedFloat.infinity sign)) = Float.Model.UnpackedFloat.infinity sign

Packing and unpacking an infinity preserves its sign.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.posInf_eq_ofModel_infinity (fmt : FloatFormat) : posInf fmt = ofModel fmt (Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.positive)

Positive executable infinity is Lean's positive packed infinity.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.negInf_eq_ofModel_infinity (fmt : FloatFormat) : negInf fmt = ofModel fmt (Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.negative)

Negative executable infinity is Lean's negative packed infinity.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.expField_ofModel_infinity (fmt : FloatFormat) (sign : Float.Model.UnpackedFloat.Sign) : (ofModel fmt (Float.Model.UnpackedFloat.infinity sign)).expField = fmt.expAllOnesNat

Model packing exposes the all-ones exponent field for either infinity sign.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.fracField_ofModel_infinity (fmt : FloatFormat) (sign : Float.Model.UnpackedFloat.Sign) : (ofModel fmt (Float.Model.UnpackedFloat.infinity sign)).fracField = 0

Model packing exposes a zero fraction field for either infinity sign.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.signBit_ofModel_infinity (fmt : FloatFormat) (sign : Float.Model.UnpackedFloat.Sign) : (ofModel fmt (Float.Model.UnpackedFloat.infinity sign)).signBit = modelSignBit sign

Model packing preserves the sign bit of an infinity.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isInf_ofModel_infinity (fmt : FloatFormat) (hfmt : fmt.supportsInfinity = true) (sign : Float.Model.UnpackedFloat.Sign) : (ofModel fmt (Float.Model.UnpackedFloat.infinity sign)).isInf = true

A model-packed infinity is classified as infinity by every infinity-bearing descriptor.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_ofModel_infinity (fmt : FloatFormat) (hfmt : fmt.supportsInfinity = true) (sign : Float.Model.UnpackedFloat.Sign) : (ofModel fmt (Float.Model.UnpackedFloat.infinity sign)).isNaN = false

A model-packed infinity is not classified as NaN by an infinity-bearing descriptor.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_ofModel_infinity (fmt : FloatFormat) (hfmt : fmt.supportsInfinity = true) (sign : Float.Model.UnpackedFloat.Sign) : (ofModel fmt (Float.Model.UnpackedFloat.infinity sign)).isFinite = false

A model-packed infinity is not finite under an infinity-bearing descriptor.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toModel_ofModel_infinity (fmt : FloatFormat) (sign : Float.Model.UnpackedFloat.Sign) : (ofModel fmt (Float.Model.UnpackedFloat.infinity sign)).toModel = Float.Model.UnpackedFloat.infinity sign

Re-decoding a model-packed infinity recovers the same logical value.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.signBit_posInf (fmt : FloatFormat) : (posInf fmt).signBit = false

Positive executable infinity has positive sign.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.signBit_negInf (fmt : FloatFormat) : (negInf fmt).signBit = true

Negative executable infinity has negative sign.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isInf_posInf (fmt : FloatFormat) (hfmt : fmt.supportsInfinity = true) : (posInf fmt).isInf = true

Positive executable infinity is classified as infinity whenever the format supports it.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isInf_negInf (fmt : FloatFormat) (hfmt : fmt.supportsInfinity = true) : (negInf fmt).isInf = true

Negative executable infinity is classified as infinity whenever the format supports it.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_posInf (fmt : FloatFormat) (hfmt : fmt.supportsInfinity = true) : (posInf fmt).isNaN = false

Positive executable infinity is not a NaN whenever the format supports infinity.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_negInf (fmt : FloatFormat) (hfmt : fmt.supportsInfinity = true) : (negInf fmt).isNaN = false

Negative executable infinity is not a NaN whenever the format supports infinity.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_posInf (fmt : FloatFormat) (hfmt : fmt.supportsInfinity = true) : (posInf fmt).isFinite = false

Positive executable infinity is not finite whenever the format supports infinity.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_negInf (fmt : FloatFormat) (hfmt : fmt.supportsInfinity = true) : (negInf fmt).isFinite = false

Negative executable infinity is not finite whenever the format supports infinity.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toModel_posInf (fmt : FloatFormat) : (posInf fmt).toModel = Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.positive

Decoding positive executable infinity recovers positive logical infinity.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toModel_negInf (fmt : FloatFormat) : (negInf fmt).toModel = Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.negative

Decoding negative executable infinity recovers negative logical infinity.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.unpack_pack_zero (spec : Float.Model.Format) (sign : Float.Model.UnpackedFloat.Sign) : Float.Model.UnpackedFloat.unpack spec (Float.Model.UnpackedFloat.pack spec (Float.Model.UnpackedFloat.zero sign)) = Float.Model.UnpackedFloat.zero sign

Packing and unpacking a signed zero preserves its sign.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.expField_ofModel_zero (fmt : FloatFormat) (sign : Float.Model.UnpackedFloat.Sign) : (ofModel fmt (Float.Model.UnpackedFloat.zero sign)).expField = 0

Model packing exposes a zero exponent field for either signed zero.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.fracField_ofModel_zero (fmt : FloatFormat) (sign : Float.Model.UnpackedFloat.Sign) : (ofModel fmt (Float.Model.UnpackedFloat.zero sign)).fracField = 0

Model packing exposes a zero fraction field for either signed zero.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.signBit_ofModel_zero (fmt : FloatFormat) (sign : Float.Model.UnpackedFloat.Sign) : (ofModel fmt (Float.Model.UnpackedFloat.zero sign)).signBit = modelSignBit sign

Model packing preserves the sign bit of zero.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isZero_ofModel_zero (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Float.Model.UnpackedFloat.Sign) : (ofModel fmt (Float.Model.UnpackedFloat.zero sign)).isZero = true

A model-packed signed zero is classified as zero by a conventional IEEE descriptor.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isInf_ofModel_zero (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Float.Model.UnpackedFloat.Sign) : (ofModel fmt (Float.Model.UnpackedFloat.zero sign)).isInf = false

A model-packed signed zero is not infinity under a conventional IEEE descriptor.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_ofModel_zero (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Float.Model.UnpackedFloat.Sign) : (ofModel fmt (Float.Model.UnpackedFloat.zero sign)).isNaN = false

A model-packed signed zero is not NaN under a conventional IEEE descriptor.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_ofModel_zero (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Float.Model.UnpackedFloat.Sign) : (ofModel fmt (Float.Model.UnpackedFloat.zero sign)).isFinite = true

A model-packed signed zero is finite under a conventional IEEE descriptor.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toModel_ofModel_zero (fmt : FloatFormat) (sign : Float.Model.UnpackedFloat.Sign) : (ofModel fmt (Float.Model.UnpackedFloat.zero sign)).toModel = Float.Model.UnpackedFloat.zero sign

Re-decoding a model-packed signed zero recovers the same logical value.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_ofModel_zero (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Float.Model.UnpackedFloat.Sign) : (ofModel fmt (Float.Model.UnpackedFloat.zero sign)).toReal = 0

IEEE model packing preserves the real value of signed zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.posZero_eq_ofModel_zero (fmt : FloatFormat) : posZero fmt = ofModel fmt (Float.Model.UnpackedFloat.zero Float.Model.UnpackedFloat.Sign.positive)

Positive executable zero is Lean's positive packed zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.negZero_eq_ofModel_zero (fmt : FloatFormat) : negZero fmt = ofModel fmt (Float.Model.UnpackedFloat.zero Float.Model.UnpackedFloat.Sign.negative)

Negative executable zero is Lean's negative packed zero.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.signBit_posZero (fmt : FloatFormat) : (posZero fmt).signBit = false

Positive executable zero has positive sign.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.signBit_negZero (fmt : FloatFormat) : (negZero fmt).signBit = true

Negative executable zero has negative sign.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.signBit_zero (fmt : FloatFormat) (sign : Bool) : (zero fmt sign).signBit = (sign && fmt.supportsSignedZero)

The policy-aware zero constructor keeps the requested sign exactly when signed zero is supported.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isZero_posZero (fmt : FloatFormat) : (posZero fmt).isZero = true

The canonical positive-zero word is classified as zero in every supported encoding.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.expField_posZero (fmt : FloatFormat) : (posZero fmt).expField = 0

Positive executable zero has a zero exponent field.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.fracField_posZero (fmt : FloatFormat) : (posZero fmt).fracField = 0

Positive executable zero has a zero fraction field.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.expField_negZero (fmt : FloatFormat) : (negZero fmt).expField = 0

Negative executable zero has a zero exponent field.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.fracField_negZero (fmt : FloatFormat) : (negZero fmt).fracField = 0

Negative executable zero has a zero fraction field.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isZero_negZero (fmt : FloatFormat) (hfmt : fmt.supportsSignedZero = true) : (negZero fmt).isZero = true

In an encoding with two zero words, negative executable zero is classified as zero.

Under the finite-unsigned-zero encoding the negative-zero word is the NaN, so the hypothesis cannot be dropped.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_posZero (fmt : FloatFormat) : (posZero fmt).isNaN = false

Positive executable zero is not a NaN in any encoding.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_negZero (fmt : FloatFormat) (hfmt : fmt.supportsSignedZero = true) : (negZero fmt).isNaN = false

Negative executable zero is not a NaN when the encoding has two zero words.

Under the finite-unsigned-zero encoding the negative-zero word is the NaN, so the hypothesis cannot be dropped.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isInf_posZero (fmt : FloatFormat) : (posZero fmt).isInf = false

Positive executable zero is not infinity in any encoding.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isInf_negZero (fmt : FloatFormat) : (negZero fmt).isInf = false

Negative executable zero is not infinity in any encoding.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_posZero (fmt : FloatFormat) : (posZero fmt).isFinite = true

Positive executable zero is finite in any encoding.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_negZero (fmt : FloatFormat) (hfmt : fmt.supportsSignedZero = true) : (negZero fmt).isFinite = true

Negative executable zero is finite when the encoding has two zero words.

Under the finite-unsigned-zero encoding the negative-zero word is the NaN, so the hypothesis cannot be dropped.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toModel_posZero (fmt : FloatFormat) : (posZero fmt).toModel = Float.Model.UnpackedFloat.zero Float.Model.UnpackedFloat.Sign.positive

Decoding positive executable zero recovers positive logical zero.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toModel_negZero (fmt : FloatFormat) : (negZero fmt).toModel = Float.Model.UnpackedFloat.zero Float.Model.UnpackedFloat.Sign.negative

Decoding negative executable zero recovers negative logical zero.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_posZero (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) : (posZero fmt).toReal = 0

Positive zero denotes real zero in every conventional IEEE format.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_negZero (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) : (negZero fmt).toReal = 0

Negative zero denotes real zero in every conventional IEEE format.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_signedZero (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (negative : Bool) : (if negative = true then negZero fmt else posZero fmt).toReal = 0

Either signed-zero constructor has real value zero in a conventional IEEE format.