lemmaroutine

Multiplication with linear clock-gap storage

Multiplication keeps suspended storage O(1)+c(t−j)O(1)+c(t-j) despite long expansion
multiplication primitive for reciprocal and interface
Lemma·lem:arith-multiplication·§10.3 Multiplication by minimum-index bands

Statement (paper)

For normalized exact input streams xx and yy, multiplication has all the conclusions of Lemma . In particular, its suspended storage at an operand place jj is O(1)+c(t−j)O(1)+c(t-j), despite the potentially long product expansion.

In plain English

For normalized exact input streams xx and yy, the product stream has all the properties of the elementary arithmetic operations. In particular, the storage suspended at an operand place jj is O(1)+c(t−j)O(1)+c(t-j), even though the product expansion is long.

Why it's here

Multiplication is the one primitive whose naive expansion has far too many term pairs, so it needs separate treatment. The proof groups term pairs into bands by minimum index, truncates the tail with error under half a unit, and evaluates each band as a small-residue adder tree. The band path cost is then charged to the clock gap t−jt-j, so the depth-first evaluation lemma gives the linear storage bound that later results (reciprocal, the uniform interface) rely on.
Classified routine:
The proof is a technical adaptation of known techniques. It groups term pairs by minimum index and truncates the tail, which is standard bookkeeping for multiplying digit streams. It then evaluates the bands with the paper's depth-first, path-only circuit evaluation lemma and charges the cost to the clock gap.

Uses

lemDepth-first circuit evaluation uses path-only storage

Used by

lemReciprocal with early-word storageclaimClipped reciprocal approximation has exact streamsclaimSuffix branch holds no coefficient wordclaimOne clock coefficient works throughout

Inside the proof

claimBand decomposition bounds multiplication tail errorclaimBand recursion yields approximation integerclaimSigned floor shifts preserve residuesclaimGate indexing and adder trees per bandclaimClock gap pays band path length

Sources

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

Phase 2 aligns this node to a Lean declaration.