claimroutineinferred_dep

Final error below 1/2; rounding and carries exact

Total error is below 1/21/2, so rounding and carries recover the product
closes the correctness argument
Claim·§9.7.2 The final integer coefficients·inside thmInteger multiplication in O(n (lg n)^{1-κ}) time

Statement (paper)

The computed first scaled result w~\widetilde w approximates w=(u∗v)/Sw=(u*v)/S with error less than EwhpE_wh_p, where Ew=S(3Es+2)<28 2γT2LE_w=S(3E_s+2)<28\,2^\gamma T^2L, and ∥w~∥<1\|\widetilde w\|<1. After the exact second scaling by 22b+4S2^{2b+4}S, the represented coefficients differ from the true integer coefficients cjc_j by less than 448b 2−b+γ≤448b 2−3b/4<12448b\,2^{-b+\gamma}\le448b\,2^{-3b/4}<\frac12, so rounding Hj/2pH_j/2^p to the nearest integer recovers each cjc_j exactly. The carry recurrence k0=0k_0=0, dj=(cj+kj) mod Q0d_j=(c_j+k_j)\bmod Q_0, kj+1=⌊(cj+kj)/Q0⌋k_{j+1}=\lfloor (c_j+k_j)/Q_0\rfloor satisfies 0≤kj≤q(Q0−1)<Q020\le k_j\le q(Q_0-1)<Q_0^2 and ∑h<jchQ0h=∑h<jdhQ0h+kjQ0j\sum_{h<j}c_hQ_0^h=\sum_{h<j}d_hQ_0^h+k_jQ_0^j for all j≤Sj\le S, so the digits djd_j are exactly the radix-Q0Q_0 digits of the product, which has exactly 2n2n bits after removing zero padding above position 2n−12n-1.

In plain English

The computed scaled result w~\widetilde w is within EwhpE_wh_p of w=(u∗v)/Sw=(u*v)/S, with Ew<28 2γT2LE_w<28\,2^\gamma T^2L and ∥w~∥<1\|\widetilde w\|<1. After the second scaling the coefficient error is below 448b 2−3b/4<12448b\,2^{-3b/4}<\tfrac12, so rounding recovers each integer coefficient cjc_j, and the carry recurrence then yields exactly the radix-Q0Q_0 digits of the 2n2n-bit product.

Why it's here

This closes the correctness argument: the stage-wise error bounds and norm margins from the disk-margin claim are summed into one error bound for w~\widetilde w. The exact identification of ww with (u∗v)/S(u*v)/S comes from the two-scalings claim, and the ring-product lemma supplies the single-truncation error behind the constants. Since the error is below 1/2, nearest-integer rounding is exact, and an induction on the carry recurrence shows the digits djd_j form the true product.
Classified routine:
Standard final step of FFT-based multiplication: the accumulated error bounds from the earlier claims are summed, error below 1/2 lets rounding recover the integer coefficients, and an ordinary carry-propagation induction yields the digits (as in Schönhage–Strassen 1971 and Harvey–van der Hoeven 2021).

Uses

claimDisk margins and error propagation through transformsclaimTwo scalings by S undo normalizationslemChirp identity and source permutation cancellationlemExact negacyclic product with one truncation

Used by

claimCost table yields the final time bound

Sources

PaperOpen
Section
§9.7.2 The final integer coefficients
Page
—
Label
—
Line
sections/08-assembly.tex:677
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Final error below 1/2, rounding and carries exact" rests on claim-thm-main-8
  • info
    inferred_dep
    outline: "Final error below 1/2, rounding and carries exact" rests on claim-thm-main-7
  • info
    inferred_dep
    outline: "Final error below 1/2, rounding and carries exact" rests on lem:chirp-permutation
  • info
    inferred_dep
    outline: "Final error below 1/2, rounding and carries exact" rests on lem:signed-ring-product