Round-six lemma `iLoop_run`

Proved

J6Seg.iLoop_run

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

theorem J6Seg.iLoop_run (m post nc pre B Lmax : ℕ) (hB : 1 ≤ B)
    (s : IState HS) (F : Fin HS → List ℤ) (R0 : List ℤ) (zA aA : ℕ → List ℤ)
    (xr : ℕ → List GI)
    (hS : RowStream Pre g B m post nc (pre * nc * post) zA aA xr)
    (hm2 : F (ρ 7) = [((2 * m : ℕ) : ℤ)]) (hmB : zsz ((2 * m : ℕ) : ℤ) ≤ B)
    (hp : F (ρ 4) = [(post : ℤ)]) (hpB : zsz (post : ℤ) ≤ B)
    (hn : F (ρ 6) = [(nc : ℤ)]) (hnB : zsz (nc : ℤ) ≤ B)
    (hpr : F (ρ 5) = [(pre : ℤ)]) (hprB : zsz (pre : ℤ) ≤ B)
    (hTot : F (ρ 9) = [((tabsT tabOf nc).length : ℤ)])
    (hTotB : zsz ((tabsT tabOf nc).length : ℤ) ≤ B)
    (hTB : ∀ q < nc, Bnd B (tabOf q)) (hTL : ∀ q < nc, (tabOf q).length ≤ Lmax)
    (hLB : zsz (Lmax : ℤ) ≤ B) :
    IRuns Isym tbl (iLoop ρ dT e)
      (encK s (J6Seg.KS ρ dT F (zA 0) [] (tabsT tabOf nc ++ R0) [] [] [] (aA 0) [] [] []))
      (encK s (J6Seg.KS ρ dT F (zA (pre * nc * post)) [] (tabsT tabOf nc ++ R0) [] [] []
        (aA (pre * nc * post)) [] [] []))
      (cIL ⌊Ck⌋₊ B m post Lmax nc (tabsT tabOf nc).length pre)

Context. B-line IL, B2 (kernel-pass wrapper) §3: the block loops

segT tabOf q = |tabOf q| :: tabOf q; the table store holds tabsT tabOf nc ++ R0 (tabsT = ⋃_{q < nc} segT q).

qLoop_run: for one outer index i, the loop over the chunks q < nc: load table q, run the post rows of block i·nc + q (kernel g q), unload; the store is consumed and U (ρ 15) collects the used tables, reversed.
iLoop_run: the loop over i < pre: the chunk loop, then the store is restored from U.

The rows come from an abstract stream (RowStream): row r is xr r, on top of stack 0 before it is zA r, the outputs so far are aA r (reversed), the kernel of row r is g (r / post % nc).

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_Defs64

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function
variable {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp} {e : Fin Pp}
  {ρ : Fin 19 → Fin HS} {dT dF : Fin HS} (hR : RegOK ρ dT dF)
  {tabOf : ℕ → List ℤ} {Pre : List GI → Prop} {g : ℕ → List GI → List GI} {Ck : ℝ}
  (hRow : RowBody6 Isym tbl e dT tabOf Pre g Ck)
include hR hRow

Formal statement

theorem J6Seg.iLoop_run (m post nc pre B Lmax : ℕ) (hB : 1 ≤ B)
    (s : IState HS) (F : Fin HS → List ℤ) (R0 : List ℤ) (zA aA : ℕ → List ℤ)
    (xr : ℕ → List GI)
    (hS : RowStream Pre g B m post nc (pre * nc * post) zA aA xr)
    (hm2 : F (ρ 7) = [((2 * m : ℕ) : ℤ)]) (hmB : zsz ((2 * m : ℕ) : ℤ) ≤ B)
    (hp : F (ρ 4) = [(post : ℤ)]) (hpB : zsz (post : ℤ) ≤ B)
    (hn : F (ρ 6) = [(nc : ℤ)]) (hnB : zsz (nc : ℤ) ≤ B)
    (hpr : F (ρ 5) = [(pre : ℤ)]) (hprB : zsz (pre : ℤ) ≤ B)
    (hTot : F (ρ 9) = [((tabsT tabOf nc).length : ℤ)])
    (hTotB : zsz ((tabsT tabOf nc).length : ℤ) ≤ B)
    (hTB : ∀ q < nc, Bnd B (tabOf q)) (hTL : ∀ q < nc, (tabOf q).length ≤ Lmax)
    (hLB : zsz (Lmax : ℤ) ≤ B) :
    IRuns Isym tbl (iLoop ρ dT e)
      (encK s (J6Seg.KS ρ dT F (zA 0) [] (tabsT tabOf nc ++ R0) [] [] [] (aA 0) [] [] []))
      (encK s (J6Seg.KS ρ dT F (zA (pre * nc * post)) [] (tabsT tabOf nc ++ R0) [] [] []
        (aA (pre * nc * post)) [] [] []))
      (cIL ⌊Ck⌋₊ B m post Lmax nc (tabsT tabOf nc).length pre) := 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 `J6Seg.iLoop_run`, Solutions/J6SegILKer3.lean (lines 171–229) of the round-six development.

View graph