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

### License

BSD License

### Topics

- Computer science/Algorithms/Mathematical

### Session Number_Theoretic_Transform

- Preliminary_Lemmas
- NTT
- Butterfly

### Depends on

- The Factorization Algorithm of Berlekamp and Zassenhaus

### Used by

- Schönhage-Strassen Multiplication
- CRYSTALS-Kyber

### Auto-related entries

- CRYSTALS-Kyber

## Cite

×

Number_Theoretic_Transform-AFP

    @article{Number_Theoretic_Transform-AFP,
      author  = {Thomas Ammer and Katharina Kreuzer},
      title   = {Number Theoretic Transform},
      journal = {Archive of Formal Proofs},
      month   = {August},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Number_Theoretic_Transform.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Sep 7, 2022 : Isabelle2021-1