Fermat-ring FFT multiplication recovers the negacyclic convolution of the pieces

Proved

NLogN.ss_lift

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

integer-multiplicationschonhage-strassen-tmturing-machines

Let $n\ge 1$ , $k,Q,M\in\mathbb N$ with $2^kQ=n$ , and write $F=2^n+1$ , $K=2^k$ . Assume

2\,(2^k)^2\,(2^M)^2 < 2^{n-1}.

Then for all integers $x,y$ , with $\hat x = \mathrm{difZ}(F,2Q,k,\mathrm{wtZ}(F,Q,0,\mathrm{pcs}(M,K,x)))$ and $\hat y$ defined likewise,

\mathrm{liftL}\big(n,k,Q,K,\ \mathrm{ditZ}(F,n,2Q,k,\ \mathrm{pmulZ}(F,\hat x,\hat y))\big) = \mathrm{ncZ}\big(K,\ \mathrm{pcs}(M,K,x),\ \mathrm{pcs}(M,K,y)\big).

In words: cutting $x$ and $y$ into $K$ signed $M$ -bit pieces, twisting by powers of $2^Q$ , applying the forward FFT, multiplying pointwise mod $F$ , applying the inverse FFT, untwisting, scaling by $K^{-1}$ and lifting to the symmetric range yields exactly (as integers, not only mod $F$ ) the negacyclic convolution

\mathrm{ncZ}(K,a,b)_m = \sum_{i+l=m} a_i b_l - \sum_{i+l=m+K} a_i b_l,\qquad 0\le m<K.

This is the algebraic heart of the Schönhage–Strassen correctness proof: the convolution theorem for the Fermat-ring transform with root $2^{2Q}$ and twist $2^Q$ (whose $K$ -th power is $2^n\equiv-1$ ), together with the size bound guaranteeing that the coefficients $|\mathrm{ncZ}_m|\le K\,2^{2M}$ are recovered exactly from their residues.

Formalization Note. A purely mathematical statement on lists of integers; difZ, ditZ, wtZ, pmulZ, liftL are the reference functions that the item-language procedures are proved to compute, pcs uses signed (sign of $x$ ) truncating pieces, and % is the canonical nonnegative residue.

Preamble

-- Schönhage–Strassen multitape-TM development (NLogN), generated by skeleton subtraction.

import Definitions.Def_IntMul_SS_Defs2

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open NLogN
open IntMul

Formal statement

theorem NLogN.ss_lift (n k Q M : ℕ) (x y : ℤ) (hn : 1 ≤ n) (hKQ : 2 ^ k * Q = n)
    (hb : 2 * ((2 : ℤ) ^ k) ^ 2 * ((2 : ℤ) ^ M) ^ 2 < 2 ^ (n - 1)) :
    liftL n k Q (2 ^ k) (ditZ (2 ^ n + 1) n (2 * Q) k (pmulZ (2 ^ n + 1)
      (difZ (2 ^ n + 1) (2 * Q) k (wtZ (2 ^ n + 1) Q 0 (pcs M (2 ^ k) x)))
      (difZ (2 ^ n + 1) (2 * Q) k (wtZ (2 ^ n + 1) Q 0 (pcs M (2 ^ k) y))))) =
      ncZ (2 ^ k) (pcs M (2 ^ k) x) (pcs M (2 ^ k) y) := by sorry

Source

A. Schönhage, V. Strassen, Schnelle Multiplikation großer Zahlen, Computing 7 (1971), 281–292 (main theorem: O(n log n log log n) multitape TM multiplication). Lemma `NLogN.ss_lift` of the Lean development NLogN/SSCorrect.lean (lines 17–79), written for the prove2.me integer-multiplication campaign.

View graph