claimroutineinferred_dep

Band recursion yields approximation integer

Finite band recursion gives an integer NtN_t approximating xyxy at scale tt
turns the banded product into a concrete integer computation
Claim·§10.3 Multiplication by minimum-index bands·inside lemMultiplication with linear clock-gap storage

Statement (paper)

There are only finitely many nonempty retained bands, and each positive nonempty band satisfies D≤47(t+h∘)D\leq\frac47(t+h_\circ). Define the integers FDF_D and NtN_t by the recursion FD=SD+⌊2hD−hD+FD+⌋F_D=S_D+\lfloor 2^{h_D-h_{D^+}}F_{D^+}\rfloor and Nt=⌊2−h0F0⌋N_t=\lfloor2^{-h_0}F_0\rfloor, starting from the most distant retained band with zero missing tail. Then the integer NtN_t satisfies Equation  for z=xyz=xy, since the difference between 2−h0F02^{-h_0}F_0 and the sum of all retained terms in scale-tt units is at most ∑D2−hD\sum_D2^{-h_D}, the error before the final floor is less than 1/21/2, and the final floor costs less than one more unit.

In plain English

Only finitely many retained bands are nonempty, and each positive nonempty band DD satisfies D≤47(t+h∘)D\leq\frac47(t+h_\circ). The recursion FD=SD+⌊2hD−hD+FD+⌋F_D=S_D+\lfloor 2^{h_D-h_{D^+}}F_{D^+}\rfloor, started at the farthest retained band, and Nt=⌊2−h0F0⌋N_t=\lfloor2^{-h_0}F_0\rfloor produce an integer NtN_t that approximates z=xyz=xy at scale tt as required by Equation (arith-approximation).

Why it's here

This turns the band-truncated product into a concrete finite computation of integers. The omitted tail is already below 1/21/2 by the previous band-decomposition claim. The floors in the recursion add at most ∑D2−hD\sum_D 2^{-h_D} of error, which keeps the error before the final floor under 1/21/2. The final floor then costs less than one more unit, so the total error fits the approximation requirement, and later claims can implement the recursion with small storage.
Classified routine:
Routine error bookkeeping for a truncated product computed by a floor-based recursion, following directly from the band-decomposition tail bound of the previous claim and a geometric bound on the accumulated floor errors.

Uses

claimBand decomposition bounds multiplication tail error

Used by

claimSigned floor shifts preserve residues

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Band recursion gives approximation integers" rests on claim-lem-arith-multiplication-1