claimroutineinferred_dep
Final error below 1/2; rounding and carries exact
Total error is below , 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 approximates with error less than , where , and . After the exact second scaling by , the represented coefficients differ from the true integer coefficients by less than , so rounding to the nearest integer recovers each exactly. The carry recurrence , , satisfies and for all , so the digits are exactly the radix- digits of the product, which has exactly bits after removing zero padding above position .
In plain English
The computed scaled result is within of , with and . After the second scaling the coefficient error is below , so rounding recovers each integer coefficient , and the carry recurrence then yields exactly the radix- digits of the -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 . The exact identification of with 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 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).