Stage 4a (round six, `jS4a`)

Proved

J6Seg.PJ.Rn.jS4a

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

complexity-theoryinteger-multiplicationkappa-improvement

Stage 4a.

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

theorem J6Seg.PJ.Rn.jS4a {W N m : ℕ} {a9 a10 a21 nB w l1 : ℤ} {v : Vr} {c : Cs} (hN : N ≤ 2 ^ W)
    (hW4 : 4 ≤ W) (hv : BV W v)
    (h9 : v 9 = a9) (h10 : v 10 = a10) (h21 : v 21 = a21) (h22 : v 22 = nB) (h23 : v 23 = l1)
    (h26 : v 26 = w) (h28 : v 28 = m) (hm : 2 * m + 2 < 2 ^ W)
    (hbl : 0 ≤ l1 + m * (2 * w + 2) ∧ l1 + m * (2 * w + 2) ≤ 2 ^ W) (hcL : c cLC = []) :
    Rn J6Seg.PJ.jS4a v c (fun v' => v' 6 = Nat.clog 2 m ∧ v' 5 = ((2 ^ Nat.clog 2 m : ℕ) : ℤ) ∧
        (∀ j ∉ ([5, 6, 23, 24] : List (Fin HS)), v' j = v j) ∧ BV W v')
      (update (update c sOut (hdrL a9 a10 a21 nB w (l1 + m * (2 * w + 2)) m ++ c sOut)) sLn
        ((l1 + m * (2 * w + 2) + 9) :: c sLn))
      (cJS4a W N m)

Context. B5 J side, part K20: stage 4a — the header of jTab

jS4a = (23 := |body|; 24 := m; 5 := 1; 6 := 0); clog loop (6 := ⌈log₂ m⌉, 5 := G); push the header and the segment length on 41, the table length on 42`` (Rn.jS4a).

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.jS4a {W N m : ℕ} {a9 a10 a21 nB w l1 : ℤ} {v : Vr} {c : Cs} (hN : N ≤ 2 ^ W)
    (hW4 : 4 ≤ W) (hv : BV W v)
    (h9 : v 9 = a9) (h10 : v 10 = a10) (h21 : v 21 = a21) (h22 : v 22 = nB) (h23 : v 23 = l1)
    (h26 : v 26 = w) (h28 : v 28 = m) (hm : 2 * m + 2 < 2 ^ W)
    (hbl : 0 ≤ l1 + m * (2 * w + 2) ∧ l1 + m * (2 * w + 2) ≤ 2 ^ W) (hcL : c cLC = []) :
    Rn J6Seg.PJ.jS4a v c (fun v' => v' 6 = Nat.clog 2 m ∧ v' 5 = ((2 ^ Nat.clog 2 m : ℕ) : ℤ) ∧
        (∀ j ∉ ([5, 6, 23, 24] : List (Fin HS)), v' j = v j) ∧ BV W v')
      (update (update c sOut (hdrL a9 a10 a21 nB w (l1 + m * (2 * w + 2)) m ++ c sOut)) sLn
        ((l1 + m * (2 * w + 2) + 9) :: c sLn))
      (cJS4a W N m) := 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.jS4a`, Solutions/J6SegILPreJK20.lean (lines 46–117) of the round-six development.

View graph