claimroutineinferred_dep

Prefix-slot rounds evaluated bit by bit

Prefix-slot rounds run bit by bit in O(TpdK)O(TpdK) total
handles slots the parallel layers cannot
Claim·§6.2 A layout on which the parallel layers apply·inside lemCost and accuracy of synthetic transform

Statement (paper)

Each round on prefix slots, forward or opposite, can be carried out by processing its participating bits individually, using O(p)O(p) bits per component without truncating between axes (after s≤D≤ds\leq D\leq d individual H0H_0 factors the coefficients are exact dyadics on the 2−(p+s)2^{-(p+s)} grid inside the disk), applying QpQ_p once at the end of the round and writing the disk-grid numerators in the supplied ww-bit component format. Such a round costs O(Tp)O(Tp), and since there are at most b+1≤Kb+1\leq K rounds on prefix slots, the total cost of the prefix-slot rounds is O(TpdK)O(TpdK).

In plain English

Each forward or opposite round acting on the prefix slots can be done exactly by processing its participating bits one at a time, with O(p)O(p) bits per component and a single truncation QpQ_p at the end of the round. Each such round costs O(Tp)O(Tp), so the at most b+1≤Kb+1\leq K prefix-slot rounds cost O(TpdK)O(TpdK) in total.

Why it's here

After the layout permutation of the previous claim places the low slots in a prefix, these rounds cannot use the chunked parallel layers, so they are handled directly. Since after s≤D≤ds\leq D\leq d individual H0H_0 factors the coefficients are exact dyadics on the 2−(p+s)2^{-(p+s)} grid, no intermediate truncation is needed, and only one QpQ_p per round enters the error analysis, which the next claim uses to get the ℓ\ell error bound.
Classified routine:
This is a direct cost and exactness bookkeeping step. It applies the individual H_0 butterfly factors to dyadic numbers on a fixed grid and truncates once per round, then sums the O(Tp) cost over the at most b+1 rounds, following the layout set up in the previous claim.

Uses

claimLayout permutation by moves and chunk exchanges

Used by

claimOne truncation per round bounds error

Sources

PaperOpen
Section
§6.2 A layout on which the parallel layers apply
Page
—
Label
—
Line
sections/06-transforms.tex:348
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Prefix-slot rounds evaluated individually and exactly" rests on claim-lem-synthetic-transform-cost-1