Round-six lemma `miL`

Proved

J6Seg.PJ.Rn.miL

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.miL {v : Vr} (hN : N ≤ 2 ^ W) (hW2 : 2 ≤ W) (hv : BV W v)
    (h1 : v 1 = c) (h2 : v 2 = n) (h7 : v 7 = a) (h24 : v 24 = lam)
    (h26 : v 26 = w) (h9 : v 9 = 2 ^ Q) (h10 : v 10 = 2 ^ (Q + 1))
    (hBc : B.st a = c) (hBn : B.len a = n) (hBw : B.w = w)
    (hca : c ≤ a) (hua : a - c < n) (hnl : n ≤ lam) (hlN : lam ≤ N) (hnW : n < 2 ^ W)
    (hAP : D SAP = ((List.range n).map (T.ap c)).reverse)
    (hAM : D SAM = ((List.range n).map (T.am c)).reverse)
    (hGM : D SGM = ((List.range lam).map T.gam).reverse)
    (hGI : D SGI = ((List.range lam).map T.gi).reverse)
    (hDD : D SDD = ((List.range lam).map T.dd).reverse)
    (hDI : D SDI = ((List.range lam).map T.di).reverse)
    (h50 : D 50 = []) (h51 : D 51 = [])
    (bAP : ∀ i < n, |T.ap c i| ≤ 2 ^ W) (bAM : ∀ i < n, |T.am c i| ≤ 2 ^ W)
    (bGM : ∀ i < lam, |T.gam i| ≤ 2 ^ W) (bGI : ∀ i < lam, |T.gi i| ≤ 2 ^ W)
    (bDD : ∀ i < lam, |T.dd i| ≤ 2 ^ W) (bDI : ∀ i < lam, |T.di i| ≤ 2 ^ W)
    (bS : ∀ uu < n, ∀ K ≤ n,
      |∑ k ∈ range K, tsT Q T c (tU w n (a - c) uu) (tV w n (a - c) uu) k| ≤ 2 ^ W)
    (bY : ∀ uu < n, |fmul Q (fmul Q (T.gi (tU w n (a - c) uu)) (T.gi (tV w n (a - c) uu)))
      (fmul Q (∑ k ∈ range n, tsT Q T c (tU w n (a - c) uu) (tV w n (a - c) uu) k) 1)| ≤ 2 ^ W)
    (bM : ∀ uu < n, |miV Q T B a uu| ≤ 2 ^ W) :
    Rn PJ.miL v D (fun v' => Fxk [3, 4, 5, 8, 11, 12, 29] v v' ∧ BV W v')
      (update D SMI (rvL (miV Q T B a) n ++ D SMI)) (cFor W n (cMiB W N n))

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 : ℕ} {T : Tables} {B : Blocks} {D : Cs} {a c n lam w : ℕ}

Formal statement

theorem J6Seg.PJ.Rn.miL {v : Vr} (hN : N ≤ 2 ^ W) (hW2 : 2 ≤ W) (hv : BV W v)
    (h1 : v 1 = c) (h2 : v 2 = n) (h7 : v 7 = a) (h24 : v 24 = lam)
    (h26 : v 26 = w) (h9 : v 9 = 2 ^ Q) (h10 : v 10 = 2 ^ (Q + 1))
    (hBc : B.st a = c) (hBn : B.len a = n) (hBw : B.w = w)
    (hca : c ≤ a) (hua : a - c < n) (hnl : n ≤ lam) (hlN : lam ≤ N) (hnW : n < 2 ^ W)
    (hAP : D SAP = ((List.range n).map (T.ap c)).reverse)
    (hAM : D SAM = ((List.range n).map (T.am c)).reverse)
    (hGM : D SGM = ((List.range lam).map T.gam).reverse)
    (hGI : D SGI = ((List.range lam).map T.gi).reverse)
    (hDD : D SDD = ((List.range lam).map T.dd).reverse)
    (hDI : D SDI = ((List.range lam).map T.di).reverse)
    (h50 : D 50 = []) (h51 : D 51 = [])
    (bAP : ∀ i < n, |T.ap c i| ≤ 2 ^ W) (bAM : ∀ i < n, |T.am c i| ≤ 2 ^ W)
    (bGM : ∀ i < lam, |T.gam i| ≤ 2 ^ W) (bGI : ∀ i < lam, |T.gi i| ≤ 2 ^ W)
    (bDD : ∀ i < lam, |T.dd i| ≤ 2 ^ W) (bDI : ∀ i < lam, |T.di i| ≤ 2 ^ W)
    (bS : ∀ uu < n, ∀ K ≤ n,
      |∑ k ∈ range K, tsT Q T c (tU w n (a - c) uu) (tV w n (a - c) uu) k| ≤ 2 ^ W)
    (bY : ∀ uu < n, |fmul Q (fmul Q (T.gi (tU w n (a - c) uu)) (T.gi (tV w n (a - c) uu)))
      (fmul Q (∑ k ∈ range n, tsT Q T c (tU w n (a - c) uu) (tV w n (a - c) uu) k) 1)| ≤ 2 ^ W)
    (bM : ∀ uu < n, |miV Q T B a uu| ≤ 2 ^ W) :
    Rn PJ.miL v D (fun v' => Fxk [3, 4, 5, 8, 11, 12, 29] v v' ∧ BV W v')
      (update D SMI (rvL (miV Q T B a) n ++ D SMI)) (cFor W n (cMiB W N n)) := 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.miL`, Solutions/J6SegILPreJK8.lean (lines 80–165) of the round-six development.

View graph