The core program (round six, `sp_core`)

Proved

J6Seg.ATab.sp_core

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

complexity-theoryinteger-multiplicationkappa-improvement

The core program.

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

theorem J6Seg.ATab.sp_core {W k pre post s t p α d pkA pkC bA bC : ℕ} (st : IState HS)
    (F : Fin HS → List ℤ) (hF : ∀ j, j ≠ 31 → F j = [])
    (hF31 : F 31 = J6A.PA.dL k pre post s t p α d)
    (hdL : ∀ x ∈ J6A.PA.dL k pre post s t p α d, |x| < 2 ^ W) (hp1 : 1 ≤ p) (hα1 : 1 ≤ α)
    (hmW : sWidth p α + 4 ≤ W) (hP : PBnd W p t α pkA pkC bA bC) (hA : ABnd W p s t α)
    (hrW : 2 * (4 * J6A.WA p α (HAx p α) + 4 * HAx p α) < 2 ^ W) :
    Sp (coreUp pkA pkC bA bC) (encK st F)
      (encK st (coreOut F (vsA (p + 2) (pkA * p + pkC + 1) (Nat.log 2 (sWidth p α) + 3) pre
        (ncA p t α) post) (tabA p s t α (pkA * p + pkC) (bA * p + bC))))
      (cCore W p t α pkA pkC bA bC)

Context. A lines, table set-up, part 9: the core program (fixed layout)

coreUp = initP rg; parA; phase; tabLoop; finiP rg. sp_core: from a state with the descriptor on 31 and every other stack empty it leaves the kerRegs values ρ 0 … ρ 8 as the list vsA … on 45, [|T|] on 42 and T.reverse on 43 (coreOut), every other stack unchanged — the input of B5's distAll after one move.

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_Defs69

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.ATab
open IntMul NLogN NLogN.KIL NLogN.RS J6Seg.PJ IntMul.HvdH Function

Formal statement

theorem J6Seg.ATab.sp_core {W k pre post s t p α d pkA pkC bA bC : ℕ} (st : IState HS)
    (F : Fin HS → List ℤ) (hF : ∀ j, j ≠ 31 → F j = [])
    (hF31 : F 31 = J6A.PA.dL k pre post s t p α d)
    (hdL : ∀ x ∈ J6A.PA.dL k pre post s t p α d, |x| < 2 ^ W) (hp1 : 1 ≤ p) (hα1 : 1 ≤ α)
    (hmW : sWidth p α + 4 ≤ W) (hP : PBnd W p t α pkA pkC bA bC) (hA : ABnd W p s t α)
    (hrW : 2 * (4 * J6A.WA p α (HAx p α) + 4 * HAx p α) < 2 ^ W) :
    Sp (coreUp pkA pkC bA bC) (encK st F)
      (encK st (coreOut F (vsA (p + 2) (pkA * p + pkC + 1) (Nat.log 2 (sWidth p α) + 3) pre
        (ncA p t α) post) (tabA p s t α (pkA * p + pkC) (bA * p + bC))))
      (cCore W p t α pkA pkC bA bC) := 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.ATab.sp_core`, Solutions/J6AILTab9.lean (lines 106–151) of the round-six development.

View graph