Correctness of unsigned-scale exact addition

For conventional IEEE descriptors, roundSum_eq identifies unsigned-scale alignment and rounding with exact dyadic addition followed by roundDyadic. The proof includes zero operands and the signed-zero result of cancellation. The roundOffset parameter covers both addition scales and the product scales used by FMA.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteScaleAdd.roundMagnitude_eq (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (roundOffset : ℕ) (sign : Bool) (mantissa scale : ℕ) : roundMagnitude fmt roundOffset sign mantissa scale = roundDyadic fmt { negative := sign, significand := mantissa, exponent := exponent fmt scale roundOffset }

Unsigned-scale rounding is the corresponding exact dyadic rounding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteScaleAdd.roundMagnitudes_eq (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (roundOffset : ℕ) (leftSign rightSign : Bool) (left right scale : ℕ) : roundMagnitudes fmt roundOffset leftSign rightSign left right scale = roundDyadic fmt (addDyadicMagnitudes leftSign rightSign left right (exponent fmt scale roundOffset))

The signed-magnitude helper rounds the exact dyadic magnitude sum.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteScaleAdd.roundAligned_eq (fmt : FloatFormat) (roundOffset : ℕ) (highSign lowSign : Bool) (high low gap scale : ℕ) : roundAligned fmt roundOffset highSign lowSign high low gap scale = roundMagnitudes fmt roundOffset highSign lowSign (high <<< gap) low scale

Bounded alignment preserves the result of aligning the complete significands.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteScaleAdd.roundMagnitudes_comm (fmt : FloatFormat) (roundOffset : ℕ) (leftSign rightSign : Bool) (left right scale : ℕ) : roundMagnitudes fmt roundOffset leftSign rightSign left right scale = roundMagnitudes fmt roundOffset rightSign leftSign right left scale

Exchanging two signed magnitudes preserves their rounded sum, including cancellation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteScaleAdd.roundSum_eq (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (roundOffset : ℕ) (leftSign rightSign : Bool) (leftMantissa leftScale rightMantissa rightScale : ℕ) : roundSum fmt roundOffset leftSign rightSign leftMantissa leftScale rightMantissa rightScale = roundDyadic fmt (addDyadic { negative := leftSign, significand := leftMantissa, exponent := exponent fmt leftScale roundOffset } { negative := rightSign, significand := rightMantissa, exponent := exponent fmt rightScale roundOffset })

roundSum is exact dyadic addition followed by one IEEE rounding step.