Round-six lemma `sp_cnt`

Proved

J6Seg.AxC.sp_cnt

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

theorem J6Seg.AxC.sp_cnt {dA : Fin HS} (hA : DAok dA) (s : IState HS) (f : Fin HS → List ℤ)
    (x1 x2 x3 x4 x5 : ℤ) (r : List ℤ) (hd : f dA = x1 :: x2 :: x3 :: x4 :: x5 :: r)
    (hu : f cU = []) (h1 : f cA1 = []) (h2 : f cA2 = []) (h3 : f cA3 = []) (hn : f cN = [])
    (B : ℕ) (b1 : zsz x1 ≤ B) (b2 : zsz x2 ≤ B) (b3 : zsz x3 ≤ B) (b4 : zsz x4 ≤ B)
    (b5 : zsz x5 ≤ B) (bm1 : zsz (x5 * x3) ≤ B) (bm2 : zsz (x2 * (x5 * x3)) ≤ B)
    (bm : zsz (2 * (x2 * (x5 * x3))) ≤ B) (hB2 : 2 ≤ B) :
    Sp (cntRS dA) (encK s f) (encK s (update f cN [2 * (x2 * (x5 * x3))])) (cCnt B)

Context. The axis program: the copy 0 → rZ (after pass 2) and the swap 0 ↔ rZ (before pass 7)

Both read the count 2·pre·t·post (the number of integers of an axis array) off the axis descriptor descAx6 = [k, pre, post, s, t, …] on dA (restored), on the scratch stacks 1 … 7.

cntRS dA: pushes 2·(pre·(t·post)) on CN = 5 (sp_cnt);
copyAx dA: gflat L ++ l on 0 and l₂ on rZ ↦ gflat L ++ l₂ on rZ, stack 0 unchanged (copyAx_runs);
swapAx dA: gflat A ++ l on 0, gflat B ++ l₂ on rZ ↦ gflat B ++ l on 0, gflat A ++ l₂ on rZ (swapAx_runs).

Convention (FineBody6): every stack other than 0, dA, rZ empty; dA ∉ {0, …, 7, 53}, dA < 56.

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.AxC
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function
open J6Seg.Slab (rZ)

Formal statement

theorem J6Seg.AxC.sp_cnt {dA : Fin HS} (hA : DAok dA) (s : IState HS) (f : Fin HS → List ℤ)
    (x1 x2 x3 x4 x5 : ℤ) (r : List ℤ) (hd : f dA = x1 :: x2 :: x3 :: x4 :: x5 :: r)
    (hu : f cU = []) (h1 : f cA1 = []) (h2 : f cA2 = []) (h3 : f cA3 = []) (hn : f cN = [])
    (B : ℕ) (b1 : zsz x1 ≤ B) (b2 : zsz x2 ≤ B) (b3 : zsz x3 ≤ B) (b4 : zsz x4 ≤ B)
    (b5 : zsz x5 ≤ B) (bm1 : zsz (x5 * x3) ≤ B) (bm2 : zsz (x2 * (x5 * x3)) ≤ B)
    (bm : zsz (2 * (x2 * (x5 * x3))) ≤ B) (hB2 : 2 ≤ B) :
    Sp (cntRS dA) (encK s f) (encK s (update f cN [2 * (x2 * (x5 * x3))])) (cCnt 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.AxC.sp_cnt`, Solutions/J6SegAxCopy.lean (lines 125–223) of the round-six development.

View graph