Round-six lemma `M_runsG`

Proved

NLogN.KFZ.M_runsG

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.R6ZCall):

theorem NLogN.KFZ.M_runsG (j : Fin (7 + E)) (d18 : Fin HS) (hd0 : d18 ≠ 0)
    {p h d σ K B : ℕ} (hB : RB p h d σ K B) (hM : MG p h d σ K)
    (Bd : ℕ) (hBd : ∀ x ∈ dsG p h d σ K, zsz x ≤ Bd)
    (s : IState HS) (G : Fin HS → List ℤ) (hR : Regs G p h d σ K) (ZF ZG : List GI) (l : List ℤ)
    (h0 : G 0 = gflat ZF ++ gflat ZG ++ l) (hX : G (X18 d18) = [])
    (zh : List GI) (c : ℕ)
    (hcall : IRuns I iprog (.call j)
      (encK (bgS s G d18 l) (fC d18 (gflat ZF ++ gflat ZG ++ []) (dsG p h d σ K)))
      (encK (bgS s G d18 l) (Function.update (fC d18 (gflat ZF ++ gflat ZG ++ [])
        (dsG p h d σ K)) 0 (gflat zh ++ []))) c) :
    IRuns I iprog (Mcall j d18) (encK s G) (encK s (Function.update G 0 (gflat zh ++ l)))
      (c + cM B Bd (p / 6) (dsG p h d σ K).length)

Context. Round six, chirp: the Prop 18 call and the product phase for any parameters

MG, dsG: the side conditions and the Prop 18 descriptor for free p h d σ K (the frozen KFZCall.M_runs reads them through n).
M_runsG: the frozen M_runs without n.
PP_runsP: the frozen PP_runs in IL.kTableP tab ext, without n.

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_R6_Defs16

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open NLogN NLogN.KFZ
open IntMul NLogN.KIL NLogN.KFB NLogN.KFM IntMul.OpenAI.Glue
variable {E : ℕ} {I : List Sym} {iprog : Fin (7 + E) → IStmt HS (7 + E)}

Formal statement

theorem NLogN.KFZ.M_runsG (j : Fin (7 + E)) (d18 : Fin HS) (hd0 : d18 ≠ 0)
    {p h d σ K B : ℕ} (hB : RB p h d σ K B) (hM : MG p h d σ K)
    (Bd : ℕ) (hBd : ∀ x ∈ dsG p h d σ K, zsz x ≤ Bd)
    (s : IState HS) (G : Fin HS → List ℤ) (hR : Regs G p h d σ K) (ZF ZG : List GI) (l : List ℤ)
    (h0 : G 0 = gflat ZF ++ gflat ZG ++ l) (hX : G (X18 d18) = [])
    (zh : List GI) (c : ℕ)
    (hcall : IRuns I iprog (.call j)
      (encK (bgS s G d18 l) (fC d18 (gflat ZF ++ gflat ZG ++ []) (dsG p h d σ K)))
      (encK (bgS s G d18 l) (Function.update (fC d18 (gflat ZF ++ gflat ZG ++ [])
        (dsG p h d σ K)) 0 (gflat zh ++ []))) c) :
    IRuns I iprog (Mcall j d18) (encK s G) (encK s (Function.update G 0 (gflat zh ++ l)))
      (c + cM B Bd (p / 6) (dsG p h d σ K).length) := 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.KFZ.M_runsG`, Solutions/R6ZCall.lean (lines 41–140) of the round-six development.

View graph