Prove2Me

Round-six lemma `sum_mu`

Proved
NLogN.KFM.sum_mu

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

theorem NLogN.KFM.sum_mu (P s : ℕ) (hs : 2 ≤ s) (hc : Nat.Coprime P s) :
    ∑ y ∈ Finset.Icc 1 s, (y : ℤ) * (if ((y : ℤ) * ((P % s : ℕ) : ℤ)) % (s : ℤ) = 1 then 1 else 0) =
      (muInv P s : ℤ)

Context. KFM S6: the sources and their inverses (math side)

  • srcN n i = s_i, prodN n i = ∏_{j<i} s_j, muN n i = μ_i = (prodN n i)^{-1} mod s_i.
  • indZ_eq: for 0 ≤ m < s, (s − ((m + s − 1) mod s)) / s = [m = 1]. This is the indicator the IL sum uses (only nmod/ndiv).
  • sum_mu: Σ_{y=1}^{s} y·[y·(P mod s) mod s = 1] = muInv P s for coprime P, s, s ≥ 2.
  • prod_mod_seq: the running product c ↦ (c·s_{i−1−k}) mod s_i ends at prodN n i mod s_i.

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_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_MultitapeModel
import Definitions.Def_IntMul_HvdH_Numeric
import Definitions.Def_IntMul_HvdH_ExpApprox
import Definitions.Def_IntMul_HvdH_RealExp
import Definitions.Def_IntMul_HvdH_Twiddle

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open NLogN NLogN.KFM
open IntMul IntMul.OpenAI.Glue IntMul.OpenAI.RP
Formal statement
theorem NLogN.KFM.sum_mu (P s : ℕ) (hs : 2 ≤ s) (hc : Nat.Coprime P s) :
    ∑ y ∈ Finset.Icc 1 s, (y : ℤ) * (if ((y : ℤ) * ((P % s : ℕ) : ℤ)) % (s : ℤ) = 1 then 1 else 0) =
      (muInv P s : ℤ) := 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 `NLogN.KFM.sum_mu`, Solutions/KFMS6.lean (lines 48–88) of the round-six development.

View graph