claimroutineinferred_dep

Signed floor shifts preserve residues

Floor shifts commute with residues, so bands need only O(D)O(D)-bit residues
lets the band recursion run with small storage
Claim·§10.3 Multiplication by minimum-index bands·inside lemMultiplication with linear clock-gap storage

Statement (paper)

For h′≥hh'\geq h and signed integers a,ba,b with a−b=k2q+h′a-b=k2^{q+h'}, one has ⌊a/2h′−h⌋−⌊b/2h′−h⌋=k2q+h\lfloor a/2^{h'-h}\rfloor-\lfloor b/2^{h'-h}\rfloor=k2^{q+h}. Consequently, Equation  can be implemented using residues with modulus 2q+hD2^{q+h_D} at band DD, processing only the diagonals t−q<i+j≤t+hDt-q<i+j\leq t+h_D (giving O((D+1)2)O((D+1)^2) candidate pairs), and the residue Nt mod 2qN_t\bmod2^q is obtained, since a next-band residue modulo 2q+h′2^{q+h'} determines the floor-shifted tail modulo 2q+h2^{q+h}, even when the underlying integers are negative.

In plain English

If h′≥hh'\geq h and signed integers a,ba,b satisfy a−b=k2q+h′a-b=k2^{q+h'}, then ⌊a/2h′−h⌋−⌊b/2h′−h⌋=k2q+h\lfloor a/2^{h'-h}\rfloor-\lfloor b/2^{h'-h}\rfloor=k2^{q+h}. Hence the band recursion can be run with residues modulo 2q+hD2^{q+h_D} at band DD, using only the diagonals t−q<i+j≤t+hDt-q<i+j\leq t+h_D (so O((D+1)2)O((D+1)^2) candidate pairs), and still yields Nt mod 2qN_t\bmod 2^q, even for negative integers.

Why it's here

This makes the exact integer recursion from the previous claim implementable with small storage. A residue modulo 2q+h′2^{q+h'} at the next band determines the floor-shifted tail modulo 2q+h2^{q+h}, so each band need only keep a bounded-width residue instead of the full integer, and signs cause no trouble. This bounds the work per band and feeds the gate-indexing and adder-tree construction in the next claim.
Classified routine:
Elementary arithmetic: ⌊(b+m2s)/2s⌋=⌊b/2s⌋+m\lfloor (b+m2^s)/2^s\rfloor=\lfloor b/2^s\rfloor+m for integers, with m=k2q+hm=k2^{q+h} and s=h′−hs=h'-h. Combined with the band recursion from the previous claim, this is standard modular bookkeeping for carrying truncated residues in a multiplication circuit.

Uses

claimBand recursion yields approximation integer

Used by

claimGate indexing and adder trees per band

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Residue implementation with signed floor shifts" rests on claim-lem-arith-multiplication-2