The eight non-kernel terms of one `A` axis (round six, `aSide_at`)

Proved

J6Seg.AC.aSide_at

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

complexity-theoryinteger-multiplicationkappa-improvement

The eight non-kernel terms of one A axis.

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

theorem J6Seg.AC.aSide_at (P : Prm) {n : ℕ} {src : ℕ → ℕ} {D k : ℕ} (h : AxANum P n src D k)
    (hD : dP6 P n = D + 1) :
    let p := pP6 P n; let s := src k; let t := tF6 P n k; let α := αN6 P n; let H := HA6 P n
    let pk := pkA6 8 16 p; let w := p + 2
    let f := Nat.log 2 (IntMul.HvdH.sWidth p α) + 3
    let pre := preT P n D k; let post := postT P n D k; let M := t / (16 * H)
    let K := KAs P * (cU6 P n 2 / (D + 1))
    cFine w 5 1 (pre * (t * post)) ≤ K ∧ cFine w 5 pre (t * post) ≤ K ∧
    cFine w 3 pre (M * (8 * H) * post) ≤ K ∧ cFine w 3 (pre * M) (8 * H * post) ≤ K ∧
    cFine w f (pre * (M * 8)) post ≤ K ∧ cFine (pk + 1) f (pre * (M * 8)) post ≤ K ∧
    (cSlabA (32 * t) (8 * (M * (8 * H))) post pre w
      (J6A.srcG s t H (J6A.WA p α H) M (8 * H)) : ℝ) ≤ K ∧
    (cSlabA (M * 8 * (8 * H)) t post pre (pk + 1) (J6A.srcC H (8 * H)) : ℝ) ≤ K

Context. A-axis costs 2: the eight non-kernel cost terms of an A axis

aSide_at: on an axis with AxANum, the six fine exposures and the two slab passes of axACost are each ≤ KAs P · cU6 P n 2 / (D + 1), KAs P = 10^12 (x+8)².

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.AC
open IntMul NLogN IntMul.Kappa.R6 J6Seg J6Seg.Side J6Seg.Ax

Formal statement

theorem J6Seg.AC.aSide_at (P : Prm) {n : ℕ} {src : ℕ → ℕ} {D k : ℕ} (h : AxANum P n src D k)
    (hD : dP6 P n = D + 1) :
    let p := pP6 P n; let s := src k; let t := tF6 P n k; let α := αN6 P n; let H := HA6 P n
    let pk := pkA6 8 16 p; let w := p + 2
    let f := Nat.log 2 (IntMul.HvdH.sWidth p α) + 3
    let pre := preT P n D k; let post := postT P n D k; let M := t / (16 * H)
    let K := KAs P * (cU6 P n 2 / (D + 1))
    cFine w 5 1 (pre * (t * post)) ≤ K ∧ cFine w 5 pre (t * post) ≤ K ∧
    cFine w 3 pre (M * (8 * H) * post) ≤ K ∧ cFine w 3 (pre * M) (8 * H * post) ≤ K ∧
    cFine w f (pre * (M * 8)) post ≤ K ∧ cFine (pk + 1) f (pre * (M * 8)) post ≤ K ∧
    (cSlabA (32 * t) (8 * (M * (8 * H))) post pre w
      (J6A.srcG s t H (J6A.WA p α H) M (8 * H)) : ℝ) ≤ K ∧
    (cSlabA (M * 8 * (8 * H)) t post pre (pk + 1) (J6A.srcC H (8 * H)) : ℝ) ≤ K := 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.AC.aSide_at`, Solutions/J6SegAKCost2.lean (lines 59–138) of the round-six development.

View graph