Stage 1 (round six, `jS1`)

Proved

J6Seg.PJ.Rn.jS1

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

complexity-theoryinteger-multiplicationkappa-improvement

Stage 1.

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

theorem J6Seg.PJ.Rn.jS1 {W N : ℕ} {v : Vr} {c : Cs} {s t lam w : ℕ} (hN : N ≤ 2 ^ W) (hN1 : 1 ≤ N)
    (hv : BV W v) (h22 : v 22 = s) (h23 : v 23 = t) (h24 : v 24 = lam) (h26 : v 26 = w)
    (hs : 0 < s) (hl : 0 < lam) (hsW : s ≤ 2 ^ W) (htW : t ≤ 2 ^ W) (hlW : lam ≤ 2 ^ W)
    (hwW : w ≤ 2 ^ W) (hW2 : 2 ≤ W)
    (hSt : c J6Seg.PJ.sSt = []) (h30 : c 30 = []) (h31 : c 31 = []) (h32 : c 32 = []) (h33 : c 33 = []) :
    Rn J6Seg.PJ.jS1 v c (fun v' => v' = update (update v 29 0) 28
        ((Jlist (mkBlocks s t lam w)).length : ℤ) ∧ BV W v')
      (cS1 c v s t lam w) (cJS1 W N s)

Context. B5 J side, part K16: stash and the near-boundary line

jS1 = (stash 3, 4, 7, 11, 12 on sSt); ljP 22 23 24 26; 28 := |LJ| (read from 31): the line LJ on 30, block starts / lengths on 32 / 33 (Rn.jS1).

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.jS1 {W N : ℕ} {v : Vr} {c : Cs} {s t lam w : ℕ} (hN : N ≤ 2 ^ W) (hN1 : 1 ≤ N)
    (hv : BV W v) (h22 : v 22 = s) (h23 : v 23 = t) (h24 : v 24 = lam) (h26 : v 26 = w)
    (hs : 0 < s) (hl : 0 < lam) (hsW : s ≤ 2 ^ W) (htW : t ≤ 2 ^ W) (hlW : lam ≤ 2 ^ W)
    (hwW : w ≤ 2 ^ W) (hW2 : 2 ≤ W)
    (hSt : c J6Seg.PJ.sSt = []) (h30 : c 30 = []) (h31 : c 31 = []) (h32 : c 32 = []) (h33 : c 33 = []) :
    Rn J6Seg.PJ.jS1 v c (fun v' => v' = update (update v 29 0) 28
        ((Jlist (mkBlocks s t lam w)).length : ℤ) ∧ BV W v')
      (cS1 c v s t lam w) (cJS1 W N s) := 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.jS1`, Solutions/J6SegILPreJK16.lean (lines 56–112) of the round-six development.

View graph