Round-six lemma `jB`

Proved

J6Seg.PJ.Rn.jB

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

theorem J6Seg.PJ.Rn.jB (hN : N ≤ 2 ^ W) (hW2 : 2 ≤ W) (hu : BV W u)
    (h1 : u 1 = B.st l) (h2 : u 2 = B.len l) (h4 : u 4 = b) (h5 : u 5 = j) (h7 : u 7 = l)
    (h20 : u 20 = Q) (h22 : u 22 = s) (h23 : u 23 = t) (h25 : u 25 = α) (h26 : u 26 = B.w)
    (hBs : B.s = s) (hs : 0 < s) (hQW : Q ≤ W + 1)
    (hcpl : ∀ i h, T.cpl i h = HvdH.expNeg Q (s ^ 2) (α ^ 2 * (HvdH.eKz s t i h).toNat))
    (bss : s * s ≤ 2 ^ W)
    (bX : α ^ 2 * (HvdH.eKz s t (l : ℤ) ((j : ℤ) - B.w)).toNat ≤ 2 ^ W)
    (bC : |T.cpl l ((j : ℤ) - B.w)| ≤ 2 ^ W)
    (bS : |u 8 + ccT T B l b j| ≤ 2 ^ W) :
    Rn (progL PJ.jB) u D (fun v' => v' 8 = u 8 + ccT T B l b j ∧ Fxk [8, 12, 29] u v' ∧ BV W v') D
      (costL W N PJ.jB)

Context. B5 J side, part K13: the coupling-window entry, innermost loop

For a row position l (on 7, block c = st l on 1, n = len l on 2), a target column b (on 4) and a slot j (on 5), ccT l b j = [hcT ∧ col = b] cpl l (j - w); the body jB adds it to 8 with one expNeg call (Rn.jB); jL = forL 54 11 5 jB sums it over j < 2w + 1 (count on 11), which is ccOf (Rn.jL).

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 : ℕ} {T : Tables} {B : Blocks} {u : Vr} {D : Cs} {l b j s t α : ℕ}

Formal statement

theorem J6Seg.PJ.Rn.jB (hN : N ≤ 2 ^ W) (hW2 : 2 ≤ W) (hu : BV W u)
    (h1 : u 1 = B.st l) (h2 : u 2 = B.len l) (h4 : u 4 = b) (h5 : u 5 = j) (h7 : u 7 = l)
    (h20 : u 20 = Q) (h22 : u 22 = s) (h23 : u 23 = t) (h25 : u 25 = α) (h26 : u 26 = B.w)
    (hBs : B.s = s) (hs : 0 < s) (hQW : Q ≤ W + 1)
    (hcpl : ∀ i h, T.cpl i h = HvdH.expNeg Q (s ^ 2) (α ^ 2 * (HvdH.eKz s t i h).toNat))
    (bss : s * s ≤ 2 ^ W)
    (bX : α ^ 2 * (HvdH.eKz s t (l : ℤ) ((j : ℤ) - B.w)).toNat ≤ 2 ^ W)
    (bC : |T.cpl l ((j : ℤ) - B.w)| ≤ 2 ^ W)
    (bS : |u 8 + ccT T B l b j| ≤ 2 ^ W) :
    Rn (progL PJ.jB) u D (fun v' => v' 8 = u 8 + ccT T B l b j ∧ Fxk [8, 12, 29] u v' ∧ BV W v') D
      (costL W N PJ.jB) := 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.jB`, Solutions/J6SegILPreJK13.lean (lines 78–155) of the round-six development.

View graph