Chapter 30 - Polynomials and the FFT

Sections 30.1--30.3 are complete within the exact generic-arithmetic functional boundary. The 46 tracked theorem groups are all kernel checked; the chapter has no remaining main-text group inside this reviewed model.

Proof architecture

The development follows the textbook dependency chain. Section 30.1 fixes coefficient and point-value representations and proves their bridges and operations. Section 30.2 builds generic DFT algebra on those representations, proves inversion and convolution, implements the recursive radix-2 FFT, and uses it for polynomial multiplication. Section 30.3 factors the same transform into bit-reversal copying and globally ordered iterative stages, then stores those stages as an evaluated layered circuit whose size and depth are read from the same syntax.

Section 30.1 - Representing polynomials

• CLRS.­Chapter30.­coeffVector_vectorToPolynomial and CLRS.­Chapter30.­vectorToPolynomial_coeffVector give the fixed-capacity coefficient round trips.

• CLRS.­Chapter30.­interpolate_pointValues_roundTrip proves the distinct-node interpolation round trip.

• CLRS.­Chapter30.­hornerEval_correct connects Horner evaluation to polynomial evaluation.

• CLRS.­Chapter30.­schoolbookMul_correct and CLRS.­Chapter30.­schoolbookMulWork_exact prove schoolbook multiplication and its exact represented work.

Section 30.2 - The DFT and recursive FFT

• CLRS.­Chapter30.­idft_dft, CLRS.­Chapter30.­dft_idft, and CLRS.­Chapter30.­dft_cyclicConvolution provide the Fourier algebra.

• CLRS.­Chapter30.­recursiveFFT_eq_dft proves the executable recursive radix-2 transform computes the generic DFT.

• CLRS.­Chapter30.­complexFFTMultiply_correct gives the unconditional automatically padded complex polynomial-multiplication wrapper.

• CLRS.­Chapter30.­paddedFFTWork_allInput_bigTheta and CLRS.­Chapter30.­fftMultiplyWork_allInput_bigTheta give the all-input Theta(n log n) work bounds.

Section 30.3 - Iterative FFT and the layered network

• CLRS.­Chapter30.­bitReverseEquiv_testBit and CLRS.­Chapter30.­bitReverseCopy_involutive specify bit reversal.

• CLRS.­Chapter30.­iterativeRadix2FFT_eq_recursiveFFT and CLRS.­Chapter30.­iterativeRadix2FFT_eq_dft close the iterative algorithmic and algebraic bridges.

• CLRS.­Chapter30.­iterativeRadix2FFTExec_totalWork and CLRS.­Chapter30.­paddedIterativeFFTWork_allInput_bigTheta attach exact and asymptotic work to the executed iterative transform.

• CLRS.­Chapter30.­fftNetwork_eval, CLRS.­Chapter30.­fftNetwork_butterflyCount, and CLRS.­Chapter30.­fftNetwork_primitiveDepth connect the stored circuit to transform semantics, exact size, and exact depth.

Cost conventions

The functional and circuit models intentionally charge different objects:

• recursive or iterative arithmetic work is 2 * k * 2^k;

• iterative total work, including bit-reversal moves, is 2^k + 2 * k * 2^k;

• the layered circuit contains k * 2^(k-1) butterflies and 3 * k * 2^(k-1) primitive arithmetic gates; and

• butterfly depth is k, while primitive arithmetic depth is 2 * k.

Execution charges successive twiddle generation and data movement. Circuit counting treats fixed twiddle powers as constants and bit reversal as wiring.

Reviewed boundary

The represented algorithms are pure functions over fixed-length and power-of-two vectors, over exact generic ring or characteristic-zero field arithmetic as required by each theorem. Mutable arrays, aliasing, imperative loops, RAM/cache/allocator and hardware costs, floating-point approximation and numerical stability, concrete parallel scheduling, number-theoretic-transform specialization, external code generation, exercises, and Problems 30-1 through 30-6 are optional extension tracks rather than missing core groups.