claimroutine

Band decomposition bounds multiplication tail error

Banding product term pairs drops tail error below 1/2 unit
justifies truncating the long product expansion
Claim·§10.3 Multiplication by minimum-index bands·inside lemMultiplication with linear clock-gap storage

Statement (paper)

Partition the ordered pairs (i,j)(i,j) of nonnegative places into the zero band {min⁡(i,j)=0}\{\min(i,j)=0\} and the positive bands PD={(i,j):D≤min⁡(i,j)<2D}\mathcal P_D=\{(i,j):D\leq\min(i,j)<2D\}, D=1,2,4,…D=1,2,4,\ldots, and retain in band DD only pairs with i+j≤t+hDi+j\leq t+h_D, where h0=h∘h_0=h_\circ and hD=h∘+⌊D/4⌋h_D=h_\circ+\lfloor D/4\rfloor. Then, in units of 2−t2^{-t}, the total absolute sum of the omitted product terms satisfies Eomit≤2A2∑D∈{0,1,2,4,…}(D+1)2−hDE_{\mathrm{omit}}\leq 2A^2\sum_{D\in\{0,1,2,4,\ldots\}}(D+1)2^{-h_D} with A=6A=6, both this series and ∑D2−hD\sum_D 2^{-h_D} converge, and the fixed integer h∘h_\circ can be chosen so that the resulting bound, including the coefficient 2A22A^2, is less than 1/21/2.

In plain English

Split the product's term pairs (i,j)(i,j) into a zero band and positive bands PD\mathcal P_D by min⁡(i,j)\min(i,j), keeping in band DD only pairs with i+j≤t+hDi+j\leq t+h_D. The omitted terms then total at most 2A2∑D(D+1)2−hD2A^2\sum_D (D+1)2^{-h_D} (with A=6A=6) in units of 2−t2^{-t}, this series converges, and h∘h_\circ can be fixed so the bound is below 1/21/2.

Why it's here

This shows that truncating the long product expansion band by band costs less than half a unit in the last place, so the retained terms still give a correctly rounded approximation. The slowly growing offset hD=h∘+⌊D/4⌋h_D=h_\circ+\lfloor D/4\rfloor makes the factor 2−hD2^{-h_D} outweigh the D+1D+1 pairs per band, so the tail sum converges and later claims can work with the finite set of retained bands.
Classified routine:
A geometric-series truncation estimate of the usual kind for schoolbook multiplication error analysis: the omitted terms are bounded by counting pairs per diagonal, and choosing the offset h_D = h_∘ + ⌊D/4⌋ makes the series converge.

Uses

Nothing else in the paper

Used by

claimBand recursion yields approximation integer

Sources

PaperOpen
Section
§10.3 Multiplication by minimum-index bands
Page
—
Label
—
Line
sections/arithmetic.tex:262
Leannot aligned

Phase 2 aligns this node to a Lean declaration.