Arbitrary integer constructors

Lean 4.33 introduced the logical floating-point models. Lean 4.34 exposes the definitions of Float.ofNat, Float.ofInt, and their binary32 counterparts. The arbitrary-integer casts use these constructors, whose scientific-literal path includes a small-input optimization. These proofs account for both branches before applying the shared integer conversion specification.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.round_shiftLeft (spec : Float.Model.Format) (sign : Float.Model.UnpackedFloat.Sign) (n k : ℕ) (e : ℤ) (hn : n ≠ 0) : Float.Model.UnpackedFloat.round spec sign (n <<< k) (e - ↑k) = Float.Model.UnpackedFloat.round spec sign n e

Moving exact trailing binary zeros into the exponent does not change model rounding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ofScientific_zero_eq_ofNat (spec : Float.Model.Format) (n : ℕ) : Float.Model.UnpackedFloat.ofScientific spec n 0 = Float.Model.UnpackedFloat.ofNat spec n

A scientific literal with decimal exponent zero is the shared natural-number constructor.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat_ofNat (n : ℕ) : toModel (ofFloat (Float.ofNat n)) = Formats.BinaryInterchange.Model.roundRat Formats.BinaryInterchange.FloatFormat.binary64 false n 1

Binary64 natural construction is nearest-even rounding of a denominator-one rational.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat32_ofNat (n : ℕ) : toModel (ofFloat32 (Float32.ofNat n)) = Formats.BinaryInterchange.Model.roundRat Formats.BinaryInterchange.FloatFormat.binary32 false n 1

Binary32 natural construction is nearest-even rounding of a denominator-one rational.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat_ofInt (n : ℤ) : toModel (ofFloat (Float.ofInt n)) = Formats.BinaryInterchange.Model.roundDyadic Formats.BinaryInterchange.FloatFormat.binary64 (Numerics.Dyadic.ofScaledInt n 0)

Binary64 integer construction uses the shared dyadic rounder, including signed overflow.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat32_ofInt (n : ℤ) : toModel (ofFloat32 (Float32.ofInt n)) = Formats.BinaryInterchange.Model.roundDyadic Formats.BinaryInterchange.FloatFormat.binary32 (Numerics.Dyadic.ofScaledInt n 0)

Binary32 integer construction uses the shared dyadic rounder, including signed overflow.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat_intToFloat (n : ℤ) : toModel (ofFloat n.toFloat) = Formats.BinaryInterchange.Model.roundDyadic Formats.BinaryInterchange.FloatFormat.binary64 (Numerics.Dyadic.ofScaledInt n 0)

The arbitrary-precision integer cast to binary64 has the same rounding specification.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat32_intToFloat32 (n : ℤ) : toModel (ofFloat32 n.toFloat32) = Formats.BinaryInterchange.Model.roundDyadic Formats.BinaryInterchange.FloatFormat.binary32 (Numerics.Dyadic.ofScaledInt n 0)

The arbitrary-precision integer cast to binary32 has the same rounding specification.