Round-six lemma `body5_runs`

Proved

J6Seg.Src.body5_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.J6SegILSrc17):

theorem J6Seg.Src.body5_runs {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp} (s0 : IState HS)
    (F : Fin HS → List ℤ) {pre post s t lam w A : ℕ} {L3 L4 L22 L23 L24 L26 : List ℤ}
    (hF3 : F 3 = (pre : ℤ) :: L3) (hF4 : F 4 = (post : ℤ) :: L4)
    (hF22 : F 22 = (s : ℤ) :: L22) (hF23 : F 23 = (t : ℤ) :: L23)
    (hF24 : F 24 = (lam : ℤ) :: L24) (hF26 : F 26 = (w : ℤ) :: L26) (h43 : F 43 = [])
    (h44 : F 44 = []) (h34 : F 34 = []) (h35 : F 35 = []) (h36 : F 36 = []) (hs : 0 < s)
    (hst : s ≤ t) (hl : 0 < lam) (hpreA : pre ≤ 2 ^ A) (hpostA : post ≤ 2 ^ A) (htA : t ≤ 2 ^ A)
    (hlA : lam ≤ 2 ^ A) (hwA : w ≤ 2 ^ A)
    (hGA : 2 ^ Nat.clog 2 (Jlist (mkBlocks s t lam w)).length ≤ 2 ^ A) (hA : 2 ≤ A) :
    IRuns I iprog body5 (encK s0 F)
      (encK s0 (regOut F (ctlOf (2 ^ Nat.clog 2 (Jlist (mkBlocks s t lam w)).length) t
        (scSrc s t lam w) (fun _ => 0)) pre post t [] []))
        (cost5 A s t (Jlist (mkBlocks s t lam w)).length
          (2 ^ Nat.clog 2 (Jlist (mkBlocks s t lam w)).length))

Context. B-line IL, source-table producers, part 17: the pass-5 body

body5: ljP 22 23 24 26, cgP 31 46, scP 23 (scatter table over t slabs), ctlPh 46 23 (n = G, n' = t), cntP 3 4 23, pop 46, cleanLJ.

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_Defs70

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.Src
open IntMul NLogN NLogN.KIL Function NLogN.RS J6Seg
open J6Seg.PreT hiding rg RF RF_in RF_out upd_RF_in upd_RF_out cE InRg
open J6Seg.Slab (srcTab flatC ctlB ctlCost)

Formal statement

theorem J6Seg.Src.body5_runs {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp} (s0 : IState HS)
    (F : Fin HS → List ℤ) {pre post s t lam w A : ℕ} {L3 L4 L22 L23 L24 L26 : List ℤ}
    (hF3 : F 3 = (pre : ℤ) :: L3) (hF4 : F 4 = (post : ℤ) :: L4)
    (hF22 : F 22 = (s : ℤ) :: L22) (hF23 : F 23 = (t : ℤ) :: L23)
    (hF24 : F 24 = (lam : ℤ) :: L24) (hF26 : F 26 = (w : ℤ) :: L26) (h43 : F 43 = [])
    (h44 : F 44 = []) (h34 : F 34 = []) (h35 : F 35 = []) (h36 : F 36 = []) (hs : 0 < s)
    (hst : s ≤ t) (hl : 0 < lam) (hpreA : pre ≤ 2 ^ A) (hpostA : post ≤ 2 ^ A) (htA : t ≤ 2 ^ A)
    (hlA : lam ≤ 2 ^ A) (hwA : w ≤ 2 ^ A)
    (hGA : 2 ^ Nat.clog 2 (Jlist (mkBlocks s t lam w)).length ≤ 2 ^ A) (hA : 2 ≤ A) :
    IRuns I iprog body5 (encK s0 F)
      (encK s0 (regOut F (ctlOf (2 ^ Nat.clog 2 (Jlist (mkBlocks s t lam w)).length) t
        (scSrc s t lam w) (fun _ => 0)) pre post t [] []))
        (cost5 A s t (Jlist (mkBlocks s t lam w)).length
          (2 ^ Nat.clog 2 (Jlist (mkBlocks s t lam w)).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 `J6Seg.Src.body5_runs`, Solutions/J6SegILSrc17.lean (lines 36–144) of the round-six development.

View graph