Refinement of native signed-magnitude addition

The shared UInt64 signed-magnitude primitive denotes exact dyadic addition before binary32 rounding. Keeping the proof separate preserves the small runtime import surface of FloatLib.Kernels.FixedWord.SignedMagnitude.Runtime.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.roundAddMagnitudesAtScale_eq_roundDyadic (xSign ySign : Bool) (xMagnitude yMagnitude scale : UInt64) (hx : xMagnitude ≠ 0) (hy : yMagnitude ≠ 0) (hsum : xMagnitude.toNat + yMagnitude.toNat < 2 ^ 64) (hscale : scale.toNat ≤ 506) : roundProduct (Numerics.FixedWord.addSignedMagnitudes xSign ySign xMagnitude yMagnitude).1 (Numerics.FixedWord.addSignedMagnitudes xSign ySign xMagnitude yMagnitude).2 scale = roundDyadic (addDyadic { negative := xSign, significand := xMagnitude.toNat, exponent := Int.ofNat scale.toNat - 298 } { negative := ySign, significand := yMagnitude.toNat, exponent := Int.ofNat scale.toNat - 298 })

Round one exact signed-magnitude sum at a shared native scale.

The hypotheses require nonzero operands, a sum magnitude below 2^64, and a scale of at most 506.