Prove2Me

Multiplication in A[y]/(yr+1)A[y]/(y^r+1) is negacyclic convolution of coefficients

Proved
IntMul.HvdH.eval_negacyclic

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

integer-multiplication

Let AA be a commutative ring, r≥1r\ge1, and z∈Az\in A with zr=−1z^r=-1 (for example z=yz=y in A[y]/(yr+1)A[y]/(y^r+1)). For coefficient vectors a,b:Z/r→Aa,b:\mathbb Z/r\to A,

(∑jajzjˉ)(∑jbjzjˉ)=∑j(∑kakbj−ksk,j)zjˉ,\Big(\sum_j a_jz^{\bar j}\Big)\Big(\sum_j b_jz^{\bar j}\Big)=\sum_j\Big(\sum_k a_kb_{j-k}s_{k,j}\Big)z^{\bar j},

with sk,j=1s_{k,j}=1 if kˉ≤jˉ\bar k\le\bar j and −1-1 otherwise. So multiplication in the synthetic coefficient ring C[y]/(yr+1)\mathbb C[y]/(y^r+1) of Harvey–van der Hoeven (§2.3) is negacyclic convolution on coefficient vectors, as used in Lemma 2.5 and Proposition 3.4.

Preamble
import Mathlib
Formal statement
namespace IntMul.HvdH
theorem eval_negacyclic {A : Type*} [CommRing A] (r : ℕ) [NeZero r] (z : A) (hz : z ^ r = -1)
    (a b : ZMod r → A) :
    (∑ j, a j * z ^ j.val) * (∑ j, b j * z ^ j.val) =
      ∑ j, (∑ k, a k * b (j - k) * (if k.val ≤ j.val then 1 else -1)) * z ^ j.val := 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, Sections 2.3 and 3.2 (Proposition 3.5, map S)

View graph