The capacitance matrix (round six, `capP`)

Proved

J6Seg.PJ.Rn.capP

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

complexity-theoryinteger-multiplicationkappa-improvement

The capacitance matrix.

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

theorem J6Seg.PJ.Rn.capP {v : Vr} (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 = B.w)
    (h28 : v 28 = m)
    (hL : D 30 = L.map (fun j : ℕ => (j : ℤ))) (hLm : L.length = m)
    (hLs : ∀ j ∈ L, j < s) (hBs : B.s = s) (hs : 0 < s) (hB : BlocksOK s t B)
    (hBl : ∀ j < s, B.len j ≤ lam)
    (h32 : D 32 = (List.range s).map (fun j => (B.st j : ℤ)))
    (h33 : D 33 = (List.range s).map (fun j => (B.len j : ℤ)))
    (hTS : TabSt Q R W s t α lam D)
    (hSAP : D SAP = []) (hSAM : D SAM = []) (hSMI : D SMI = []) (hSV : D SV = []) (hSC : D SC = [])
    (h48 : D 48 = []) (h50 : D 50 = []) (h51 : D 51 = []) (h53 : D 53 = []) (h54 : D 54 = [])
    (hCu : D PreT.Cu = []) (hSM : D SMAT = []) (h14 : D 14 = [])
    (hQW : Q ≤ W) (hsN : s ≤ N) (hlN : lam ≤ N) (hmN : m ≤ N) (hNMN : lam * (2 * B.w + 1) ≤ N)
    (hmm : m * m ≤ N)
    (bss : s * s ≤ 2 ^ W) (hGB : GlobBnd Q W s t α lam)
    (hRB : ∀ a < s, RowBnd Q R W s t α lam B a) :
    Rn J6Seg.PJ.capP v D (fun v' => Fxk (6 :: BIG) v v' ∧ BV W v')
      (update D 14 (matL (fun i k => capI Q (mkTables Q R s t α) B (Lg L i) (Lg L k)) m))
      (cCapP W N lam (lam * (2 * B.w + 1)) m)

Context. B5 J side, part K11: the capacitance matrix

capP = forL 48 28 6 rowB; 11 := m·m; mvK SMAT 14: the matrix matL (fun i k => capI (L[i]) (L[k])) m on 14 (Rn.capP).

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
set_option maxRecDepth 100000
open IntMul NLogN NLogN.KIL NLogN.RS Function Finset
variable {Q R W N s t α lam m : ℕ} {B : Blocks} {L : List ℕ} {D : Cs}

Formal statement

theorem J6Seg.PJ.Rn.capP {v : Vr} (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 = B.w)
    (h28 : v 28 = m)
    (hL : D 30 = L.map (fun j : ℕ => (j : ℤ))) (hLm : L.length = m)
    (hLs : ∀ j ∈ L, j < s) (hBs : B.s = s) (hs : 0 < s) (hB : BlocksOK s t B)
    (hBl : ∀ j < s, B.len j ≤ lam)
    (h32 : D 32 = (List.range s).map (fun j => (B.st j : ℤ)))
    (h33 : D 33 = (List.range s).map (fun j => (B.len j : ℤ)))
    (hTS : TabSt Q R W s t α lam D)
    (hSAP : D SAP = []) (hSAM : D SAM = []) (hSMI : D SMI = []) (hSV : D SV = []) (hSC : D SC = [])
    (h48 : D 48 = []) (h50 : D 50 = []) (h51 : D 51 = []) (h53 : D 53 = []) (h54 : D 54 = [])
    (hCu : D PreT.Cu = []) (hSM : D SMAT = []) (h14 : D 14 = [])
    (hQW : Q ≤ W) (hsN : s ≤ N) (hlN : lam ≤ N) (hmN : m ≤ N) (hNMN : lam * (2 * B.w + 1) ≤ N)
    (hmm : m * m ≤ N)
    (bss : s * s ≤ 2 ^ W) (hGB : GlobBnd Q W s t α lam)
    (hRB : ∀ a < s, RowBnd Q R W s t α lam B a) :
    Rn J6Seg.PJ.capP v D (fun v' => Fxk (6 :: BIG) v v' ∧ BV W v')
      (update D 14 (matL (fun i k => capI Q (mkTables Q R s t α) B (Lg L i) (Lg L k)) m))
      (cCapP W N lam (lam * (2 * B.w + 1)) m) := 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.capP`, Solutions/J6SegILPreJK11.lean (lines 77–202) of the round-six development.

View graph