Correctness of native-word division for binary32

The proof connects the native logarithm, quotient rounding, and complete finite divider to the generic exact-rational specification. Runtime clients can import Division.Runtime without this development.

For significands below 2^24, the scaling shifts and rounded quotient fit in UInt64. The proof uses those bounds to connect native quotient-and-remainder rounding to exact rational rounding, including ties, subnormal results, and overflow.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.roundRatScaledWord_eq (sign : Bool) (num den : UInt64) (exponent : ℤ) (hnumFit : num.toNat < 2 ^ 24) (hdenFit : den.toNat < 2 ^ 24) : roundRatScaledWord sign num den exponent = roundRatScaled sign num.toNat den.toNat exponent

Native-word rational rounding agrees with the existing exact binary32 rounder.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.divFiniteImpl_eq (x y : Value) : divFiniteImpl? x y = divFinite? x y

The one-word finite division kernel equals the generic exact-rational implementation.