Executable normalization for binary interchange formats

These computations normalize exact integer mantissas with round-to-nearest, ties-to-even. Mantissa widths and target exponents are parameters; no named binary format is selected.

Proofs relating these computations to Lean's logical floating-point model are kept in ModelRounding.Proof, so executable clients can import this module without the large semantic proof layer.

References

• IEEE Standard for Floating-Point Arithmetic, IEEE 754-2019, Section 4.3.1.
• Lean 4, Init.Data.Float.Model.Unpacked.Round.

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundMantissaAtExponentEven (mantissa : ℕ) (exponent targetExponent : ℤ) : ℕ

Round an exact integer mantissa after expressing it at targetExponent.

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundMantissaToLeadingBitEven (mantissa leadingBit : ℕ) : ℕ

Round a positive integer mantissa to the precision specified by leadingBit + 1; a rounding carry can produce one extra bit.

def FloatLib.Floats.Formats.BinaryInterchange.Model.finishRoundedMantissa (spec : Float.Model.Format) (sign : Float.Model.UnpackedFloat.Sign) (rounded : ℕ × ℤ) : Float.Model.UnpackedFloat

Complete model rounding after the first rounded mantissa and exponent are known.