Bounds for normal field packing

A normal exponent becomes a positive, in-range biased field, and removing the hidden bit from a normalized significand leaves a legal fraction. Together these bounds show that the finite-range packing guard accepts every in-range IEEE normal value.

The arithmetic facts are shared by nearest and directed rounding before either correctness proof layer is imported.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.minNormalExponent_le_maxNormalExponent (fmt : FloatFormat) : fmt.minNormalExponent ≤ fmt.maxNormalExponent

The smallest normal exponent does not exceed the largest normal exponent.

Normal field bounds

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.biasedExponent_pos (fmt : FloatFormat) (exponent : ℤ) (hmin : fmt.minNormalExponent ≤ exponent) : 0 < exponent + Int.ofNat fmt.exponentBias

A normal unbiased exponent produces a positive biased exponent field.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ofNat_toNat_biasedExponent (fmt : FloatFormat) (exponent : ℤ) (hmin : fmt.minNormalExponent ≤ exponent) : Int.ofNat (exponent + Int.ofNat fmt.exponentBias).toNat = exponent + Int.ofNat fmt.exponentBias

Conversion of a normal biased exponent through Int.toNat is exact.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.encodedExponent_le_maxFiniteExpField (fmt : FloatFormat) (exponent : ℤ) (hmin : fmt.minNormalExponent ≤ exponent) (hmax : exponent ≤ fmt.maxNormalExponent) : (exponent + Int.ofNat fmt.exponentBias).toNat ≤ fmt.maxFiniteExpField

A representable normal exponent remains within the descriptor's finite exponent range.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.encodedExponent_ne_zero (fmt : FloatFormat) (exponent : ℤ) (hmin : fmt.minNormalExponent ≤ exponent) : (exponent + Int.ofNat fmt.exponentBias).toNat ≠ 0

A normal unbiased exponent never encodes as the zero exponent field.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.decode_encodedExponent (fmt : FloatFormat) (exponent : ℤ) (hmin : fmt.minNormalExponent ≤ exponent) : Int.ofNat (exponent + Int.ofNat fmt.exponentBias).toNat - Int.ofNat fmt.exponentBias - Int.ofNat fmt.fracWidth = exponent - Int.ofNat fmt.fracWidth

Decoding a normal biased exponent recovers the intended normalized dyadic scale.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.normalizedMantissa_sub_pow2_lt (fmt : FloatFormat) (mantissa : ℕ) (hlow : pow2 fmt.fracWidth ≤ mantissa) (hhigh : mantissa < pow2 (fmt.fracWidth + 1)) : mantissa - pow2 fmt.fracWidth < 2 ^ fmt.fracWidth

Removing the implicit leading bit from a normalized mantissa fits the fraction field.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.pow2_add_normalizedMantissa_sub (fmt : FloatFormat) (mantissa : ℕ) (hlow : pow2 fmt.fracWidth ≤ mantissa) : pow2 fmt.fracWidth + (mantissa - pow2 fmt.fracWidth) = mantissa

Restoring the implicit leading bit reconstructs a normalized mantissa exactly.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Directed.Internal.fraction_le_maxFiniteFracField_ieee (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (mantissa : ℕ) (hhigh : mantissa < pow2 (fmt.fracWidth + 1)) : mantissa - pow2 fmt.fracWidth ≤ fmt.maxFiniteFracField

Removing the hidden bit from a normalized IEEE significand leaves a legal fraction field.

Both dyadic and rational packing use this fact. Keeping it here makes the format argument independent of the exact-number representation used by the caller.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Directed.Internal.packingGuard_eq_false (fmt : FloatFormat) (exponent : ℤ) (fraction : ℕ) (hmin : fmt.minNormalExponent ≤ exponent) (hmax : exponent ≤ fmt.maxNormalExponent) (hfraction : fraction ≤ fmt.maxFiniteFracField) : have encodedExponent := (exponent + Int.ofNat fmt.exponentBias).toNat; (decide (encodedExponent > fmt.maxFiniteExpField) || encodedExponent == fmt.maxFiniteExpField && decide (fraction > fmt.maxFiniteFracField)) = false

In-range normal fields cannot trigger the overflow guard shared by the dyadic and rational packers.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Directed.Internal.normalizedGuard_eq_false (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (mantissa : ℕ) (exponent : ℤ) (hhigh : mantissa < pow2 (fmt.fracWidth + 1)) (hmin : fmt.minNormalExponent ≤ exponent) (hmax : exponent ≤ fmt.maxNormalExponent) : have encodedExponent := (exponent + Int.ofNat fmt.exponentBias).toNat; have fraction := mantissa - pow2 fmt.fracWidth; (decide (encodedExponent > fmt.maxFiniteExpField) || encodedExponent == fmt.maxFiniteExpField && decide (fraction > fmt.maxFiniteFracField)) = false

A normalized in-range IEEE significand cannot trigger the overflow guard shared by the dyadic and rational packers: the encoded exponent does not exceed the maximal finite field and the fraction is legal.