Moving K integer items between stacks in linear time

Proved

NLogN.mvK_runs

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

integer-multiplicationschonhage-strassen-tmturing-machines

Let $X\neq Y$ be stacks, both different from CC, T3 and DL. Let $A$ be a list of integers each of bit length at most $m$ (Bnd m A). Assume $X$ holds the items of $A$ (first entry on top) over $R$ , and DL has $|A|$ on top. Then mvK X Y runs from $s$ to

s\big[X := R\big]\big[Y := \mathrm{reverse}(\mathrm{ints}\ A)\mathbin{+\!\!+}s.G\,Y\big]

(the block is moved and reversed), with cost at most

|A|\cdot 1000\,(m+|{|A|}|_2+3)+300\,(|{|A|}|_2+1)+40,

where $|{|A|}|_2$ is the bit length of the length $|A|$ .

Block moves of the $K=2^k$ coefficient vectors between the work stacks occur several times per level of the Schönhage–Strassen procedure; the bound is linear in the total size of the moved data plus counter overhead.

Formalization Note. States are IState NS records with item stacks G : Fin NS → List Item (head = top), input pointer ip and output out; s.upd X L replaces stack X by L; ints A is the list of integer items of A. The named stacks (ARG, PRM, RN, RF, DX, DL, …) are fixed indices in Fin 32. IRuns I iprog p s s' c means that p executes from s to exactly s' with some cost $c' \le c$ , so costs are upper bounds; the program text iprog and input I are arbitrary unless constrained.

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
variable {P : ℕ} {I : List Sym} {iprog : Fin P → IStmt NS P}

Formal statement

theorem NLogN.mvK_runs {X Y : Fin NS} (hXY : X ≠ Y) (hXC : X ≠ CC) (hYC : Y ≠ CC) (hX3 : X ≠ T3)
    (hY3 : Y ≠ T3) (hXH : X ≠ DL) (hYH : Y ≠ DL) (s : IState NS) (A : List ℤ) (R LH : List Item)
    (m : ℕ) (hX : s.G X = ints A ++ R) (hH : s.G DL = .int A.length :: LH) (hA : Bnd m A) :
    IRuns I iprog (mvK X Y) s ((s.upd X R).upd Y ((ints A).reverse ++ s.G Y))
      (A.length * (1000 * (m + zsz (A.length : ℤ) + 3)) + 300 * (zsz (A.length : ℤ) + 1) + 40) := 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.mvK_runs` of the Lean development NLogN/SSFM1.lean (lines 57–76), written for the prove2.me integer-multiplication campaign.

View graph