The kernel pass of one `A` axis (round six, `kerA_le`)

Proved

J6Seg.AC.kerA_le

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

complexity-theoryinteger-multiplicationkappa-improvement

The kernel pass of one A axis.

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

theorem J6Seg.AC.kerA_le {p H WA pre nc post T G f : ℕ} (hp : 64 ≤ p) (hH : 1 ≤ H) (hHp : H ≤ p)
    (hWw : 2 * WA ≤ 8 * H) (hf : 2 ^ f = 8 * H) (hpre : 1 ≤ pre) (hnc : 1 ≤ nc)
    (hpost : 1 ≤ post) (hR : pre * nc * post * (2 * H) = T) (hG : p < 2 ^ G) (hG8 : 8 ≤ G) :
    kerC (cAK2 (2 * WA) (2 * H) (8 * H) (8 * p + 16) (17 * p + 40) (mulSup (2 * (20 * p + 60)))
        (mulSup (2 * ((17 * p + 40) * (2 * (2 * WA + 2 * H)) + 2))) (20 * p + 60) (17 * p + 40 + 2)
        + 2) (17 * p + 40 + 2) (2 ^ f) post (17 + 2 * WA + (2 * WA + 2 * H) + 2 * H) nc
      (nc * (17 + 2 * WA + (2 * WA + 2 * H) + 2 * H + 1)) pre (2 * (pre * nc * post * 2 ^ f)) ≤
      10 ^ 16 * CfA * (T * p * G ^ 2)

Context. A-axis costs 5: the kernel pass of one A axis

fmB_nat: fmB m ≤ CfA (m+1) · 5 (E+2)² when m + 1 < 2^E;
kerA_le: with p ≥ 64, 1 ≤ H ≤ p, 2W ≤ 8H, 2^f = 8H, pre · nc · post · 2H = T and p < 2^G, G ≥ 8, the kernel pass of axA_pass (kernel v2, the parameters of akCond_at) costs at most 10^16 · CfA · T p G².

Per row: cAK2 + 2 ≤ 6·10^15 · CfA · H p G² (cAK2_le), and pre · nc · post · H ≤ T.

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.KR J6Seg.KR.AK J6Seg.Ax

Formal statement

theorem J6Seg.AC.kerA_le {p H WA pre nc post T G f : ℕ} (hp : 64 ≤ p) (hH : 1 ≤ H) (hHp : H ≤ p)
    (hWw : 2 * WA ≤ 8 * H) (hf : 2 ^ f = 8 * H) (hpre : 1 ≤ pre) (hnc : 1 ≤ nc)
    (hpost : 1 ≤ post) (hR : pre * nc * post * (2 * H) = T) (hG : p < 2 ^ G) (hG8 : 8 ≤ G) :
    kerC (cAK2 (2 * WA) (2 * H) (8 * H) (8 * p + 16) (17 * p + 40) (mulSup (2 * (20 * p + 60)))
        (mulSup (2 * ((17 * p + 40) * (2 * (2 * WA + 2 * H)) + 2))) (20 * p + 60) (17 * p + 40 + 2)
        + 2) (17 * p + 40 + 2) (2 ^ f) post (17 + 2 * WA + (2 * WA + 2 * H) + 2 * H) nc
      (nc * (17 + 2 * WA + (2 * WA + 2 * H) + 2 * H + 1)) pre (2 * (pre * nc * post * 2 ^ f)) ≤
      10 ^ 16 * CfA * (T * p * G ^ 2) := 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.kerA_le`, Solutions/J6SegAKCost5.lean (lines 54–196) of the round-six development.

View graph