claimroutineinferred_dep

Two scalings by S undo normalizations

Two scalings by SS turn (u∗v)/S2(u*v)/S^2 into 22b+4(u∗v)2^{2b+4}(u*v)
ties the computed pipeline to the exact product
Claim·§9.6 The multiplication algorithm·inside thmInteger multiplication in O(n (lg n)^{1-κ}) time

Statement (paper)

The two occurrences of SS in the algorithm undo different normalizations. By , the exact counterpart after the three transforms is (u∗v)/S2(u*v)/S^2, so after the first scale it is w=(u∗v)/Sw=(u*v)/S, and the second scale gives 22b+4(u∗v)2^{2b+4}(u*v), whose inverse image under Φ\Phi is the original integer coefficient convolution.

In plain English

The two occurrences of SS in the algorithm undo different normalizations: after the three transforms the exact counterpart is (u∗v)/S2(u*v)/S^2, the first scale gives w=(u∗v)/Sw=(u*v)/S, and the second scale gives 22b+4(u∗v)2^{2b+4}(u*v). Its inverse image under Φ\Phi is the original integer coefficient convolution.

Why it's here

This is the bookkeeping step that ties the computed pipeline to the exact product. It applies the source-permutation cancellation identity from the chirp lemma, (RFs+)[(RFsu)(RFsv)]=(u∗v)/S2(RF_{\boldsymbol s}^+)[(RF_{\boldsymbol s}u)(RF_{\boldsymbol s}v)]=(u*v)/S^2, to show that the first factor SS restores w=(u∗v)/Sw=(u*v)/S and the second restores the true convolution up to the known power of 2. The later error analysis can therefore compare the computed w~\widetilde w with this exact ww and conclude that rounding and carries recover the exact product.
Classified routine:
Bookkeeping consequence of the source-permutation cancellation identity in lem-chirp-permutation: it tracks the normalization factors S and the power of 2 to match the computed pipeline to the exact convolution.

Uses

claimCRT address map via controlled shiftsclaimChirp transform and source transform procedureslemChirp identity and source permutation cancellation

Used by

claimFinal error below 1/2; rounding and carries exact

Sources

PaperOpen
Section
§9.6 The multiplication algorithm
Page
—
Label
—
Line
sections/08-assembly.tex:498
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Multiplication algorithm and normalization bookkeeping" rests on claim-thm-main-4
  • info
    inferred_dep
    outline: "Multiplication algorithm and normalization bookkeeping" rests on claim-thm-main-6
  • info
    inferred_dep
    outline: "Multiplication algorithm and normalization bookkeeping" rests on lem:chirp-permutation