Exact negacyclic multiplication through a Fermat-type modulus

Proved

IntMul.HvdH.fermatNegaMul_eq

by xuanji · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

integer-multiplication

Let $n,P\ge1$ and let $u,v\in\mathbb Z^n$ have entries of absolute value at most $M$ , where $4nM^2<2^P$ . Put $B=2^P$ and $F=B^n+1$ . The algorithm fermatNegaMul evaluates $u,v$ at $y=B$ (so $y^n\equiv-1\pmod F$ ). It reduces both values modulo $F$ , multiplies them modulo $F$ , takes the balanced residue in $(-F/2,F/2]$ , and reads off $n$ balanced base- $B$ digits. It returns exactly the coefficients of the product in $\mathbb Z[y]/(y^n+1)$ :

w_k=\sum_{i\le k}u_iv_{k-i}-\sum_{k<i<n}u_iv_{k+n-i}\qquad(0\le k<n).

So a negacyclic polynomial product costs one multiplication modulo the Fermat-type number $2^{nP}+1$ . This replaces the Kronecker step of Lemma 2.5 of Harvey–van der Hoeven when the pointwise products are done exactly.

Preamble

import Definitions.Def_IntMul_HvdH_Fermat

Formal statement

namespace IntMul.HvdH
theorem fermatNegaMul_eq (P n : ℕ) (u v : List ℤ) (M : ℤ) (hn : 1 ≤ n) (hP1 : 1 ≤ P)
    (hu : u.length = n) (hv : v.length = n) (hM0 : 0 ≤ M)
    (hub : ∀ x ∈ u, |x| ≤ M) (hvb : ∀ x ∈ v, |x| ≤ M) (hP : 4 * n * M ^ 2 < 2 ^ P) :
    fermatNegaMul P n u v = negFold n (polyMul u v) := by sorry
end IntMul.HvdH

Source

Harvey, van der Hoeven, Integer multiplication in time O(n log n), Annals of Math. 193 (2021), https://hal.science/hal-02070778, Lemma 2.5 (variant)

View graph