Round-six lemma `colL`

Proved

J6Seg.PJ.Rn.colL

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.J6SegILPreJK8):

theorem J6Seg.PJ.Rn.colL {v : Vr} (hN : N ≤ 2 ^ W) (hW2 : 2 ≤ W) (hv : BV W v)
    (h7 : v 7 = a) (h9 : v 9 = 2 ^ Q) (h11 : v 11 = NN) (h28 : v 28 = m)
    (hQW : Q ≤ W) (hmW : m < 2 ^ W) (hNW : NN < 2 ^ W) (hNN : NN ≤ N) (hmN : m ≤ N)
    (hL : D 30 = L.map (fun j : ℕ => (j : ℤ))) (hLm : L.length = m) (hLb : ∀ j ∈ L, j ≤ 2 ^ W)
    (h53 : D 53 = []) (h54 : D 54 = [])
    (hSC : D SC = ((List.range NN).map gc).reverse) (hSV : D SV = ((List.range NN).map gv).reverse)
    (bc : ∀ i < NN, |gc i| ≤ 2 ^ W) (bv : ∀ i < NN, |gv i| ≤ 2 ^ W)
    (bS : ∀ k < m, ∀ K ≤ NN, |(if a = Lg L k then (2 : ℤ) ^ Q else 0) +
      ∑ y ∈ range K, cTm gv gc (Lg L k) y| ≤ 2 ^ W) :
    Rn PJ.colL v D (fun v' => Fxk [1, 3, 4, 5, 8, 12, 29] v v' ∧ BV W v')
      (update D SMAT (rvL (fun k => cEnt Q a gv gc NN (Lg L k)) m ++ D SMAT))
      (cFor W m (cColB W N NN))

Context. B5 J side, part K8: the M⁻¹ row loop, the column loop, clearing a stack

PJ.clrK X C r: pop X r times (Rn.clrK);
PJ.miL = forL 50 2 3 (8 := 0; PJ.tsL; PJ.miT): pushes miV a u for u < n on SMI (Rn.miL);
PJ.colL = forL 53 28 3 PJ.colB: for each column k < m, b = L[k], pushes [a = b] 2^Q + Σ_y [gC y = b] gV y on SMAT = 43 (Rn.colL).

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 J6Seg.PJ.E Finset
variable {Q W N NN m a : ℕ} {gv gc : ℕ → ℤ} {L : List ℕ} {D : Cs}

Formal statement

theorem J6Seg.PJ.Rn.colL {v : Vr} (hN : N ≤ 2 ^ W) (hW2 : 2 ≤ W) (hv : BV W v)
    (h7 : v 7 = a) (h9 : v 9 = 2 ^ Q) (h11 : v 11 = NN) (h28 : v 28 = m)
    (hQW : Q ≤ W) (hmW : m < 2 ^ W) (hNW : NN < 2 ^ W) (hNN : NN ≤ N) (hmN : m ≤ N)
    (hL : D 30 = L.map (fun j : ℕ => (j : ℤ))) (hLm : L.length = m) (hLb : ∀ j ∈ L, j ≤ 2 ^ W)
    (h53 : D 53 = []) (h54 : D 54 = [])
    (hSC : D SC = ((List.range NN).map gc).reverse) (hSV : D SV = ((List.range NN).map gv).reverse)
    (bc : ∀ i < NN, |gc i| ≤ 2 ^ W) (bv : ∀ i < NN, |gv i| ≤ 2 ^ W)
    (bS : ∀ k < m, ∀ K ≤ NN, |(if a = Lg L k then (2 : ℤ) ^ Q else 0) +
      ∑ y ∈ range K, cTm gv gc (Lg L k) y| ≤ 2 ^ W) :
    Rn PJ.colL v D (fun v' => Fxk [1, 3, 4, 5, 8, 12, 29] v v' ∧ BV W v')
      (update D SMAT (rvL (fun k => cEnt Q a gv gc NN (Lg L k)) m ++ D SMAT))
      (cFor W m (cColB W N NN)) := 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.colL`, Solutions/J6SegILPreJK8.lean (lines 192–307) of the round-six development.

View graph