HvdH machine lemma AX.eDelR_all (One resampling axis, part 6: the tables of the `B̃` axis)

Proved

NLogN.AX.eDelR_all

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

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

The following holds (Lean statement, in the scope of module NLogN.HAx6):

theorem NLogN.AX.eDelR_all (s : ℕ) (st : IState HS) (hS : ∃ L, st.G bS = .int (s : ℤ) :: L) :
    eDelR.ok st ∧ eDelR.run st = st.upd bD (ints ((eDel s).map (Nat.cast : ℕ → ℤ)) ++ st.G bD) ∧
      eDelR.cost st ≤ tabCost 1 s ((eDelE.size + 1) * 10 ^ 7 * (s + 4) ^ 2) + 10 ^ 9

Context. The lemma belongs to the part One resampling axis, part 6: the tables of the B̃ axis: Each Rsp table builder is relocated by its own permutation so that it reads its scalar parameters from the B̃ layout (see HAx5) and pushes its table on the stack the relocated bapP reads. Three derived scalars are pushed on the temporaries 10 (e), 11 (s²), 12 (2α² - 2) for the duration of the table building.

Formalization Note. This is a lemma of the Lean development NLogN, a multitape-Turing-machine implementation of the Harvey–van der Hoeven $O(n\log n)$ integer multiplication algorithm, used in the proof of NLogN.FIN.theorem_1_1_nlogn : IntMul.MulTimeBound fun n => n * Real.log n. All names refer to the definition bundles IntMul_HvdH_M_Defs1–IntMul_HvdH_M_Defs8 (namespace NLogN), built on the platform model Def_IntMul_MultitapeModel and the published reference Def_IntMul_HvdH_MachineRef. The machine layer: IState HS is a state of 64 item stacks; RM programs have a semantics p.run s, a definedness predicate p.ok M s and a cost p.cost M s relative to a multiplication spec M : MulSpec; zsz z is the bit length of $|z|$ .

Preamble

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

import Definitions.Def_IntMul_HvdH_M_Defs8

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

set_option linter.unusedSimpArgs false
open NLogN
open NLogN.AX
open IntMul NLogN IntMul.HvdH.Ref NLogN.GL NLogN.Rsp

Formal statement

theorem NLogN.AX.eDelR_all (s : ℕ) (st : IState HS) (hS : ∃ L, st.G bS = .int (s : ℤ) :: L) :
    eDelR.ok st ∧ eDelR.run st = st.upd bD (ints ((eDel s).map (Nat.cast : ℕ → ℤ)) ++ st.G bD) ∧
      eDelR.cost st ≤ tabCost 1 s ((eDelE.size + 1) * 10 ^ 7 * (s + 4) ^ 2) + 10 ^ 9 := 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.AX.eDelR_all` of the Lean development NLogN/HAx6.lean (lines 87–94), written for the prove2.me integer-multiplication campaign.

View graph