Abstract
This entry contains an Isabelle formalization of the Number Theoretic Transform (NTT) which is the analogue to a Discrete Fourier Transform (DFT) over a finite field. Roots of unity in the complex numbers are replaced by those in a finite field.
First, we define both NTT and the inverse transform INTT in Isabelle and prove them to be mutually inverse.
DFT can be efficiently computed by the recursive Fast Fourier Transform (FFT). In our formalization, this algorithm is adapted to the setting of the NTT: We implement a Fast Number Theoretic Transform (FNTT) based on the Butterfly scheme by Cooley and Tukey. Additionally, we provide an inverse transform IFNTT and prove it mutually inverse to FNTT.
Afterwards, a recursive formalization of the FNTT running time is examined and the famous $O(n \log n)$ bounds are proven.