Round-six lemma `jKprog_spec`

Proved

J6Seg.JK.jKprog_spec

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

complexity-theoryinteger-multiplicationkappa-improvement

An auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.

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

theorem J6Seg.JK.jKprog_spec {M : MulSpec} {Φm Bx : ℕ} (hMB : MulBnd M (k + 2) Φm) (s : IState HS)
    {F0 : Fin HS → List ℤ} {x : List GI} {l : List ℤ}
    (hF0 : ∀ j, j ≠ 0 → j ≠ dTJ → F0 j = []) (hT : F0 dTJ = jTab P k K G fs bs cc)
    (h0 : F0 0 = gflat x ++ l) (hP : JPre P k K G Xb Bc fs bs cc x) (hBx : 3 * k + 10 ≤ Bx) :
    MSp M jKprog (encK s F0)
      (encK s (update F0 0 (gflat (liftG (jKerG P K G fs.length fs bs cc) x) ++ l)))
      (jC k K G fs bs cc (uC Φm Bx Bc))

Context. B-line IL, the J kernel (B4), part 17: jKprog_spec

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_Defs66

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.JK
open IntMul NLogN NLogN.KIL NLogN.KFB Function Finset
variable {P k K G Xb Bc : ℕ} {fs : List (List ℤ)} {bs : List (List ℤ × List ℤ × ℤ × ℤ)}
  {cc : List (List ℤ)}

Formal statement

theorem J6Seg.JK.jKprog_spec {M : MulSpec} {Φm Bx : ℕ} (hMB : MulBnd M (k + 2) Φm) (s : IState HS)
    {F0 : Fin HS → List ℤ} {x : List GI} {l : List ℤ}
    (hF0 : ∀ j, j ≠ 0 → j ≠ dTJ → F0 j = []) (hT : F0 dTJ = jTab P k K G fs bs cc)
    (h0 : F0 0 = gflat x ++ l) (hP : JPre P k K G Xb Bc fs bs cc x) (hBx : 3 * k + 10 ≤ Bx) :
    MSp M jKprog (encK s F0)
      (encK s (update F0 0 (gflat (liftG (jKerG P K G fs.length fs bs cc) x) ++ l)))
      (jC k K G fs bs cc (uC Φm Bx 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.JK.jKprog_spec`, Solutions/J6SegILJKer17.lean (lines 20–233) of the round-six development.

View graph