TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Kernels.FixedWord.SignedMagnitude.Proof

Exactness of shared native signed-magnitude arithmetic #

The format-independent UInt64 signed-magnitude primitive implements exact dyadic addition under its capacity hypotheses. Equal signs require a no-overflow hypothesis; opposite signs reduce to an exact difference. The two-limb refinement is in SignedMagnitude.UInt128.Proof.

source
def FloatLib.Numerics.FixedWord.signedMagnitudeDyadic (negative : Bool) (magnitude : UInt64) (exponent : ℤ) :
Dyadic

Interpret a native 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 added.

Instances For
    source
    theorem FloatLib.Numerics.FixedWord.addSignedMagnitudes_sign_eq_false_of_magnitude_eq_zero (leftNegative rightNegative : Bool) (leftMagnitude rightMagnitude : UInt64) (hleft : leftMagnitude ≠ 0) (hright : rightMagnitude ≠ 0) (hsum : leftNegative = rightNegative → leftMagnitude.toNat + rightMagnitude.toNat < 2 ^ 64) (hzero : (addSignedMagnitudes leftNegative rightNegative leftMagnitude rightMagnitude).2 = 0) :
    (addSignedMagnitudes leftNegative rightNegative leftMagnitude rightMagnitude).1 = false

    A zero magnitude returned by native signed-magnitude addition always has a positive sign.

    The no-overflow premise rules out a wrapped same-sign sum. With nonzero inputs, the remaining zero case is exact cancellation of opposite, equal magnitudes.

    source
    theorem FloatLib.Numerics.FixedWord.signedMagnitudeDyadic_addSignedMagnitudes_eq_addFields (leftNegative rightNegative : Bool) (leftMagnitude rightMagnitude : UInt64) (exponent : ℤ) (hleft : leftMagnitude ≠ 0) (hright : rightMagnitude ≠ 0) (hsum : leftNegative = rightNegative → leftMagnitude.toNat + rightMagnitude.toNat < 2 ^ 64) :
    signedMagnitudeDyadic (addSignedMagnitudes leftNegative rightNegative leftMagnitude rightMagnitude).1 (addSignedMagnitudes leftNegative rightNegative leftMagnitude rightMagnitude).2 exponent = Dyadic.addFields leftNegative leftMagnitude.toNat exponent rightNegative rightMagnitude.toNat exponent

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

    The only capacity hypothesis is required by same-sign addition. Opposite-sign subtraction cannot overflow, while the nonzero hypotheses exclude the input-zero branches handled directly by format-specific kernels.