Round-six lemma `axB_run`

Proved

J6Seg.axB_run

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.J6SegILSweep8):

theorem J6Seg.axB_run (B k : ℕ) (hk : k ≤ D) (hb : SwB P n src D B) (s : IState HS)
    (F : Fin HS → List ℤ) (L : List GI) (l c17 : List ℤ) (hlen : L.length = TW P n D)
    (hgb : GB (pP6 P n + 2) L) :
    IRuns Isym tbl (axB σ dS dA eX)
      (encK s (SS σ dS F (gflat L ++ l) ((svW src D).drop k) (update (vK P n src D k) 17 c17)))
      (encK s (SS σ dS F (gflat (pf k L) ++ l) ((svW src D).drop (k + 1))
        (update (vK P n src D (k + 1)) 17 c17))) (cAx ⌊Cx⌋₊ B)

Context. B-line IL, B6 §8: one axis (axB_run) and the loop over the axes (swL_run)

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_Defs67

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function
variable {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp} {eX : Fin Pp}
  {σ : Fin 19 → Fin HS} {dS dA : Fin HS} (hW : SwOK σ dS dA)
  {P : Prm} {n : ℕ} {src : ℕ → ℕ} {D : ℕ} {Cx : ℝ}
  {pf : ℕ → List GI → List GI}
  (hX : AxisBodyF P n src D pf Isym tbl eX dA Cx) (hD : dP6 P n = D + 1)
include hW hX hD

Formal statement

theorem J6Seg.axB_run (B k : ℕ) (hk : k ≤ D) (hb : SwB P n src D B) (s : IState HS)
    (F : Fin HS → List ℤ) (L : List GI) (l c17 : List ℤ) (hlen : L.length = TW P n D)
    (hgb : GB (pP6 P n + 2) L) :
    IRuns Isym tbl (axB σ dS dA eX)
      (encK s (SS σ dS F (gflat L ++ l) ((svW src D).drop k) (update (vK P n src D k) 17 c17)))
      (encK s (SS σ dS F (gflat (pf k L) ++ l) ((svW src D).drop (k + 1))
        (update (vK P n src D (k + 1)) 17 c17))) (cAx ⌊Cx⌋₊ B) := 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.axB_run`, Solutions/J6SegILSweep8.lean (lines 39–99) of the round-six development.

View graph