Round-six lemma `jcost_ax`

Proved

J6Seg.Side.jcost_ax

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

theorem J6Seg.Side.jcost_ax (u B : ℕ) :
    dP6 P n * kerC (JK.jC (axkJ6 P n src k ap) (axw6 P n) (axG6 P n src k)
        (JK.jFs (axQ6 P n src k) (axR6 P n) (axs6 src k) (axt6 P n k) (axl6 P n) (axw6 P n)
          (axα6 P n))
        (JK.jBs (axQ6 P n src k) (axR6 P n) (axs6 src k) (axt6 P n k) (axl6 P n) (axw6 P n)
          (axα6 P n))
        (JK.jCc (axQ6 P n src k) (axR6 P n) (axs6 src k) (axt6 P n k) (axl6 P n) (axw6 P n)
          (axα6 P n) (axw6 P n)) u + 2)
      B (2 ^ axfJ6 P n src k) (axpost6 P n D k) (axTJ6 P n src k ap).length 1
      (tabsT (fun _ => axTJ6 P n src k ap) 1).length (axpre6 P n D k)
      (2 * (axpre6 P n D k * 1 * axpost6 P n D k * 2 ^ axfJ6 P n src k)) ≤
    TP6 P n * (400000 * (axw6 P n + 1) * u + 40000000000 * (B + 2) * (axw6 P n + 1))

Context. J cost 4: the J pass as a natural-number polynomial

kerC_le1: kerC Ckn B m post Lj 1 Tot pre N ≤ pre·post·Ckn + 10^5 (B+2)(pre·post·(m+1) + pre (Lj + Tot + 2) + N + 2);
jcost_arith: the generic arithmetic;
jcost_ax: on an axis, for every u and B, d · kerC (jC … u + 2) B (2^fJ) post |TJ6| 1 |TJ| pre NJ ≤ T (4·10^5 (w+1) u + 4·10^10 (B+2)(w+1));
jBody_ax: |jBody| ≤ 1460 w m + 24 m + G + 3w + 13.

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_Defs70

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.Side
open Finset
open IntMul NLogN IntMul.Kappa.R6 J6Seg
variable {P : Prm} {n : ℕ} {src : ℕ → ℕ} {D k : ℕ} (ap : AxPlan6) (h : AxJ P n src D k)
include h

Formal statement

theorem J6Seg.Side.jcost_ax (u B : ℕ) :
    dP6 P n * kerC (JK.jC (axkJ6 P n src k ap) (axw6 P n) (axG6 P n src k)
        (JK.jFs (axQ6 P n src k) (axR6 P n) (axs6 src k) (axt6 P n k) (axl6 P n) (axw6 P n)
          (axα6 P n))
        (JK.jBs (axQ6 P n src k) (axR6 P n) (axs6 src k) (axt6 P n k) (axl6 P n) (axw6 P n)
          (axα6 P n))
        (JK.jCc (axQ6 P n src k) (axR6 P n) (axs6 src k) (axt6 P n k) (axl6 P n) (axw6 P n)
          (axα6 P n) (axw6 P n)) u + 2)
      B (2 ^ axfJ6 P n src k) (axpost6 P n D k) (axTJ6 P n src k ap).length 1
      (tabsT (fun _ => axTJ6 P n src k ap) 1).length (axpre6 P n D k)
      (2 * (axpre6 P n D k * 1 * axpost6 P n D k * 2 ^ axfJ6 P n src k)) ≤
    TP6 P n * (400000 * (axw6 P n + 1) * u + 40000000000 * (B + 2) * (axw6 P n + 1)) := 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.Side.jcost_ax`, Solutions/J6SegJCost4.lean (lines 131–267) of the round-six development.

View graph