Number Theoretic Transform

Thomas Ammer and Katharina Kreuzer

August 18, 2022

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.

BSD License


Theories of Number_Theoretic_Transform