Stage 2 (round six, `jS2`)

Proved

J6Seg.PJ.Rn.jS2

by xuanji · Oct 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theoryinteger-multiplicationkappa-improvement

Stage 2.

The following holds (Lean statement, in the scope of module Solutions.J6SegILPreJK17):

theorem J6Seg.PJ.Rn.jS2 {Q R W N s t α lam w : ℕ} {L : List ℕ} {v : Vr} {c : Cs}
    (hNW : N < 2 ^ W) (hW2 : 2 ≤ W) (hv : BV W v)
    (h9 : v 9 = 2 ^ Q) (h10 : v 10 = 2 ^ (Q + 1)) (h20 : v 20 = Q) (h21 : v 21 = R)
    (h22 : v 22 = s) (h23 : v 23 = t) (h24 : v 24 = lam) (h25 : v 25 = α) (h26 : v 26 = w)
    (h28 : v 28 = L.length)
    (hLdef : L = Jlist (mkBlocks s t lam w))
    (h30 : c 30 = L.map (fun j : ℕ => (j : ℤ)))
    (h32 : c 32 = Src.STL s t lam) (h33 : c 33 = Src.LNL s t lam)
    (hs : 0 < s) (hl : 1 ≤ lam) (hws : w ≤ s)
    (hCu : c PreT.Cu = []) (hDI : c SDI = []) (hDD : c SDD = []) (hGM : c SGM = [])
    (hGI : c SGI = []) (hSAP : c SAP = []) (hSAM : c SAM = []) (hSMI : c SMI = [])
    (hSV : c SV = []) (hSC : c SC = []) (h48 : c 48 = []) (h50 : c 50 = []) (h51 : c 51 = [])
    (h53 : c 53 = []) (h54 : c 54 = []) (hSM : c SMAT = []) (h14 : c 14 = [])
    (hQW : Q ≤ W) (hsN : s ≤ N) (hlN : lam ≤ N) (hNMN : lam * (2 * w + 1) ≤ N)
    (hmm : L.length * L.length ≤ N) (hmc : L.length * (2 * w + 2) ≤ N) (hwW : 2 * w + 1 < 2 ^ W)
    (bss : s * s ≤ 2 ^ W) (hGB : GlobBnd Q W s t α lam)
    (bgm : ∀ i < lam, |(mkTables Q R s t α).gam i| ≤ 2 ^ W)
    (bgi : ∀ i < lam, |(mkTables Q R s t α).gi i| ≤ 2 ^ W)
    (bdd : ∀ i < lam, |(mkTables Q R s t α).dd i| ≤ 2 ^ W)
    (bdi : ∀ i < lam, |(mkTables Q R s t α).di i| ≤ 2 ^ W)
    (hRB : ∀ a < s, RowBnd Q R W s t α lam (mkBlocks s t lam w) a)
    (hCB : ∀ r < L.length, CcBnd W s t α (mkTables Q R s t α) (mkBlocks s t lam w) (Lg L r)) :
    Rn J6Seg.PJ.jS2 v c (fun v' => Fxk FS2 v v' ∧ BV W v')
      (update (update (tabSt Q R s t lam α c) 14
        (matL (fun i k => capI Q (mkTables Q R s t α) (mkBlocks s t lam w) (Lg L i) (Lg L k))
          L.length)) 41
        (JK.flatT (ccRows (mkTables Q R s t α) (mkBlocks s t lam w) L L.length) ++ c 41))
      (cJS2 W N Q R lam w L.length)

Context. B5 J side, part K17: stage 2 — tables, capacitance matrix, coupling windows

jS2 = tabP; capP; ccP (Rn.jS2): the reversed line tables on SDI … SGI, the capacitance matrix on 14, and JK.flatT (ccRows …) in front of 41.

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_Defs71

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.PJ
open IntMul NLogN NLogN.KIL NLogN.RS Function

Formal statement

theorem J6Seg.PJ.Rn.jS2 {Q R W N s t α lam w : ℕ} {L : List ℕ} {v : Vr} {c : Cs}
    (hNW : N < 2 ^ W) (hW2 : 2 ≤ W) (hv : BV W v)
    (h9 : v 9 = 2 ^ Q) (h10 : v 10 = 2 ^ (Q + 1)) (h20 : v 20 = Q) (h21 : v 21 = R)
    (h22 : v 22 = s) (h23 : v 23 = t) (h24 : v 24 = lam) (h25 : v 25 = α) (h26 : v 26 = w)
    (h28 : v 28 = L.length)
    (hLdef : L = Jlist (mkBlocks s t lam w))
    (h30 : c 30 = L.map (fun j : ℕ => (j : ℤ)))
    (h32 : c 32 = Src.STL s t lam) (h33 : c 33 = Src.LNL s t lam)
    (hs : 0 < s) (hl : 1 ≤ lam) (hws : w ≤ s)
    (hCu : c PreT.Cu = []) (hDI : c SDI = []) (hDD : c SDD = []) (hGM : c SGM = [])
    (hGI : c SGI = []) (hSAP : c SAP = []) (hSAM : c SAM = []) (hSMI : c SMI = [])
    (hSV : c SV = []) (hSC : c SC = []) (h48 : c 48 = []) (h50 : c 50 = []) (h51 : c 51 = [])
    (h53 : c 53 = []) (h54 : c 54 = []) (hSM : c SMAT = []) (h14 : c 14 = [])
    (hQW : Q ≤ W) (hsN : s ≤ N) (hlN : lam ≤ N) (hNMN : lam * (2 * w + 1) ≤ N)
    (hmm : L.length * L.length ≤ N) (hmc : L.length * (2 * w + 2) ≤ N) (hwW : 2 * w + 1 < 2 ^ W)
    (bss : s * s ≤ 2 ^ W) (hGB : GlobBnd Q W s t α lam)
    (bgm : ∀ i < lam, |(mkTables Q R s t α).gam i| ≤ 2 ^ W)
    (bgi : ∀ i < lam, |(mkTables Q R s t α).gi i| ≤ 2 ^ W)
    (bdd : ∀ i < lam, |(mkTables Q R s t α).dd i| ≤ 2 ^ W)
    (bdi : ∀ i < lam, |(mkTables Q R s t α).di i| ≤ 2 ^ W)
    (hRB : ∀ a < s, RowBnd Q R W s t α lam (mkBlocks s t lam w) a)
    (hCB : ∀ r < L.length, CcBnd W s t α (mkTables Q R s t α) (mkBlocks s t lam w) (Lg L r)) :
    Rn J6Seg.PJ.jS2 v c (fun v' => Fxk FS2 v v' ∧ BV W v')
      (update (update (tabSt Q R s t lam α c) 14
        (matL (fun i k => capI Q (mkTables Q R s t α) (mkBlocks s t lam w) (Lg L i) (Lg L k))
          L.length)) 41
        (JK.flatT (ccRows (mkTables Q R s t α) (mkBlocks s t lam w) L L.length) ++ c 41))
      (cJS2 W N Q R lam w L.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.PJ.Rn.jS2`, Solutions/J6SegILPreJK17.lean (lines 30–134) of the round-six development.

View graph