Passes 2 and 6 (round six, `stepC`)

Proved

J6Seg.Ax.stepC

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

complexity-theoryinteger-multiplicationkappa-improvement

Passes 2 and 6 (the chunk kernel).

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

theorem J6Seg.Ax.stepC (hMul : MulOK Isym tbl pM NLogN.KFUU.MS) (hK : tbl e = KR.chunkI2 pM)
    (hFine : FineBody6 Isym tbl eF eB dF C₀) (hC0 : 0 ≤ C₀) (hR : RegOK ρ KR.dT dF)
    (hρA : ∀ i, ρ i ≠ dA) (hA0 : dA ≠ 0) (hTA : KR.dT ≠ dA)
    (hS : SetupBody6 Isym tbl eUp eDn ρ dA (descAx6 P n src D k) (chunkRegs6 P n src D k ap.pl) Cp)
    (hReg : AxReg P n src D k) (hTab : TabAt P n src k) (hgC : ChunkOutAt P ap n src k)
    (hBud : AxBudgetAt P ap n src D k Cc) :
    PassOK Isym tbl (kpSt eUp eDn ρ KR.dT dF eF eB e) dA (descAx6 P n src D k)
      (fun L => L.length = axpre6 P n D k * axnc6 P n k * (2 ^ axfC6 P n * axpost6 P n D k) ∧
        GB (axwd6 P n src k ap) L ∧ ∀ b < axpre6 P n D k * axnc6 P n k, ∀ c < axpost6 P n D k,
          (lineAt (2 ^ axfC6 P n) (axpost6 P n D k) L b c).length = axl6 P n ∧
          KR.AB (axX6 P n src k ap) (lineAt (2 ^ axfC6 P n) (axpost6 P n D k) L b c))
      (gY6 P n src D k) (2 * Cp + (2 * C₀ * Cc + Cc))

Context. B-line axis program (AxisU6), part 8: the kernel steps of axis k

stepC (passes 2, 6): kpass_ok with the chunk kernel KR.chunkK2_rowBody6 (B3) on dT = 49, the set-up chunkRegs6 (B5), the chunk table bound (TabAt), the chunk output bound (ChunkOutAt) and the budget;
stepJ (pass 4): kpass_ok with the J kernel JK.jKer_row (B4) on dTJ = 33, the set-up jRegs6, the J output bound (ValAt) and the budget.

Cost of each: 2 Cp + 2 C₀ Cc + Cc.

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 J6Seg.Ax
set_option maxHeartbeats 4000000
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function
variable {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp} {dA dF : Fin HS}
  {ρ : Fin 19 → Fin HS} {eF eB eUp eDn e pM : Fin Pp}
  {P : Prm} {ap : AxPlan6} {n : ℕ} {src : ℕ → ℕ} {D k : ℕ} {C₀ Cp Cc : ℝ}

Formal statement

theorem J6Seg.Ax.stepC (hMul : MulOK Isym tbl pM NLogN.KFUU.MS) (hK : tbl e = KR.chunkI2 pM)
    (hFine : FineBody6 Isym tbl eF eB dF C₀) (hC0 : 0 ≤ C₀) (hR : RegOK ρ KR.dT dF)
    (hρA : ∀ i, ρ i ≠ dA) (hA0 : dA ≠ 0) (hTA : KR.dT ≠ dA)
    (hS : SetupBody6 Isym tbl eUp eDn ρ dA (descAx6 P n src D k) (chunkRegs6 P n src D k ap.pl) Cp)
    (hReg : AxReg P n src D k) (hTab : TabAt P n src k) (hgC : ChunkOutAt P ap n src k)
    (hBud : AxBudgetAt P ap n src D k Cc) :
    PassOK Isym tbl (kpSt eUp eDn ρ KR.dT dF eF eB e) dA (descAx6 P n src D k)
      (fun L => L.length = axpre6 P n D k * axnc6 P n k * (2 ^ axfC6 P n * axpost6 P n D k) ∧
        GB (axwd6 P n src k ap) L ∧ ∀ b < axpre6 P n D k * axnc6 P n k, ∀ c < axpost6 P n D k,
          (lineAt (2 ^ axfC6 P n) (axpost6 P n D k) L b c).length = axl6 P n ∧
          KR.AB (axX6 P n src k ap) (lineAt (2 ^ axfC6 P n) (axpost6 P n D k) L b c))
      (gY6 P n src D k) (2 * Cp + (2 * C₀ * Cc + Cc)) := 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.Ax.stepC`, Solutions/J6SegAxis8.lean (lines 30–80) of the round-six development.

View graph