Encoding one block into the Fermat ring: result

Proved

NLogN.encP_run

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

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

Under the same register hypotheses (stack GU starts with blk, registers hold $2^P$ , $|blk|$ , $2^{2|blk|P}$ , $F$ ), the program encP consumes the block and pushes on EO the integer $E$ if $E\ge0$ and $E+F$ otherwise, where $E = \mathrm{encRaw}(P, blk) = \bigl(\kappa(\mathrm{re}^+) - \kappa(\mathrm{re}^-)\bigr) + \bigl(\kappa(\mathrm{im}^+) - \kappa(\mathrm{im}^-)\bigr)2^{2|blk|P}$ with $\kappa =$ kpack (2^P) applied to the positive and negative parts of the real and imaginary coordinates.

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 2000000

Formal statement

theorem NLogN.encP_run (s : IState HS) (P : ℕ) (blk : List (ℤ × ℤ)) (R LR LM LW LF : List Item)
    (F : ℤ) (hU : s.G GU = gints blk ++ R) (hR : s.G CR = .int (2 ^ P) :: LR)
    (hM : s.G CM = .int blk.length :: LM)
    (hW : s.G RW = .int (2 ^ (2 * blk.length * P)) :: LW) (hF : s.G FR = .int F :: LF) :
    encP.run s = (s.upd GU R).upd EO
      (.int (if encRaw P blk < 0 then encRaw P blk + F else encRaw P blk) :: s.G EO) := 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.encP_run` of the Lean development NLogN/HEnc.lean (lines 160–219), written for the prove2.me integer-multiplication campaign.

View graph