Packing a digit list into one integer: cost

Proved

NLogN.packOne_cost

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

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

Under the hypotheses of the packing result (stack $E_i$ holds the reversed list $L$ of digits with $0\le L_k<2^b$ , CR holds $2^b$ , CM holds $|L|$ , registers distinct), and $1\le b\le Q$ , $\mathrm{zsz}(|L|)\le Q$ , the program packOne E_i X costs at most $2\cdot10^5(|L|+1)(Q+3) + 30000(b|L|+Q+4)$ .

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
open NLogN
open IntMul IntMul.HvdH IntMul.HvdH.Ref
set_option maxHeartbeats 1000000

Formal statement

theorem NLogN.packOne_cost (M : MulSpec) (Ei X : Fin HS) (s : IState HS) (b Q : ℕ) (L : List ℤ)
    (Ri LR LM : List Item)
    (hEi : s.G Ei = ints L.reverse ++ Ri) (hR : s.G CR = .int (2 ^ b) :: LR)
    (hM : s.G CM = .int L.length :: LM) (hL : ∀ x ∈ L, 0 ≤ x ∧ x < 2 ^ b)
    (hb1 : 1 ≤ b) (hbQ : b ≤ Q) (hMQ : zsz (L.length : ℤ) ≤ Q)
    (h1 : Ei ≠ CA) (h2 : Ei ≠ CY) (h3 : Ei ≠ CR) (h4 : Ei ≠ CM) (h5 : Ei ≠ EC) (h6 : Ei ≠ X)
    (h7 : X ≠ CA) (h8 : X ≠ CY) (h9 : X ≠ CR) (h10 : X ≠ CM) (h11 : X ≠ EC) :
    (packOne Ei X).cost M s ≤ 200000 * (L.length + 1) * (Q + 3) +
      30000 * (b * L.length + Q + 4) := 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.packOne_cost` of the Lean development NLogN/HEncCost.lean (lines 73–117), written for the prove2.me integer-multiplication campaign.

View graph