Shared integer rounding at the native boundary

These proofs identify Lean's integer conversion kernels with FloatLib's existing rational quantizer and dyadic integral rounder. The arguments do not depend on a machine integer width.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundRat_den_one_eq_roundDyadic (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Bool) (n : ℕ) : roundRat fmt sign n 1 = roundDyadic fmt { negative := sign, significand := n, exponent := 0 }

Rounding an integer magnitude as a denominator-one rational gives the same complete IEEE word as dyadic rounding. The equality includes nearest-even ties and overflow to signed infinity.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ofModel_ofInt_eq_roundDyadic (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (n : ℤ) : ofModel fmt (Float.Model.UnpackedFloat.ofInt fmt.toModel n) = roundDyadic fmt (Numerics.Dyadic.ofScaledInt n 0)

Lean's integer constructor is FloatLib's nearest-even dyadic rounding of that integer.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundToInt_eq_roundDyadicToInt (sign : Float.Model.UnpackedFloat.Sign) (mantissa : ℕ) (exponent : ℤ) : Float.Model.UnpackedFloat.roundToInt sign mantissa exponent = roundDyadicToInt IEEERoundingMode.towardZero { negative := modelSignBit sign, significand := mantissa, exponent := exponent }

Lean's finite conversion kernel truncates exactly the dyadic interpreted by FloatLib. No rounding of the floating-point value occurs before truncation.