### 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.