claimroutineinferred_dep

Clock gap pays band path length

Band path cost is at most C0+C1(t−j)C_0+C_1(t-j), giving linear clock-gap storage
yields the storage bound of the multiplication lemma
Claim·§10.3 Multiplication by minimum-index bands·inside lemMultiplication with linear clock-gap storage

Statement (paper)

For an original input digit at an operand place jj in a positive band DD, the full path cost through the bands up to DD, which is at most C(D+1)C(D+1) for a fixed constant CC, is bounded by C0+C1(t−j)C_0+C_1(t-j) for fixed constants C0,C1C_0,C_1; the zero band has constant depth and only constant overshoot. Consequently the suspended storage at jj is O(1)+c(t−j)O(1)+c(t-j), and every intrinsic path and local word width is O(t+1)O(t+1).

In plain English

For an input digit at operand place jj in a positive band DD, the total path cost through bands up to DD (at most C(D+1)C(D+1)) is bounded by C0+C1(t−j)C_0+C_1(t-j), and the zero band costs only a constant. Hence suspended storage at jj is O(1)+c(t−j)O(1)+c(t-j) and all intrinsic path and local word widths are O(t+1)O(t+1).

Why it's here

This is the accounting step that ties the band circuit's path length to the clock gap t−jt-j, so the long product expansion costs no more than a linear term in t−jt-j. Combined with the path-only storage bound of the depth-first evaluation lemma and the per-band depth and width bounds from the gate-indexing claim, it gives the storage bound stated in the multiplication lemma.
Classified routine:
A bookkeeping step inside the multiplication lemma: it combines the per-band depth and width bounds from the gate-indexing claim with the path-only storage bound of depth-first circuit evaluation, using the fact that band index D grows linearly in the clock gap t-j.

Uses

lemDepth-first circuit evaluation uses path-only storageclaimGate indexing and adder trees per band

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Clock gap pays band path length" rests on claim-lem-arith-multiplication-4