Correctness of native binary32 product rounding

The binary32 product path keeps the unrounded product and all rounding decisions in native words. The refinement covers normal, subnormal, carry, overflow, and signed-zero branches and relates each one to the generic exact-dyadic rounder.

roundProduct_eq_roundDyadic applies to every UInt64 magnitude at a scale of at most 506, covering multiplication, aligned addition, and fused multiply-add. Runtime clients import Rounding.Runtime independently of these proofs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.roundDyadic_shiftLeft_add_of_lt_half (sign : Bool) (small large gap : ℕ) (exponent : ℤ) (hlargeLow : 2 ^ 23 ≤ large) (hlargeHigh : large < 2 ^ 24) (hgap : 0 < gap) (hsmall : small < 2 ^ (gap - 1)) (hnormal : -126 ≤ Int.ofNat (23 + gap) + exponent) (hoverflow : Int.ofNat (23 + gap) + exponent ≤ 127) : roundDyadic { negative := sign, significand := large <<< gap + small, exponent := exponent } = mkBits sign (Int.ofNat (23 + gap) + exponent + 127).toNat (large - 2 ^ 23)

An aligned remainder below half an ulp leaves a normal binary32 mantissa unchanged by rounding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.roundProduct_eq_roundDyadic (sign : Bool) (product scale : UInt64) (hscale : scale.toNat ≤ 506) : roundProduct sign product scale = roundDyadic { negative := sign, significand := product.toNat, exponent := Int.ofNat scale.toNat - 298 }

Native word rounding agrees with the generic dyadic rounder.

The scale bound covers binary32 multiplication and aligned addition. The magnitude needs no separate hypothesis because every UInt64 value is below 2^64.