The `J` core (round six, `eJcore`)

Proved

J6Seg.PJ.Rn.eJcore

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

complexity-theoryinteger-multiplicationkappa-improvement

The J core.

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

theorem J6Seg.PJ.Rn.eJcore {kA kC wA wC k pre post s t p α d W N : ℕ} {Z : Fin HS}
    (hZ : Z ∉ rg) (hZ5 : Z.val < 56) (hZT : Z ≠ sTmp) (hZC : Z ≠ cRdC)
    {c : Cs} (hcZ : c Z = dsc k pre post s t p α d) (hZv : Z.val = 49 ∨ Z.val = 55)
    (hc : ∀ j, j ≠ Z → c j = [])
    (hW : parBig kA kC wA wC k pre post s t p α d < 2 ^ W)
    (hNW : N < 2 ^ W) (hW4 : 4 ≤ W) (hN5 : 5 ≤ N)
    (hs : 0 < s) (hws : wF d ≤ s) (hQW : segPF p d s ≤ W)
    (hsN : s ≤ N) (hlN : lamP d ≤ N) (hNMN : lamP d * (2 * wF d + 1) ≤ N)
    (hmm : (LJ s t (lamP d) (wF d)).length * (LJ s t (lamP d) (wF d)).length ≤ N)
    (hmc : (LJ s t (lamP d) (wF d)).length * (2 * wF d + 2) ≤ N)
    (bss : s * s ≤ 2 ^ W) (hlw : lamP d + wF d ≤ 2 ^ W)
    (hW8 : 8 * ((LJ s t (lamP d) (wF d)).length + 1) ^ 2 ≤ 2 ^ W)
    (hJB : JB (segPF p d s) (p / 7) W s t α (lamP d) (wF d))
    (hMb : ∀ q ≤ (LJ s t (lamP d) (wF d)).length, ∀ i < (LJ s t (lamP d) (wF d)).length,
      ∀ k < (LJ s t (lamP d) (wF d)).length,
      |Mseq (segPF p d s) (bandS (lamP d + wF d) (s - lamP d - wF d)) (LJ s t (lamP d) (wF d))
        (capI (segPF p d s) (mkTables (segPF p d s) (p / 7) s t α) (mkBlocks s t (lamP d) (wF d)))
        q i k| ≤ 2 ^ W)
    (hbl : (JK.jBody (kA * segPF p d s + kC) (JK.jFs (segPF p d s) (p / 7) s t (lamP d) (wF d) α)
      (JK.jBs (segPF p d s) (p / 7) s t (lamP d) (wF d) α)
      (JK.jCc (segPF p d s) (p / 7) s t (lamP d) (wF d) α (wF d))).length ≤ 2 ^ W) :
    Rn (J6Seg.PJ.eJcore kA kC wA wC Z) (fun _ => 0) c (BV W)
      (update (update (update c sX (cVals (wA * segPF p d s + wC)
        (Nat.clog 2 (LJ s t (lamP d) (wF d)).length) pre 1 post)) sOut
        (tabsT (fun _ => jTabX (segPF p d s) (p / 7) s t (lamP d) (wF d) α (kA * segPF p d s + kC))
          1)) sLn
        [((tabsT (fun _ => jTabX (segPF p d s) (p / 7) s t (lamP d) (wF d) α
          (kA * segPF p d s + kC)) 1).length : ℤ)])
      (cJHead kA kC wA wC W N d s p (LJ s t (lamP d) (wF d)).length +
        cJTail W N (LJ s t (lamP d) (wF d)).length)

Context. B5 J side, part K27: Rn.eJcore

The register-file core of the J set-up: from the descriptor on Z ∈ {49, 55} (all else empty) to cVals wd ⌈log₂ m⌉ pre 1 post on sX, tabsT (fun _ => jTab …) 1 on sOut and its length on sLn.

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.eJcore {kA kC wA wC k pre post s t p α d W N : ℕ} {Z : Fin HS}
    (hZ : Z ∉ rg) (hZ5 : Z.val < 56) (hZT : Z ≠ sTmp) (hZC : Z ≠ cRdC)
    {c : Cs} (hcZ : c Z = dsc k pre post s t p α d) (hZv : Z.val = 49 ∨ Z.val = 55)
    (hc : ∀ j, j ≠ Z → c j = [])
    (hW : parBig kA kC wA wC k pre post s t p α d < 2 ^ W)
    (hNW : N < 2 ^ W) (hW4 : 4 ≤ W) (hN5 : 5 ≤ N)
    (hs : 0 < s) (hws : wF d ≤ s) (hQW : segPF p d s ≤ W)
    (hsN : s ≤ N) (hlN : lamP d ≤ N) (hNMN : lamP d * (2 * wF d + 1) ≤ N)
    (hmm : (LJ s t (lamP d) (wF d)).length * (LJ s t (lamP d) (wF d)).length ≤ N)
    (hmc : (LJ s t (lamP d) (wF d)).length * (2 * wF d + 2) ≤ N)
    (bss : s * s ≤ 2 ^ W) (hlw : lamP d + wF d ≤ 2 ^ W)
    (hW8 : 8 * ((LJ s t (lamP d) (wF d)).length + 1) ^ 2 ≤ 2 ^ W)
    (hJB : JB (segPF p d s) (p / 7) W s t α (lamP d) (wF d))
    (hMb : ∀ q ≤ (LJ s t (lamP d) (wF d)).length, ∀ i < (LJ s t (lamP d) (wF d)).length,
      ∀ k < (LJ s t (lamP d) (wF d)).length,
      |Mseq (segPF p d s) (bandS (lamP d + wF d) (s - lamP d - wF d)) (LJ s t (lamP d) (wF d))
        (capI (segPF p d s) (mkTables (segPF p d s) (p / 7) s t α) (mkBlocks s t (lamP d) (wF d)))
        q i k| ≤ 2 ^ W)
    (hbl : (JK.jBody (kA * segPF p d s + kC) (JK.jFs (segPF p d s) (p / 7) s t (lamP d) (wF d) α)
      (JK.jBs (segPF p d s) (p / 7) s t (lamP d) (wF d) α)
      (JK.jCc (segPF p d s) (p / 7) s t (lamP d) (wF d) α (wF d))).length ≤ 2 ^ W) :
    Rn (J6Seg.PJ.eJcore kA kC wA wC Z) (fun _ => 0) c (BV W)
      (update (update (update c sX (cVals (wA * segPF p d s + wC)
        (Nat.clog 2 (LJ s t (lamP d) (wF d)).length) pre 1 post)) sOut
        (tabsT (fun _ => jTabX (segPF p d s) (p / 7) s t (lamP d) (wF d) α (kA * segPF p d s + kC))
          1)) sLn
        [((tabsT (fun _ => jTabX (segPF p d s) (p / 7) s t (lamP d) (wF d) α
          (kA * segPF p d s + kC)) 1).length : ℤ)])
      (cJHead kA kC wA wC W N d s p (LJ s t (lamP d) (wF d)).length +
        cJTail W N (LJ s t (lamP d) (wF d)).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.eJcore`, Solutions/J6SegILPreJK27.lean (lines 28–168) of the round-six development.

View graph