Round-six lemma `sp_cnt`

Proved

IntMul.Kappa.R6.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.R6SLib):

theorem IntMul.Kappa.R6.sp_cnt (s : IState HS) (f : Fin HS → List ℤ) (C rd R : Fin HS) (tst : Ex HS)
    (Pr : ℕ → Prop) [DecidablePred Pr] (N Bb : ℕ) (lR : List ℤ)
    (hC5 : C.val < 56) (hd5 : rd.val < 56) (hR5 : R.val < 56) (hCd : C ≠ rd) (hRd : R ≠ rd)
    (hRC : R ≠ C) (hfC : f C = []) (hfR : f R = (N : ℤ) :: lR) (hz : zsz ((N + 1 : ℕ) : ℤ) ≤ Bb)
    (htc : tst.Clean)
    (htst : ∀ x, 1 ≤ x → x ≤ N → ∀ acc : ℤ, 0 ≤ acc → acc ≤ N →
      tst.ok (encK s (update (update f rd (acc :: f rd)) C [(x : ℤ)])) ∧
      (tst.eval (encK s (update (update f rd (acc :: f rd)) C [(x : ℤ)])) < 0 ↔ Pr x) ∧
      tst.Bnd (encK s (update (update f rd (acc :: f rd)) C [(x : ℤ)])) Bb) :
    Sp (IntMul.Kappa.R6.cntR C rd R tst) (encK s f)
      (encK s (update f rd ((∑ x ∈ Icc 1 N, if Pr x then (1 : ℤ) else 0) :: f rd)))
      ((N * (tst.size + 7) + 3) * kU Bb)

Context. Round-six setup, part 2: register-program lemmas on managed states

All setup states are encK s f (KIL): the lists f j of integers pushed over the state s after the reads. A step is a Sp p s t c (ok, run, cost). Every cost is a multiple of the unit kU Bb = 10^7 (Bb+2)^2 for a uniform bit bound Bb.

sp_push, sp_asg, sp_pop: single steps.
sp_rep: a counted loop rep C (reg R) b through a family of managed states.
sp_cnt (cntR): #{x ∈ [1, N] : Pr x} by a test expression.
sp_sum (sumR): Σ_{y=1}^{c} y · [y g ≡ 1 (mod c)].

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_Defs69

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open IntMul IntMul.Kappa IntMul.Kappa.R6
open IntMul NLogN NLogN.KIL NLogN.KFM NLogN.RS Finset Function

Formal statement

theorem IntMul.Kappa.R6.sp_cnt (s : IState HS) (f : Fin HS → List ℤ) (C rd R : Fin HS) (tst : Ex HS)
    (Pr : ℕ → Prop) [DecidablePred Pr] (N Bb : ℕ) (lR : List ℤ)
    (hC5 : C.val < 56) (hd5 : rd.val < 56) (hR5 : R.val < 56) (hCd : C ≠ rd) (hRd : R ≠ rd)
    (hRC : R ≠ C) (hfC : f C = []) (hfR : f R = (N : ℤ) :: lR) (hz : zsz ((N + 1 : ℕ) : ℤ) ≤ Bb)
    (htc : tst.Clean)
    (htst : ∀ x, 1 ≤ x → x ≤ N → ∀ acc : ℤ, 0 ≤ acc → acc ≤ N →
      tst.ok (encK s (update (update f rd (acc :: f rd)) C [(x : ℤ)])) ∧
      (tst.eval (encK s (update (update f rd (acc :: f rd)) C [(x : ℤ)])) < 0 ↔ Pr x) ∧
      tst.Bnd (encK s (update (update f rd (acc :: f rd)) C [(x : ℤ)])) Bb) :
    Sp (IntMul.Kappa.R6.cntR C rd R tst) (encK s f)
      (encK s (update f rd ((∑ x ∈ Icc 1 N, if Pr x then (1 : ℤ) else 0) :: f rd)))
      ((N * (tst.size + 7) + 3) * kU Bb) := 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 `IntMul.Kappa.R6.sp_cnt`, Solutions/R6SLib.lean (lines 111–186) of the round-six development.

View graph