Exactness of two-limb signed-magnitude arithmetic

Two-limb signed-magnitude addition has an exact-dyadic refinement through UInt128. The proof factors execution through a signed integer coefficient, so carrier arithmetic and exact-dyadic semantics meet at one small, representation-independent boundary.

def FloatLib.Numerics.FixedWord.signedMagnitudeDyadic128 (negative : Bool) (magnitude : UInt128) (exponent : ℤ) : Dyadic

Interpret a two-limb signed magnitude as the canonical exact dyadic used after addition.

Exact cancellation is normalized to positive zero with exponent zero. Nonzero results retain the common exponent at which their magnitudes were combined.

theorem FloatLib.Numerics.FixedWord.signedMagnitudeDyadic128_eq_of_toNat_ne_zero (negative : Bool) (magnitude : UInt128) (exponent : ℤ) (hnonzero : magnitude.toNat ≠ 0) : signedMagnitudeDyadic128 negative magnitude exponent = { negative := negative, significand := magnitude.toNat, exponent := exponent }

A nonzero two-limb signed magnitude has the direct dyadic fields expected by downstream rounding. Keeping this interpretation theorem next to the representation prevents arithmetic clients from depending on the integer encoding used internally.

theorem FloatLib.Numerics.FixedWord.signedMagnitudeDyadic128_addSignedMagnitudes128_eq_addFields (leftNegative rightNegative : Bool) (leftMagnitude rightMagnitude : UInt128) (exponent : ℤ) (hleft : leftMagnitude.toNat ≠ 0) (hright : rightMagnitude.toNat ≠ 0) (hsum : leftNegative = rightNegative → leftMagnitude.toNat + rightMagnitude.toNat < 2 ^ 128) : signedMagnitudeDyadic128 (addSignedMagnitudes128 leftNegative rightNegative leftMagnitude rightMagnitude).1 (addSignedMagnitudes128 leftNegative rightNegative leftMagnitude rightMagnitude).2 exponent = Dyadic.addFields leftNegative leftMagnitude.toNat exponent rightNegative rightMagnitude.toNat exponent

Two-limb signed-magnitude addition denotes exact dyadic addition at a common exponent.

The hypotheses use the mathematical carrier view directly, avoiding representation-specific zero lemmas at every caller.