claimroutineinferred_dep

Gate indexing and adder trees per band

Band gates indexed by

(r,s,o)

with adder trees of depth

O(\log^2 D)

turns the residue recursion into a describable circuit

Claim·§10.3 Multiplication by minimum-index bands·inside lemMultiplication with linear clock-gap storage

Statement (paper)

For each band the finite gate structure can be indexed without storing an absolute operand place at each gate: the triples

(r,s,o)

with

D\leq r<2D

t-q<s\leq t+h_D

o\in\{0,1\}

enumerate the relevant pairs exactly once (with the analogous enumeration using

r=0

for the zero band), the offsets

r-D

s-(t-q+1)

and

o

have

O(\log(D+2))

bits and are obtained from paths in padded binary selection trees, and the full places are computed from the root clock in scratch. Each nonzero term is a constant-bit signed product

x_iy_j

shifted into a word of width

W_D=q+h_D=O(D+1)

interpreted modulo

2^{W_D}

, and adding these words and the shifted tail by Equation gives a band depth of

O(\log^2(D+2))

In plain English

In each band the gates can be indexed by triples

(r,s,o)

with

D\leq r<2D

t-q<s\leq t+h_D

o\in\{0,1\}

, which list the relevant pairs exactly once (using

r=0

for the zero band), with offsets of

O(\log(D+2))

bits. Each nonzero term is a constant-bit signed product

x_iy_j

placed in a word of width

W_D=q+h_D=O(D+1)

modulo

2^{W_D}

, and summing these words plus the shifted tail gives band depth

O(\log^2(D+2))

Why it's here

This turns the small-residue band recursion from the previous claim into an actual circuit that can be described with little storage. Offsets come from paths in padded binary selection trees and absolute places are recomputed from the root clock in scratch, so no gate stores a full operand place. The adder-tree bound then gives the per-band depth that the next claim uses to compare against the clock gap.

Classified routine:

Standard circuit bookkeeping: gates are indexed by small offsets, and the depth bound comes from adding O(D)-bit words with logarithmic-depth adder trees (Eq. arith-adder-depth). This is a direct implementation of the band recursion from the previous claim.

Uses

claimSigned floor shifts preserve residues

Used by

claimClock gap pays band path length

Sources

PaperOpen

Section: §10.3 Multiplication by minimum-index bands
Page: —
Label: —
Line: sections/arithmetic.tex:359

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Gate indexing and adder trees per band" rests on claim-lem-arith-multiplication-3