claimroutineinferred_dep

One truncation per round bounds error

One truncation per round gives total error ≤2 ℓ2−p\le\sqrt2\,\ell2^{-p}
accumulates the transform's error
Claim·§6.2 A layout on which the parallel layers apply·inside lemCost and accuracy of synthetic transform

Statement (paper)

Each forward or opposite round, including the rounds on prefix slots, returns exactly the result of a single truncation QpQ_p applied after the exact contraction round, and the layout permutations are isometries. Starting from zero error, after at most ℓ\ell rounds the computed array differs from the exact one by less than 2 ℓ 2−p\sqrt2\,\ell\,2^{-p} and remains in the disk.

In plain English

Each forward or opposite round, including those on prefix slots, equals the exact contraction round followed by a single truncation QpQ_p, and the layout permutations are isometries. So starting from zero error, after at most ℓ\ell rounds the computed array is within 2 ℓ 2−p\sqrt2\,\ell\,2^{-p} of the exact one and stays in the disk.

Why it's here

The layer rounds and the bit-by-bit prefix-slot rounds each incur just one truncation QpQ_p per round, and the twiddle rotations add no error. Since the layout permutations preserve norms, the per-round errors simply add, giving at most ℓ\ell truncation errors of size at most 2 2−p\sqrt2\,2^{-p} each. This yields the accuracy guarantee of the transform in the parent lemma.
Classified routine:
Standard error accumulation argument: exact contraction (unitary/norm-nonincreasing butterfly) followed by one rounding step per round, with isometric permutations, so errors add linearly (as in classical fixed-point FFT error analyses). It follows directly from the preceding claims on layer rounds and prefix-slot rounds.

Uses

claimEach layout round meets layer hypothesesclaimPrefix-slot rounds evaluated bit by bitclaimTwiddle rotations without coefficient sorting

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "One truncation per round gives ℓ error bound" rests on claim-lem-synthetic-transform-cost-3
  • info
    inferred_dep
    outline: "One truncation per round gives ℓ error bound" rests on claim-lem-synthetic-transform-cost-4
  • info
    inferred_dep
    outline: "One truncation per round gives ℓ error bound" rests on claim-lem-synthetic-transform-cost-5