The tail (round six, `miT`)

Proved

J6Seg.PJ.Rn.miT

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

complexity-theoryinteger-multiplicationkappa-improvement

The tail.

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

theorem J6Seg.PJ.Rn.miT (hN : N ≤ 2 ^ W) (hW2 : 2 ≤ W) (hu : BV W u)
    (h1 : u 1 = c) (h2 : u 2 = n) (h3 : u 3 = uu) (h7 : u 7 = a) (h24 : u 24 = lam)
    (h26 : u 26 = w) (h9 : u 9 = 2 ^ Q) (h10 : u 10 = 2 ^ (Q + 1))
    (hBc : B.st a = c) (hBn : B.len a = n) (hBw : B.w = w)
    (h8 : u 8 = ∑ k ∈ range n, tsT Q T c (tU w n (a - c) uu) (tV w n (a - c) uu) k)
    (hca : c ≤ a) (hua : a - c < n) (huu : uu < n) (hnl : n ≤ lam) (hlN : lam ≤ N)
    (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)
    (bGI : ∀ i < lam, |T.gi i| ≤ 2 ^ W) (bDD : ∀ i < lam, |T.dd i| ≤ 2 ^ W)
    (bDI : ∀ i < lam, |T.di i| ≤ 2 ^ W)
    (bY : |fmul Q (fmul Q (T.gi (tU w n (a - c) uu)) (T.gi (tV w n (a - c) uu))) (fmul Q (u 8) 1)| ≤
      2 ^ W)
    (bM : |miV Q T B a uu| ≤ 2 ^ W) :
    Rn (progL PJ.miT) u D (fun v' => Fxk [4, 5, 8, 29] u v' ∧ BV W v')
      (update D SMI (miV Q T B a uu :: D SMI)) (costL W N PJ.miT)

Context. B5 J side, part K3: the TsumI loop and the M⁻¹ row tail

PJ.tsL = forL 51 2 4 PJ.tsB: 8 ← 8 + Σ_{k<n} tsT (Rn.tsL);
PJ.miT: from the sum on 8, the entry miV a u of the M⁻¹ row (tables SGI = 37, SDD = 35, SDI = 34, reversed, length λ), pushed on SMI = 40 (Rn.miT).

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_Defs70

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} {c n a uu lam w : ℕ}

Formal statement

theorem J6Seg.PJ.Rn.miT (hN : N ≤ 2 ^ W) (hW2 : 2 ≤ W) (hu : BV W u)
    (h1 : u 1 = c) (h2 : u 2 = n) (h3 : u 3 = uu) (h7 : u 7 = a) (h24 : u 24 = lam)
    (h26 : u 26 = w) (h9 : u 9 = 2 ^ Q) (h10 : u 10 = 2 ^ (Q + 1))
    (hBc : B.st a = c) (hBn : B.len a = n) (hBw : B.w = w)
    (h8 : u 8 = ∑ k ∈ range n, tsT Q T c (tU w n (a - c) uu) (tV w n (a - c) uu) k)
    (hca : c ≤ a) (hua : a - c < n) (huu : uu < n) (hnl : n ≤ lam) (hlN : lam ≤ N)
    (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)
    (bGI : ∀ i < lam, |T.gi i| ≤ 2 ^ W) (bDD : ∀ i < lam, |T.dd i| ≤ 2 ^ W)
    (bDI : ∀ i < lam, |T.di i| ≤ 2 ^ W)
    (bY : |fmul Q (fmul Q (T.gi (tU w n (a - c) uu)) (T.gi (tV w n (a - c) uu))) (fmul Q (u 8) 1)| ≤
      2 ^ W)
    (bM : |miV Q T B a uu| ≤ 2 ^ W) :
    Rn (progL PJ.miT) u D (fun v' => Fxk [4, 5, 8, 29] u v' ∧ BV W v')
      (update D SMI (miV Q T B a uu :: D SMI)) (costL W N PJ.miT) := 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.miT`, Solutions/J6SegILPreJK3.lean (lines 77–187) of the round-six development.

View graph