Round-six lemma `uloop_runs`

Proved

NLogN.KFC.uloop_runs

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

complexity-theoryinteger-multiplicationkappa-improvement

An auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.

The following holds (Lean statement, in the scope of module Solutions.KFCBase):

theorem NLogN.KFC.uloop_runs {C D : Fin HS} (hCD : C ≠ D) (n : ℕ) (T : ℕ → IState HS) (LC LD : List Item)
    (hLC : NM LC) (hLD : NM LD) (c : ℕ) (b : IStmt HS Pp)
    (hb : ∀ k < n, ∀ LC' LD', IRuns I iprog b (cf (T k) C D LC' LD') (cf (T (k + 1)) C D LC' LD') c) :
    IRuns I iprog (uloop C D b) (cf (T 0) C D (marks n ++ LC) LD)
      (cf (T n) C D (marks n ++ LC) LD) (n * (c + 64) + 60)

Context. KFC base: fine-cost item-language loops

Item-language (IStmt) building blocks whose per-element cost is O(1 + zsz a) for the moved entry a, with no binary loop counter per element:

mvW X Y : move integers from X to Y until the top of X is not an integer (delimiter-driven, cost (76 w + 131) per entry of bit size ≤ w);
uloop C D b: run b once per mark on the unary counter C (the marks are moved to D and then moved back, so the counter is restored); overhead 64 per iteration;
mvB X Y C D: move exactly n integers, n = number of marks on C;
toU A X K K2: push n marks on X, where n ≥ 0 is the integer on top of A (binary counter, cost O((n+1)(zsz n + 2)); superseded by the linear KFCUnary.toUL, which the programs use);
clrM X : drop all marks on top of X.

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).

Preamble

-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.

import Definitions.Def_IntMul_Kappa_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_MultitapeModel

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open NLogN NLogN.KFC
open IntMul
variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

Formal statement

theorem NLogN.KFC.uloop_runs {C D : Fin HS} (hCD : C ≠ D) (n : ℕ) (T : ℕ → IState HS) (LC LD : List Item)
    (hLC : NM LC) (hLD : NM LD) (c : ℕ) (b : IStmt HS Pp)
    (hb : ∀ k < n, ∀ LC' LD', IRuns I iprog b (cf (T k) C D LC' LD') (cf (T (k + 1)) C D LC' LD') c) :
    IRuns I iprog (uloop C D b) (cf (T 0) C D (marks n ++ LC) LD)
      (cf (T n) C D (marks n ++ LC) LD) (n * (c + 64) + 60) := by sorry

Source

S. Jain, round-six networks for the integer-multiplication κ-improvement campaign (https://github.com/Swapnil-jain/integer-mult-kappa, commit 5868dc7) and D. Colkitt, integer-mult-bounds (https://github.com/CrocSwap/integer-mult-bounds); target `IntMul.Kappa.jain_round6_framework`. Lean declaration `NLogN.KFC.uloop_runs`, Solutions/KFCBase.lean (lines 140–204) of the round-six development.

View graph