Stage 3 (round six, `jS3`)

Proved

J6Seg.PJ.Rn.jS3

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

complexity-theoryinteger-multiplicationkappa-improvement

Stage 3.

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

theorem J6Seg.PJ.Rn.jS3 {Q W N s lam w kJ : ℕ} {L : List ℕ} {A : ℕ → ℕ → ℤ} {v : Vr} {c : Cs}
    {a1 a2 a3 a4 : ℤ}
    (hN : N ≤ 2 ^ W) (hN5 : 5 ≤ N) (hW2 : 2 ≤ W) (hv : BV W v)
    (h9 : v 9 = 2 ^ Q) (h10 : v 10 = 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, a2, a3, a4]) (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)
    (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) :
    Rn J6Seg.PJ.jS3 v c (fun v' => (∀ j ∈ ([9, 10, 20, 24, 25, 26] : List (Fin HS)), v' j = v j) ∧
        v' 21 = ((2 ^ kJ : ℕ) : ℤ) ∧ v' 28 = L.length ∧
        v' 22 = JK.nBd (bsOf Q L (lam + w) (s - lam - w) A) ∧
        v' 23 = ((JK.flatT (fsOf Q L (lam + w) (s - lam - w) A) ++
          JK.flatB kJ (bsOf Q L (lam + w) (s - lam - w) A)).length : ℤ) ∧ BV W v')
      (update (update c 14 (matL (Mseq Q (bandS (lam + w) (s - lam - w)) L A L.length) L.length)) 41
        (JK.flatT (fsOf Q L (lam + w) (s - lam - w) A) ++
          JK.flatB kJ (bsOf Q L (lam + w) (s - lam - w) A) ++ c 41))
      (cJS3 W N L.length)

Context. B5 J side, part K18: stage 3 — elimination and serialization

jS3 = (11 := λ+w; 12 := (s-λ-w)⁺; 21 := 2^kJ); elimP; (28 := m; 11; 12); serP (Rn.jS3): flatT fs ++ flatB kJ bs in front of 41, 22 := nBd bs, 23 := its length.

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

Formal statement

theorem J6Seg.PJ.Rn.jS3 {Q W N s lam w kJ : ℕ} {L : List ℕ} {A : ℕ → ℕ → ℤ} {v : Vr} {c : Cs}
    {a1 a2 a3 a4 : ℤ}
    (hN : N ≤ 2 ^ W) (hN5 : 5 ≤ N) (hW2 : 2 ≤ W) (hv : BV W v)
    (h9 : v 9 = 2 ^ Q) (h10 : v 10 = 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, a2, a3, a4]) (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)
    (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) :
    Rn J6Seg.PJ.jS3 v c (fun v' => (∀ j ∈ ([9, 10, 20, 24, 25, 26] : List (Fin HS)), v' j = v j) ∧
        v' 21 = ((2 ^ kJ : ℕ) : ℤ) ∧ v' 28 = L.length ∧
        v' 22 = JK.nBd (bsOf Q L (lam + w) (s - lam - w) A) ∧
        v' 23 = ((JK.flatT (fsOf Q L (lam + w) (s - lam - w) A) ++
          JK.flatB kJ (bsOf Q L (lam + w) (s - lam - w) A)).length : ℤ) ∧ BV W v')
      (update (update c 14 (matL (Mseq Q (bandS (lam + w) (s - lam - w)) L A L.length) L.length)) 41
        (JK.flatT (fsOf Q L (lam + w) (s - lam - w) A) ++
          JK.flatB kJ (bsOf Q L (lam + w) (s - lam - w) A) ++ c 41))
      (cJS3 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.jS3`, Solutions/J6SegILPreJK18.lean (lines 33–178) of the round-six development.

View graph