lemmastandard

Roots of unity orthogonality and inverse transforms

Roots of unity sum to tt or 00, so Ft+Ft−=t−1IF_t^+F_t^-=t^{-1}I
makes forward and opposite transforms inverse
Lemma·lem:synthetic-characters·§6.1 Roots, butterflies, and stored frequency order

Statement (paper)

If jj is an integer, then ∑k=0t−1ωtjk={t,t∣j,0,t∤j.Ft+Ft−=t−1I. \sum_{k=0}^{t-1}\omega_t^{jk} =\begin{cases}t,&t\mid j,\\0,&t\nmid j.\end{cases} \qquad F_t^+F_t^-=t^{-1}I.

In plain English

For an integer jj, the sum ∑k=0t−1ωtjk\sum_{k=0}^{t-1}\omega_t^{jk} equals tt if tt divides jj and 00 otherwise. Consequently the opposite-sign transforms satisfy Ft+Ft−=t−1IF_t^+F_t^-=t^{-1}I.

Why it's here

This is the standard character-orthogonality fact, here established for the paper's synthetic roots ωt\omega_t. It shows the forward and opposite transforms invert each other up to the scalar t−1t^{-1}, which the transform-cost and convolution results rely on to recover exact products after pointwise multiplication.
Classified standard:
Orthogonality of roots of unity (geometric-series identity) and the resulting DFT inversion formula, a textbook fact (e.g., Cooley–Tukey 1965; any text on the discrete Fourier transform), here applied to synthetic roots of unity as in Schönhage–Strassen-style constructions.

Uses

Nothing else in the paper

Used by

claimFull procedures include layout conjugationclaimExact normalization identity via retained order

Sources

PaperOpen
Section
§6.1 Roots, butterflies, and stored frequency order
Page
—
Label
lem:synthetic-characters
Line
sections/06-transforms.tex:52
Leannot aligned

Phase 2 aligns this node to a Lean declaration.