Round-six lemma `ctlPh_runs`

Proved

J6Seg.Src.ctlPh_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.J6SegILSrc14):

theorem J6Seg.Src.ctlPh_runs {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp} (s0 : IState HS)
    (F : Fin HS → List ℤ) {Rn Rn' : Fin HS} (hR5 : Rn.val < 56) (hR5' : Rn'.val < 56)
    (dR : Rn ≠ 20 ∧ Rn ≠ 21) (dR' : Rn' ≠ 20 ∧ Rn' ≠ 21 ∧ Rn' ≠ 38 ∧ Rn' ≠ 44 ∧ Rn' ≠ 45)
    {n n' A : ℕ} {src : ℕ → Option ℕ} {argOf : ℕ → ℤ} (hs : MonoSrc n n' src) {LN LN' : List ℤ}
    (hFN : F Rn = (n : ℤ) :: LN) (hFN' : F Rn' = (n' : ℤ) :: LN')
    (h44 : F 44 = srcTab src argOf n') (h43 : F 43 = []) (h34 : F 34 = []) (h35 : F 35 = [])
    (h36 : F 36 = []) (hnA : n ≤ 2 ^ A) (hnA' : n' ≤ 2 ^ A) (ha : ∀ l < n', |argOf l| ≤ 2 ^ A)
    (hA : 2 ≤ A) :
    IRuns I iprog (ctlPh Rn Rn') (encK s0 F)
      (encK s0 (update (update (update F 44 []) 38 (((n + n' : ℕ) : ℤ) :: F 38)) 45
        (flatC (ctlOf n n' src argOf) ++ F 45))) (ctlPhC A n n')

Context. B-line IL, source-table producers, part 14: the control phase

ctlPh Rn Rn': with the source table srcTab src argOf n' on 44 (alone), n on Rn and n' on Rn': push n', n on bN' = 20, bN = 21, run ctlB (J6SegILCtl5), pop them and drop the table. Output: flatC (ctlOf n n' src argOf) on rC = 45, n + n' on rNC = 38, 44 emptied (ctlPh_runs).

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 NLogN.KFUU (cU)

Formal statement

theorem J6Seg.Src.ctlPh_runs {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp} (s0 : IState HS)
    (F : Fin HS → List ℤ) {Rn Rn' : Fin HS} (hR5 : Rn.val < 56) (hR5' : Rn'.val < 56)
    (dR : Rn ≠ 20 ∧ Rn ≠ 21) (dR' : Rn' ≠ 20 ∧ Rn' ≠ 21 ∧ Rn' ≠ 38 ∧ Rn' ≠ 44 ∧ Rn' ≠ 45)
    {n n' A : ℕ} {src : ℕ → Option ℕ} {argOf : ℕ → ℤ} (hs : MonoSrc n n' src) {LN LN' : List ℤ}
    (hFN : F Rn = (n : ℤ) :: LN) (hFN' : F Rn' = (n' : ℤ) :: LN')
    (h44 : F 44 = srcTab src argOf n') (h43 : F 43 = []) (h34 : F 34 = []) (h35 : F 35 = [])
    (h36 : F 36 = []) (hnA : n ≤ 2 ^ A) (hnA' : n' ≤ 2 ^ A) (ha : ∀ l < n', |argOf l| ≤ 2 ^ A)
    (hA : 2 ≤ A) :
    IRuns I iprog (ctlPh Rn Rn') (encK s0 F)
      (encK s0 (update (update (update F 44 []) 38 (((n + n' : ℕ) : ℤ) :: F 38)) 45
        (flatC (ctlOf n n' src argOf) ++ F 45))) (ctlPhC A n n') := 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.ctlPh_runs`, Solutions/J6SegILSrc14.lean (lines 51–119) of the round-six development.

View graph