Stack-machine duplication of an integer item onto another stack

Proved

NLogN.Runs.dupInt

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

integer-multiplicationschonhage-strassen-tmturing-machines

Let $q,i,j,t_1,t_2$ be pairwise distinct stacks of a state $\sigma$ . Assume stack $i$ is $\mathrm{enc}(z)$ followed by $R_i$ for an integer $z$ , where $R_i$ and the tops of $j$ , $t_1$ , $t_2$ do not start with a bit symbol. Then dupInt q i j t1 t2 runs from $\sigma$ to

\sigma\big[j := \mathrm{enc}(z) \mathbin{+\!\!+} \sigma.\mathrm{stk}\ j\big]

(stack $i$ is restored, $z$ is copied on top of $j$ ), with cost at most $\mathrm{dupCost}(|z|_2)+17$ , linear in the bit length $|z|_2$ of $z$ .

This implements the item-language instruction dup, used throughout the Schönhage–Strassen procedures to copy rulers, moduli and counters.

Formalization Note. Machine states are St S records: stacks stk : Fin S → List Sym over the 16-letter alphabet Sym = Fin 16 (head = top), input position ip and output out; σ.set i L replaces stack i. An integer item is stored as (Item.int z).enc: a sign header followed by the minimal binary magnitude, least significant bit nearest the header; bitOf detects bit symbols, and the hypotheses bitOf (…).head? = none say that the following stack content does not start with a bit (so item boundaries are recognisable). Runs I prog p σ σ' c means p runs from σ to exactly σ' with some cost $c'\le c$ ; the procedures prog and input I are arbitrary.

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
variable {S P : ℕ} {I : List Sym} {prog : Fin P → Stmt S P}

Formal statement

theorem NLogN.Runs.dupInt {q i j t1 t2 : Fin S} (hqi : q ≠ i) (hqj : q ≠ j) (hqt1 : q ≠ t1)
    (hqt2 : q ≠ t2) (hij : i ≠ j) (hit1 : i ≠ t1) (hit2 : i ≠ t2) (hjt1 : j ≠ t1) (hjt2 : j ≠ t2)
    (ht12 : t1 ≠ t2) (σ : St S) (z : ℤ) (Ri : List Sym)
    (hi : σ.stk i = (Item.int z).enc ++ Ri) (hRi : bitOf Ri.head? = none)
    (hj : bitOf (σ.stk j).head? = none) (ht1 : bitOf (σ.stk t1).head? = none)
    (ht2 : bitOf (σ.stk t2).head? = none) :
    NLogN.Runs I prog (NLogN.dupInt q i j t1 t2 : Stmt S P) σ
      (σ.set j ((Item.int z).enc ++ σ.stk j)) (dupCost (zsz z) + 17) := 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.Runs.dupInt` of the Lean development NLogN/IntOps2.lean (lines 85–131), written for the prove2.me integer-multiplication campaign.

View graph