Moving a list of Gaussian integers to the output stack

Proved

NLogN.FW.mvPairs_spec

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

harvey-van-der-hoeven-tminteger-multiplicationturing-machines

Let $Z$ be a list of $N\cdot 2^e$ pairs of integers stored on stack KO, registers NN and KR holding $N$ and $2^e$ , and suppose all coordinates, $N2^e$ and $N$ have bit length $\le W$ and $e+1\le W$ . Then the loop mvPairs moves $Z$ (reversed) onto OUT within cost $8000(W+2) + N2^e\cdot 40000(W+2) + 32$ .

Formalization Note. The machine layer: IState HS is a state with $64$ stacks of items (Item = integer or mark), an input position and an output; RM programs (straight-line register code RS, loops rep, conditionals, calls of the multiplication procedure through a MulSpec $M$ giving its domain and cost) have a functional semantics p.run s, a definedness predicate p.ok M s and a cost p.cost M s; Spec M p s s' c abbreviates p.ok M s ∧ p.run s = s' ∧ p.cost M s ≤ c. ints L / gints U push an integer list / a list of pairs as items (head = top); zsz z is the bit length of $|z|$ . MulBnd M m Φ says the multiplication procedure accepts all pairs of integers of bit length $\le m$ at cost $\le Φ$ . Register names (GU, CR, KB, XN, …) are fixed stack indices.

Preamble

-- Harvey–van der Hoeven multitape-TM development (NLogN), generated by skeleton subtraction.

import Definitions.Def_IntMul_HvdH_M_Defs4

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
open NLogN
open NLogN.FW
open IntMul IntMul.HvdH NLogN

Formal statement

theorem NLogN.FW.mvPairs_spec (M : MulSpec) (N e W : ℕ) (s : IState HS) (Z : List (ℤ × ℤ)) (RK LN LR : List Item)
    (hZl : Z.length = N * 2 ^ e) (hK : s.G KO = gints Z ++ RK) (hN : s.G NN = .int (N : ℤ) :: LN)
    (hR : s.G KR = .int ((2 ^ e : ℕ) : ℤ) :: LR)
    (hZW : ∀ p ∈ Z, zsz p.1 ≤ W ∧ zsz p.2 ≤ W) (hNW : zsz ((N * 2 ^ e : ℕ) : ℤ) ≤ W)
    (hNW1 : zsz (N : ℤ) ≤ W) (heW : e + 1 ≤ W) :
    Spec M mvPairs s ((s.upd KO RK).upd OUT (gints Z.reverse ++ s.G OUT))
      (8000 * (W + 2) + N * 2 ^ e * (40000 * (W + 2)) + 32) := by sorry

Source

D. Harvey, J. van der Hoeven, Integer multiplication in time O(n log n), Ann. of Math. 193 (2021), 563–617 (Theorem 1.1: multitape Turing machine multiplication in O(n log n)). Lemma `NLogN.FW.mvPairs_spec` of the Lean development NLogN/HFW8.lean (lines 246–304), written for the prove2.me integer-multiplication campaign.

View graph