Round-six lemma `body1_runs`

Proved

J6Seg.Src.body1_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.J6SegILSrc15):

theorem J6Seg.Src.body1_runs {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp} (s0 : IState HS)
    (F : Fin HS → List ℤ) {p pre post Q s t A : ℕ} {L1 L3 L4 L20 L22 L23 : List ℤ}
    (hF1 : F 1 = (p : ℤ) :: L1) (hF3 : F 3 = (pre : ℤ) :: L3) (hF4 : F 4 = (post : ℤ) :: L4)
    (hF20 : F 20 = (Q : ℤ) :: L20) (hF22 : F 22 = (s : ℤ) :: L22)
    (hF23 : F 23 = (t : ℤ) :: L23) (h43 : F 43 = []) (h44 : F 44 = []) (h34 : F 34 = [])
    (h35 : F 35 = []) (h36 : F 36 = []) (hpQ : p + 1 ≤ Q) (hs : 0 < s) (hst : s ≤ t)
    (hpA : p ≤ 2 ^ A) (hQA : 2 ^ Q ≤ 2 ^ A) (hpreA : pre ≤ 2 ^ A) (hpostA : post ≤ 2 ^ A)
    (htA : t ≤ 2 ^ A) (hA : 2 ≤ A) :
    IRuns I iprog body1 (encK s0 F)
      (encK s0 (regOut F (ctlOf t t (selSrc s t) (fun _ => ((2 ^ (Q - p - 1) : ℕ) : ℤ))) pre post t
        [] [])) (cost1 A Q t)

Context. B-line IL, source-table producers, part 15: the register file; pass 1 and pass 7 bodies

regOut F cs pre post n' K1 K2: F with the slab register file pushed (rC, rNC, rNB, rM, rTOT, rK1, rK2); regOut_RF: on RF v c with empty registers it is RF v (extend ρS (slabV …) c).
body1: 2^(Q-p-1) on 46 (pw2P), selP 22 23 46 23, ctlPh 23 23, cntP 3 4 23, pop 46. Input registers (as left by parP): 1 = p, 3 = pre, 4 = post, 20 = Q, 22 = s, 23 = t.
body7: outP 1 22 23 25 23, ctlPh 23 23, cntP 3 4 23, 2^(Q-p) on 41, 2^p on 42 (25 = α).

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_Defs67

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)
open J6Seg.PJ (rg RF RF_in RF_out upd_RF_out)
open J6Seg.Ax (ρS slabV)

Formal statement

theorem J6Seg.Src.body1_runs {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp} (s0 : IState HS)
    (F : Fin HS → List ℤ) {p pre post Q s t A : ℕ} {L1 L3 L4 L20 L22 L23 : List ℤ}
    (hF1 : F 1 = (p : ℤ) :: L1) (hF3 : F 3 = (pre : ℤ) :: L3) (hF4 : F 4 = (post : ℤ) :: L4)
    (hF20 : F 20 = (Q : ℤ) :: L20) (hF22 : F 22 = (s : ℤ) :: L22)
    (hF23 : F 23 = (t : ℤ) :: L23) (h43 : F 43 = []) (h44 : F 44 = []) (h34 : F 34 = [])
    (h35 : F 35 = []) (h36 : F 36 = []) (hpQ : p + 1 ≤ Q) (hs : 0 < s) (hst : s ≤ t)
    (hpA : p ≤ 2 ^ A) (hQA : 2 ^ Q ≤ 2 ^ A) (hpreA : pre ≤ 2 ^ A) (hpostA : post ≤ 2 ^ A)
    (htA : t ≤ 2 ^ A) (hA : 2 ≤ A) :
    IRuns I iprog body1 (encK s0 F)
      (encK s0 (regOut F (ctlOf t t (selSrc s t) (fun _ => ((2 ^ (Q - p - 1) : ℕ) : ℤ))) pre post t
        [] [])) (cost1 A Q t) := 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.body1_runs`, Solutions/J6SegILSrc15.lean (lines 96–196) of the round-six development.

View graph