Round-six lemma `sp_sum`

Proved

IntMul.Kappa.R6.sp_sum

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_sum (s : IState HS) (f : Fin HS → List ℤ) (Cy Rc Rg Rm : Fin HS) (c g A Bb : ℕ)
    (lc lg lm : List ℤ) (hC5 : Cy.val < 56) (hc5 : Rc.val < 56) (hg5 : Rg.val < 56)
    (hm5 : Rm.val < 56) (h1 : Cy ≠ Rc) (h2 : Cy ≠ Rg) (h3 : Cy ≠ Rm) (h4 : Rc ≠ Rg)
    (h5 : Rc ≠ Rm) (h6 : Rg ≠ Rm) (hfC : f Cy = []) (hfc : f Rc = (c : ℤ) :: lc)
    (hfg : f Rg = (g : ℤ) :: lg) (hfm : f Rm = 0 :: lm) (hc : 2 ≤ c) (hg : g < c)
    (hA : 2 ≤ A) (hcA : c * c ≤ A) (hB : A ^ 6 < 2 ^ Bb) :
    Sp (sumR Cy Rc Rg Rm) (encK s f)
      (encK s (update f Rm ((∑ y ∈ Icc 1 c, sumT c g y) :: lm))) ((c * 22 + 1) * 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_sum (s : IState HS) (f : Fin HS → List ℤ) (Cy Rc Rg Rm : Fin HS) (c g A Bb : ℕ)
    (lc lg lm : List ℤ) (hC5 : Cy.val < 56) (hc5 : Rc.val < 56) (hg5 : Rg.val < 56)
    (hm5 : Rm.val < 56) (h1 : Cy ≠ Rc) (h2 : Cy ≠ Rg) (h3 : Cy ≠ Rm) (h4 : Rc ≠ Rg)
    (h5 : Rc ≠ Rm) (h6 : Rg ≠ Rm) (hfC : f Cy = []) (hfc : f Rc = (c : ℤ) :: lc)
    (hfg : f Rg = (g : ℤ) :: lg) (hfm : f Rm = 0 :: lm) (hc : 2 ≤ c) (hg : g < c)
    (hA : 2 ≤ A) (hcA : c * c ≤ A) (hB : A ^ 6 < 2 ^ Bb) :
    Sp (sumR Cy Rc Rg Rm) (encK s f)
      (encK s (update f Rm ((∑ y ∈ Icc 1 c, sumT c g y) :: lm))) ((c * 22 + 1) * 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_sum`, Solutions/R6SLib.lean (lines 215–314) of the round-six development.

View graph