Correctness of signed-magnitude dyadic addition

The runtime aligns dyadic significands and adds their natural-number magnitudes with separate signs. addDyadicImpl_eq identifies this implementation with exact dyadic addition, including cancellation and the signed-zero rule.

The @[csimp] theorem addDyadic_eq_addDyadicImpl supplies the equality used by the compiler substitution. The remaining public lemmas describe equal- and adjacent-exponent cases used by native arithmetic refinements.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.addDyadic_sameSign_sameExponent (sign : Bool) (left right : ℕ) (exponent : ℤ) (hleft : left ≠ 0) (hright : right ≠ 0) : addDyadic { negative := sign, significand := left, exponent := exponent } { negative := sign, significand := right, exponent := exponent } = { negative := sign, significand := left + right, exponent := exponent }

Adding two nonzero dyadics with the same sign and exponent adds only their significands.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.addDyadic_oppositeSign_sameExponent_largeLeft (largeSign smallSign : Bool) (large small : ℕ) (exponent : ℤ) (hlarge : large ≠ 0) (hsmall : small ≠ 0) (hsign : largeSign ≠ smallSign) (hlt : small < large) : addDyadic { negative := largeSign, significand := large, exponent := exponent } { negative := smallSign, significand := small, exponent := exponent } = { negative := largeSign, significand := large - small, exponent := exponent }

Subtract equal-exponent dyadic magnitudes when the left operand has the larger magnitude.

Opposite signs turn addition into exact subtraction; the result keeps the sign of the larger magnitude and needs no rounding or exponent adjustment.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.addDyadic_oppositeSign_sameExponent_largeRight (smallSign largeSign : Bool) (small large : ℕ) (exponent : ℤ) (hsmall : small ≠ 0) (hlarge : large ≠ 0) (hsign : smallSign ≠ largeSign) (hlt : small < large) : addDyadic { negative := smallSign, significand := small, exponent := exponent } { negative := largeSign, significand := large, exponent := exponent } = { negative := largeSign, significand := large - small, exponent := exponent }

Subtract equal-exponent dyadic magnitudes when the right operand has the larger magnitude.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.addDyadic_oppositeSign_sameExponent_eq_zero (leftSign rightSign : Bool) (magnitude : ℕ) (exponent : ℤ) (hmagnitude : magnitude ≠ 0) (hsign : leftSign ≠ rightSign) : addDyadic { negative := leftSign, significand := magnitude, exponent := exponent } { negative := rightSign, significand := magnitude, exponent := exponent } = { negative := false, significand := 0, exponent := 0 }

Equal nonzero magnitudes with opposite signs cancel to canonical positive zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.addDyadic_oppositeSign_adjacentExponent_largeLeft (largeSign smallSign : Bool) (large small : ℕ) (exponent : ℤ) (hlarge : large ≠ 0) (hsmall : small ≠ 0) (hsign : largeSign ≠ smallSign) (hlt : small < large.shiftLeft 1) : addDyadic { negative := largeSign, significand := large, exponent := exponent + 1 } { negative := smallSign, significand := small, exponent := exponent } = { negative := largeSign, significand := large.shiftLeft 1 - small, exponent := exponent }

Opposite-sign subtraction with the larger left operand one exponent higher.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.addDyadic_oppositeSign_adjacentExponent_largeRight (smallSign largeSign : Bool) (small large : ℕ) (exponent : ℤ) (hsmall : small ≠ 0) (hlarge : large ≠ 0) (hsign : smallSign ≠ largeSign) (hlt : small < large.shiftLeft 1) : addDyadic { negative := smallSign, significand := small, exponent := exponent } { negative := largeSign, significand := large, exponent := exponent + 1 } = { negative := largeSign, significand := large.shiftLeft 1 - small, exponent := exponent }

Opposite-sign subtraction with the larger right operand one exponent higher.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.addDyadic_alignRightOffset (offset : ℕ) (xSign ySign : Bool) (xMagnitude yMagnitude xScale yScale : ℕ) (hx : xMagnitude ≠ 0) (hy : yMagnitude ≠ 0) (hscale : xScale ≤ yScale) : addDyadic { negative := xSign, significand := xMagnitude, exponent := Int.ofNat xScale - Int.ofNat offset } { negative := ySign, significand := yMagnitude, exponent := Int.ofNat yScale - Int.ofNat offset } = addDyadic { negative := xSign, significand := xMagnitude, exponent := Int.ofNat xScale - Int.ofNat offset } { negative := ySign, significand := yMagnitude <<< (yScale - xScale), exponent := Int.ofNat xScale - Int.ofNat offset }

Align the right dyadic magnitude to the left exponent without changing the exact sum.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.addDyadic_alignLeftOffset (offset : ℕ) (xSign ySign : Bool) (xMagnitude yMagnitude xScale yScale : ℕ) (hx : xMagnitude ≠ 0) (hy : yMagnitude ≠ 0) (hscale : yScale < xScale) : addDyadic { negative := xSign, significand := xMagnitude, exponent := Int.ofNat xScale - Int.ofNat offset } { negative := ySign, significand := yMagnitude, exponent := Int.ofNat yScale - Int.ofNat offset } = addDyadic { negative := xSign, significand := xMagnitude <<< (xScale - yScale), exponent := Int.ofNat yScale - Int.ofNat offset } { negative := ySign, significand := yMagnitude, exponent := Int.ofNat yScale - Int.ofNat offset }

Align the left dyadic magnitude to the right exponent without changing the exact sum.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.addDyadicImpl_eq (a b : Numerics.Dyadic) : addDyadicImpl a b = addDyadic a b

Signed-magnitude dyadic addition is equal to the public exact definition.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.addDyadic_comm (a b : Numerics.Dyadic) : addDyadic a b = addDyadic b a

Exact dyadic addition is commutative, including its signed-zero rule.

@[csimp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.addDyadic_eq_addDyadicImpl : addDyadic = addDyadicImpl

Compile exact dyadic addition through the verified signed-magnitude implementation.