The tail (round six, `jTail`)

Proved

J6Seg.PJ.Rn.jTail

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

theorem J6Seg.PJ.Rn.jTail {Q W N s lam w kJ : ℕ} {L : List ℕ} {A : ℕ → ℕ → ℤ} {v : Vr} {c : Cs}
    {a1 wd pre post a9 a10 : ℤ}
    (hN : N ≤ 2 ^ W) (hN5 : 5 ≤ N) (hW4 : 4 ≤ W) (hv : BV W v)
    (h9 : v 9 = a9) (h10 : v 10 = a10) (h9' : a9 = 2 ^ Q) (h10' : a10 = 2 ^ (Q + 1))
    (h22 : v 22 = s) (h24 : v 24 = lam) (h26 : v 26 = w) (h28 : v 28 = L.length)
    (hSt : c J6Seg.PJ.sSt = [((2 ^ kJ : ℕ) : ℤ), a1, wd, post, pre]) (hStb : ∀ x ∈ c J6Seg.PJ.sSt, |x| ≤ 2 ^ W)
    (h30 : c 30 = L.map (fun j : ℕ => (j : ℤ))) (h31 : c 31 = [(L.length : ℤ)])
    (h14 : c 14 = matL (fun i k => A (Lg L i) (Lg L k)) L.length)
    (hE : ∀ j ∈ ([15, 16, 17, 18, 19, 27, 47, 48, 50, 51] : List (Fin HS)), c j = [])
    (hlwW : lam + w ≤ 2 ^ W) (hsW : s ≤ 2 ^ W)
    (hW8 : 8 * (L.length + 1) ^ 2 ≤ 2 ^ W) (hLb : ∀ j ∈ L, j ≤ 2 ^ W)
    (hmm : L.length * L.length ≤ 2 ^ W) (hm2 : 2 * L.length + 2 < 2 ^ W)
    (hMb : ∀ q ≤ L.length, ∀ i < L.length, ∀ k < L.length,
      |Mseq Q (bandS (lam + w) (s - lam - w)) L A q i k| ≤ 2 ^ W)
    (hbl : ((JK.flatT (fsOf Q L (lam + w) (s - lam - w) A) ++
      JK.flatB kJ (bsOf Q L (lam + w) (s - lam - w) A)).length : ℤ) + L.length * (2 * (w : ℤ) + 2)
        ≤ 2 ^ W) :
    Rn J6Seg.PJ.jTail v c (BV W) (tailSt Q kJ s lam w L A a9 a10 wd pre post c) (cJTail W N L.length)

Context. B5 J side, part K22: the tail jS3; jS4a; jS4b

From the capacitance matrix on 14, the coupling rows in front of 41, the line on 30, [m] on 31 and the stash [2^kJ, kJ, wd, post, pre]: elimination, serialization, header, register values, clean-up (Rn.jTail).

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

Formal statement

theorem J6Seg.PJ.Rn.jTail {Q W N s lam w kJ : ℕ} {L : List ℕ} {A : ℕ → ℕ → ℤ} {v : Vr} {c : Cs}
    {a1 wd pre post a9 a10 : ℤ}
    (hN : N ≤ 2 ^ W) (hN5 : 5 ≤ N) (hW4 : 4 ≤ W) (hv : BV W v)
    (h9 : v 9 = a9) (h10 : v 10 = a10) (h9' : a9 = 2 ^ Q) (h10' : a10 = 2 ^ (Q + 1))
    (h22 : v 22 = s) (h24 : v 24 = lam) (h26 : v 26 = w) (h28 : v 28 = L.length)
    (hSt : c J6Seg.PJ.sSt = [((2 ^ kJ : ℕ) : ℤ), a1, wd, post, pre]) (hStb : ∀ x ∈ c J6Seg.PJ.sSt, |x| ≤ 2 ^ W)
    (h30 : c 30 = L.map (fun j : ℕ => (j : ℤ))) (h31 : c 31 = [(L.length : ℤ)])
    (h14 : c 14 = matL (fun i k => A (Lg L i) (Lg L k)) L.length)
    (hE : ∀ j ∈ ([15, 16, 17, 18, 19, 27, 47, 48, 50, 51] : List (Fin HS)), c j = [])
    (hlwW : lam + w ≤ 2 ^ W) (hsW : s ≤ 2 ^ W)
    (hW8 : 8 * (L.length + 1) ^ 2 ≤ 2 ^ W) (hLb : ∀ j ∈ L, j ≤ 2 ^ W)
    (hmm : L.length * L.length ≤ 2 ^ W) (hm2 : 2 * L.length + 2 < 2 ^ W)
    (hMb : ∀ q ≤ L.length, ∀ i < L.length, ∀ k < L.length,
      |Mseq Q (bandS (lam + w) (s - lam - w)) L A q i k| ≤ 2 ^ W)
    (hbl : ((JK.flatT (fsOf Q L (lam + w) (s - lam - w) A) ++
      JK.flatB kJ (bsOf Q L (lam + w) (s - lam - w) A)).length : ℤ) + L.length * (2 * (w : ℤ) + 2)
        ≤ 2 ^ W) :
    Rn J6Seg.PJ.jTail v c (BV W) (tailSt Q kJ s lam w L A a9 a10 wd pre post c) (cJTail W N L.length) := 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.jTail`, Solutions/J6SegILPreJK22.lean (lines 38–112) of the round-six development.

View graph