Round-six lemma `cwB`

Proved

J6Seg.PJ.Rn.cwB

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

theorem J6Seg.PJ.Rn.cwB (hN : N ≤ 2 ^ W) (hW2 : 2 ≤ W) (hu : BV W u)
    (h4 : u 4 = b) (h8 : u 8 = y) (h11 : u 11 = NN) (hy : y < NN) (hNN : NN ≤ N)
    (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 : |u 5 + cTm gv gc b y| ≤ 2 ^ W) :
    Rn (progL PJ.cwB) u D (fun v' => v' 5 = u 5 + cTm gv gc b y ∧ Fxk [1, 5, 12, 29] u v' ∧ BV W v') D
      (costL W N PJ.cwB)

Context. B5 J side, part K6: the capacitance entry as a slot sum

capI_slots: capI a b = [a = b] 2^P + Σ_{y < n (2w+1)} [gC y = b] gV y;
PJ.cwB / PJ.cwL = forL 54 11 8 PJ.cwB: 5 ← 5 + Σ_y [gC y = r4] gV y, reading SC, SV (reversed, length n (2w+1) on 11) (Rn.cwB, Rn.cwL).

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 {W N NN b y : ℕ} {gv gc : ℕ → ℤ} {u : Vr} {D : Cs}

Formal statement

theorem J6Seg.PJ.Rn.cwB (hN : N ≤ 2 ^ W) (hW2 : 2 ≤ W) (hu : BV W u)
    (h4 : u 4 = b) (h8 : u 8 = y) (h11 : u 11 = NN) (hy : y < NN) (hNN : NN ≤ N)
    (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 : |u 5 + cTm gv gc b y| ≤ 2 ^ W) :
    Rn (progL PJ.cwB) u D (fun v' => v' 5 = u 5 + cTm gv gc b y ∧ Fxk [1, 5, 12, 29] u v' ∧ BV W v') D
      (costL W N PJ.cwB) := 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.cwB`, Solutions/J6SegILPreJK6.lean (lines 46–122) of the round-six development.

View graph