The native chunk set-up (round six, `eCn_sp`)

Proved

J6Seg.PJ.eCn_sp

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

complexity-theoryinteger-multiplicationkappa-improvement

The native chunk set-up.

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

theorem J6Seg.PJ.eCn_sp (pl : Plan6) {k pre post s t p α d W M B : ℕ} {Zn : Fin HS}
    (hZ : Zn ∉ rg) (hZ5 : Zn.val < 56) (hZT : Zn ≠ sTmp) (hZC : Zn ≠ cRdC) (hZ2 : Zn ≠ sT2)
    (hZx : Zn ≠ J6Seg.PJ.sSt ∧ Zn ≠ sX ∧ Zn ≠ sOut ∧ Zn ≠ sLn ∧ Zn ≠ cLC ∧ Zn ≠ 13 ∧ Zn ≠ 51 ∧ Zn ≠ 53 ∧
      Zn ≠ 54 ∧ Zn ≠ PreT.Cu)
    (oN : Fin 19 → Fin HS) (hinj : Injective oN) (hlt : ∀ i, (oN i).val < 56)
    (hx : ∀ i, oN i ≠ sX ∧ oN i ≠ sLn ∧ oN i ≠ sOut ∧ oN i ≠ sT2 ∧ oN i ≠ cLC) (hZo : ∀ i, oN i ≠ Zn)
    (hW : parBig pl.kA pl.kC pl.wA pl.wC k pre post s t p α d < 2 ^ W)
    (bpk : pl.pkA * segPF p d s + pl.pkC ≤ 2 ^ W) (bb : pl.bA * segPF p d s + pl.bC ≤ 2 ^ W)
    (bl : pl.pkA + pl.pkC + pl.bA + pl.bC + 2 ≤ 2 ^ W)
    (hPA : segPF p d s ≤ W) (hA2 : 2 ≤ W)
    (TB : PreT.TabB (segPF p d s) (p / 7) s t α (lamP d) W)
    (hpkM : pl.pkA * segPF p d s + pl.pkC ≤ M) (hbM : pl.bA * segPF p d s + pl.bC ≤ M)
    (hncA : t / lamP d * lamP d ≤ 2 ^ W) (hncA' : t / lamP d * (9 + 10 * lamP d) ≤ 2 ^ W)
    (hvB : ∀ a ∈ cVals (pl.wA * segPF p d s + pl.wC) (Nat.log 2 (lamF d)) pre (t / lamP d) post,
      zsz a ≤ B)
    (hlB : zsz ((tabsT (PreT.tabQ2 (segPF p d s) (p / 7) s t (lamP d) α
      (pl.pkA * segPF p d s + pl.pkC) (pl.bA * segPF p d s + pl.bC)) (t / lamP d)).length : ℤ) ≤ B)
    (hTB : Bnd B (tabsT (PreT.tabQ2 (segPF p d s) (p / 7) s t (lamP d) α
      (pl.pkA * segPF p d s + pl.pkC) (pl.bA * segPF p d s + pl.bC)) (t / lamP d)))
    (s0 : IState HS) :
    Sp (eCn pl Zn oN) (encK s0 (F0 Zn (dsc k pre post s t p α d)))
      (encK s0 (extend oN (kerRegs (pl.wA * segPF p d s + pl.wC) (pl.wA * segPF p d s + pl.wC)
        (Nat.log 2 (lamF d)) pre (t / lamP d) post
        (tabsT (PreT.tabQ2 (segPF p d s) (p / 7) s t (lamP d) α
          (pl.pkA * segPF p d s + pl.pkC) (pl.bA * segPF p d s + pl.bC)) (t / lamP d)))
        (F0 Zn (dsc k pre post s t p α d))))
      (cECn pl W d (NF d s) (segPF p d s) (lamP d) (p / 7) M (t / lamP d) B
        (tabsT (PreT.tabQ2 (segPF p d s) (p / 7) s t (lamP d) α
          (pl.pkA * segPF p d s + pl.pkC) (pl.bA * segPF p d s + pl.bC)) (t / lamP d)).length)

Context. B5 chunk side, part 10: the native set-up pair eCn / tearP

eCn = initP rg; eCcore; finiP rg; distAll oN: from the descriptor alone on Zn to the chunk-pass register file kerRegs … on oN (eCn_sp).

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.eCn_sp (pl : Plan6) {k pre post s t p α d W M B : ℕ} {Zn : Fin HS}
    (hZ : Zn ∉ rg) (hZ5 : Zn.val < 56) (hZT : Zn ≠ sTmp) (hZC : Zn ≠ cRdC) (hZ2 : Zn ≠ sT2)
    (hZx : Zn ≠ J6Seg.PJ.sSt ∧ Zn ≠ sX ∧ Zn ≠ sOut ∧ Zn ≠ sLn ∧ Zn ≠ cLC ∧ Zn ≠ 13 ∧ Zn ≠ 51 ∧ Zn ≠ 53 ∧
      Zn ≠ 54 ∧ Zn ≠ PreT.Cu)
    (oN : Fin 19 → Fin HS) (hinj : Injective oN) (hlt : ∀ i, (oN i).val < 56)
    (hx : ∀ i, oN i ≠ sX ∧ oN i ≠ sLn ∧ oN i ≠ sOut ∧ oN i ≠ sT2 ∧ oN i ≠ cLC) (hZo : ∀ i, oN i ≠ Zn)
    (hW : parBig pl.kA pl.kC pl.wA pl.wC k pre post s t p α d < 2 ^ W)
    (bpk : pl.pkA * segPF p d s + pl.pkC ≤ 2 ^ W) (bb : pl.bA * segPF p d s + pl.bC ≤ 2 ^ W)
    (bl : pl.pkA + pl.pkC + pl.bA + pl.bC + 2 ≤ 2 ^ W)
    (hPA : segPF p d s ≤ W) (hA2 : 2 ≤ W)
    (TB : PreT.TabB (segPF p d s) (p / 7) s t α (lamP d) W)
    (hpkM : pl.pkA * segPF p d s + pl.pkC ≤ M) (hbM : pl.bA * segPF p d s + pl.bC ≤ M)
    (hncA : t / lamP d * lamP d ≤ 2 ^ W) (hncA' : t / lamP d * (9 + 10 * lamP d) ≤ 2 ^ W)
    (hvB : ∀ a ∈ cVals (pl.wA * segPF p d s + pl.wC) (Nat.log 2 (lamF d)) pre (t / lamP d) post,
      zsz a ≤ B)
    (hlB : zsz ((tabsT (PreT.tabQ2 (segPF p d s) (p / 7) s t (lamP d) α
      (pl.pkA * segPF p d s + pl.pkC) (pl.bA * segPF p d s + pl.bC)) (t / lamP d)).length : ℤ) ≤ B)
    (hTB : Bnd B (tabsT (PreT.tabQ2 (segPF p d s) (p / 7) s t (lamP d) α
      (pl.pkA * segPF p d s + pl.pkC) (pl.bA * segPF p d s + pl.bC)) (t / lamP d)))
    (s0 : IState HS) :
    Sp (eCn pl Zn oN) (encK s0 (F0 Zn (dsc k pre post s t p α d)))
      (encK s0 (extend oN (kerRegs (pl.wA * segPF p d s + pl.wC) (pl.wA * segPF p d s + pl.wC)
        (Nat.log 2 (lamF d)) pre (t / lamP d) post
        (tabsT (PreT.tabQ2 (segPF p d s) (p / 7) s t (lamP d) α
          (pl.pkA * segPF p d s + pl.pkC) (pl.bA * segPF p d s + pl.bC)) (t / lamP d)))
        (F0 Zn (dsc k pre post s t p α d))))
      (cECn pl W d (NF d s) (segPF p d s) (lamP d) (p / 7) M (t / lamP d) B
        (tabsT (PreT.tabQ2 (segPF p d s) (p / 7) s t (lamP d) α
          (pl.pkA * segPF p d s + pl.pkC) (pl.bA * segPF p d s + pl.bC)) (t / lamP 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.eCn_sp`, Solutions/J6SegILPreJC10.lean (lines 61–123) of the round-six development.

View graph