Stage 4b (round six, `jS4b`)

Proved

J6Seg.PJ.Rn.jS4b

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

complexity-theoryinteger-multiplicationkappa-improvement

Stage 4b.

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

theorem J6Seg.PJ.Rn.jS4b {W N m : ℕ} {x0 x1 x2 x3 x4 : ℤ} {L Mx : List ℤ} {v : Vr} {c : Cs}
    (hN : N ≤ 2 ^ W) (hN5 : 5 ≤ N) (hW2 : 2 ≤ W) (hv : BV W v)
    (h5 : v 5 = ((2 ^ Nat.clog 2 m : ℕ) : ℤ)) (h6 : v 6 = Nat.clog 2 m) (h28 : v 28 = m)
    (hSt : c J6Seg.PJ.sSt = [x0, x1, x2, x3, x4]) (hStb : ∀ x ∈ c J6Seg.PJ.sSt, |x| ≤ 2 ^ W)
    (h30 : c 30 = L) (hLl : L.length = m) (hLb : ∀ x ∈ L, |x| ≤ 2 ^ W)
    (h31 : c 31 = [(m : ℤ)]) (h14 : c 14 = Mx) (hMl : Mx.length = m * m)
    (hMb : ∀ x ∈ Mx, |x| ≤ 2 ^ W) (h50 : c 50 = []) (hmm : m * m ≤ 2 ^ W) :
    Rn J6Seg.PJ.jS4b v c (fun v' => BV W v')
      (update (update (update (update (update c sX
        (jVs x2 x4 x3 ((2 ^ Nat.clog 2 m : ℕ) : ℤ) (Nat.clog 2 m) ++ c sX)) J6Seg.PJ.sSt []) 30 []) 31 []) 14 [])
      (cJS4b W N m)

Context. B5 J side, part K21: stage 4b — the register values and the last clears

jS4b = (3, 4, 7 := pre, post, wd from the stash; 29 := 1); cMid; drop the stash; clear 30, 31, 14 (Rn.jS4b): the values ρ 0 … ρ 8 of the J pass on sX.

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.jS4b {W N m : ℕ} {x0 x1 x2 x3 x4 : ℤ} {L Mx : List ℤ} {v : Vr} {c : Cs}
    (hN : N ≤ 2 ^ W) (hN5 : 5 ≤ N) (hW2 : 2 ≤ W) (hv : BV W v)
    (h5 : v 5 = ((2 ^ Nat.clog 2 m : ℕ) : ℤ)) (h6 : v 6 = Nat.clog 2 m) (h28 : v 28 = m)
    (hSt : c J6Seg.PJ.sSt = [x0, x1, x2, x3, x4]) (hStb : ∀ x ∈ c J6Seg.PJ.sSt, |x| ≤ 2 ^ W)
    (h30 : c 30 = L) (hLl : L.length = m) (hLb : ∀ x ∈ L, |x| ≤ 2 ^ W)
    (h31 : c 31 = [(m : ℤ)]) (h14 : c 14 = Mx) (hMl : Mx.length = m * m)
    (hMb : ∀ x ∈ Mx, |x| ≤ 2 ^ W) (h50 : c 50 = []) (hmm : m * m ≤ 2 ^ W) :
    Rn J6Seg.PJ.jS4b v c (fun v' => BV W v')
      (update (update (update (update (update c sX
        (jVs x2 x4 x3 ((2 ^ Nat.clog 2 m : ℕ) : ℤ) (Nat.clog 2 m) ++ c sX)) J6Seg.PJ.sSt []) 30 []) 31 []) 14 [])
      (cJS4b 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.jS4b`, Solutions/J6SegILPreJK21.lean (lines 32–147) of the round-six development.

View graph