claimroutineinferred_dep

Twiddle rotations without coefficient sorting

Twiddle rotations are signed cyclic shifts costing

O(rp)

per record

keeps twiddle multiplication within the budget

Claim·§6.2 A layout on which the parallel layers apply·inside lemCost and accuracy of synthetic transform

Statement (paper)

For each output record of a forward butterfly round, the descriptor locates the new branch bit

b_i

and the lower named slots encoding

k_i

, so the exponent

E

of is computed from current slot values in

\operatorname{poly}(p)

time per polynomial record, which fits within the scan cost

O(rp)

of the record. Before an opposite round at position

h

, the lower slots again encode the same

k_i

and slot

h

gives

b_i

, so the inverse monomial uses the same exponent. Writing

E=er+s

with

0\leq s<r

, multiplication by

y^E

modulo

y^r+1

, and likewise by

y^{-E}

, is realized by splitting the coefficient list before position

r-s

, putting the tail before the head, negating the moved tail and applying the common sign

(-1)^e

, at cost

O(rp)

per record and with no coefficient sort.

In plain English

The twiddle exponent

E

for each output record of a butterfly round is computable from the descriptor's slot values in

\operatorname{poly}(p)

time, and the inverse round uses the same exponent. Multiplying a record by

y^{\pm E}

modulo

y^r+1

is a signed cyclic rotation of its coefficient list, costing

O(rp)

per record with no sort.

Why it's here

This step shows that the twiddle multiplications in each round cost only a scan of each record, so they fit within the cost budget of the parallel layers on the layout from the earlier claim. Writing

E=er+s

turns the monomial multiplication into splitting the list at

r-s

, moving the tail to the front, negating it and applying the sign

(-1)^e

. The same slot structure gives the same exponent for the opposite round, so the inverse monomial is handled identically. This prepares the per-round cost and truncation accounting in the next claim.

Classified routine:

Multiplication by a monomial y^E modulo y^r+1 is the well-known negacyclic shift used in Schönhage–Strassen-style synthetic FFTs. Here it is checked to cost a linear scan per record on the paper's layout, which is bookkeeping on top of the earlier layout 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:372

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Twiddle exponents and monomial as signed rotation" rests on claim-lem-synthetic-transform-cost-1