Shared internal facts for directed binary semantics

These descriptor and field-packing facts are common to dyadic and rational directed rounding. Keeping them below both proof layers prevents each numerical representation from rebuilding the same IEEE-specialization arguments.

Dyadic

This module exports the format-generic normalization, executable branch, grid-bound, and field-packing theorems for directed dyadic rounding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Directed.Internal.encodedExponent_lt_expAllOnes_ieee (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (exponent : ℤ) (hmin : fmt.minNormalExponent ≤ exponent) (hmax : exponent ≤ fmt.maxNormalExponent) : (exponent + Int.ofNat fmt.exponentBias).toNat < fmt.expAllOnesNat

Encoding an in-range IEEE normal exponent produces a field strictly below the all-ones pattern.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Directed.Internal.isFinite_ofFields_of_normal_exponent (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (fraction : ℕ) (exponent : ℤ) (hmin : fmt.minNormalExponent ≤ exponent) (hmax : exponent ≤ fmt.maxNormalExponent) : (ofFields fmt false (exponent + Int.ofNat fmt.exponentBias).toNat fraction).isFinite = true

Any fraction field packed with an in-range IEEE normal exponent denotes a finite value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Directed.Internal.isFinite_ofFields_normalized (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (mantissa : ℕ) (exponent : ℤ) (hmin : fmt.minNormalExponent ≤ exponent) (hmax : exponent ≤ fmt.maxNormalExponent) : (ofFields fmt false (exponent + Int.ofNat fmt.exponentBias).toNat (mantissa - pow2 fmt.fracWidth)).isFinite = true

Packing an in-range normalized IEEE mantissa and exponent produces a finite encoding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Directed.Internal.normalizationCarry_value (fmt : FloatFormat) (exponent : ℤ) : ↑(pow2 fmt.fracWidth) * bpow (exponent + 1 - Int.ofNat fmt.fracWidth) = ↑(pow2 (fmt.fracWidth + 1)) * bpow (exponent - Int.ofNat fmt.fracWidth)

A normalization carry preserves the represented real value while moving one bit from the significand into the exponent.