Section 30.2 - The DFT and FFT

The generic algebraic core works over characteristic-zero fields: primitive roots supply orthogonality, the positive-exponent CLRS transform is polynomial evaluation at powers of a root, and idft gives both inverse directions. Fourier-space pointwise multiplication is connected to cyclic convolution and, under an explicit capacity premise, to ordinary polynomial multiplication. The actual radix-2 FFT recursively splits even and odd coefficients, reuses a successively generated twiddle trace, combines the children through a butterfly layer, and supplies an inverse agreeing with idft. Its arithmetic counters are projections of the same execution: each counter is exactly k * 2^k, and zero padding lifts the total work to an all-input Theta(n log n) theorem.

complexDft_mathlib is the separate compatibility boundary with Mathlib's complex ZMod.dft; its statement exposes the required output-index sign change. The generic FFT multiplication execution is correct under the minimal no-wrap capacity premise; the complex wrapper constructs a sufficient power-of-two capacity and primitive root internally. The multiplication work field charges three recursive transforms, pointwise products, and inverse scaling, with an exact composition and an all-input Theta(n log n) bound. Section 30.3 builds the iterative and layered-circuit refinements on this recursive core.

Implementation pages:

• Roots of unity

• Generic DFT and complex compatibility

• Inversion and convolution

• Recursive radix-2 FFT

• Recursive FFT definitions

• Recursive FFT correctness

• Recursive FFT costs

• FFT polynomial multiplication