Round-six lemma `coreF_runs`

Proved

NLogN.KFC.coreF_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.KFCFwdMain):

theorem NLogN.KFC.coreF_runs (s : IState HS) (P q M B w : ℕ) (r : ℕ → ℕ → ℕ → List ℤ)
    (R LCP LDP LCQ LDQ LCM LDM LCB LDB : List Item)
    (h0 : s.G sX = ints (flF (KIL.blkIn r q M) 0 P) ++ R)
    (hCP : s.G sCP = marks P ++ LCP) (hDP : s.G sDP = LDP) (hLCP : NM LCP) (hLDP : NM LDP)
    (hCQ : s.G sCQ = marks q ++ LCQ) (hDQ : s.G sDQ = LDQ) (hLCQ : NM LCQ) (hLDQ : NM LDQ)
    (hCM : s.G sCM = marks M ++ LCM) (hDM : s.G sDM = LDM) (hLCM : NM LCM) (hLDM : NM LDM)
    (hCB : s.G sCB = marks B ++ LCB) (hDB : s.G sDB = LDB) (hLCB : NM LCB) (hLDB : NM LDB)
    (hr : ∀ p y m, (r p y m).length = B) (hb : ∀ p y m, Bnd w (r p y m))
    (hB : 1 ≤ B) (hq : 1 ≤ q) (hM : 1 ≤ M) :
    IRuns I iprog coreF s (s.upd sX (ints (flF (KIL.blkOut r q M) 0 P) ++ R))
      (P * (cBlk q M B w + 1064) + (flF (KIL.blkOut r q M) 0 P).length * kap w + 100)

Context. KFC: the self-contained fine-cost forward field move fwdF

fwdF_spec: on t with ints xs ++ R on stack 0 and P, q, M, B on stacks 1 … 4, fwdF ends in t.upd 0 (ints (pull [P,q,M,B] [P,M,q,B] gS 0 xs) ++ R) (all scratch stacks restored) with cost ≤ cFwdF P q M B w = (2q+16)·kap w·V + cUL P + cUL q + cUL M + cUL B + 1000, V = P·q·M·B, w a bound on the bit size of the entries of xs only.

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
set_option maxRecDepth 20000
open IntMul AModel
variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

Formal statement

theorem NLogN.KFC.coreF_runs (s : IState HS) (P q M B w : ℕ) (r : ℕ → ℕ → ℕ → List ℤ)
    (R LCP LDP LCQ LDQ LCM LDM LCB LDB : List Item)
    (h0 : s.G sX = ints (flF (KIL.blkIn r q M) 0 P) ++ R)
    (hCP : s.G sCP = marks P ++ LCP) (hDP : s.G sDP = LDP) (hLCP : NM LCP) (hLDP : NM LDP)
    (hCQ : s.G sCQ = marks q ++ LCQ) (hDQ : s.G sDQ = LDQ) (hLCQ : NM LCQ) (hLDQ : NM LDQ)
    (hCM : s.G sCM = marks M ++ LCM) (hDM : s.G sDM = LDM) (hLCM : NM LCM) (hLDM : NM LDM)
    (hCB : s.G sCB = marks B ++ LCB) (hDB : s.G sDB = LDB) (hLCB : NM LCB) (hLDB : NM LDB)
    (hr : ∀ p y m, (r p y m).length = B) (hb : ∀ p y m, Bnd w (r p y m))
    (hB : 1 ≤ B) (hq : 1 ≤ q) (hM : 1 ≤ M) :
    IRuns I iprog coreF s (s.upd sX (ints (flF (KIL.blkOut r q M) 0 P) ++ R))
      (P * (cBlk q M B w + 1064) + (flF (KIL.blkOut r q M) 0 P).length * kap w + 100) := 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.coreF_runs`, Solutions/KFCFwdMain.lean (lines 83–126) of the round-six development.

View graph