sigma_apply
The theorem establishes that the k-th divisor sum sigma_k(n) equals the sum of d^k over all positive divisors d of n. Number theorists working inside the Recognition Science arithmetic layer would cite it when evaluating sigma at arbitrary n during factorization or inversion arguments. The proof is a one-line simplification that delegates directly to Mathlib's ArithmeticFunction.sigma_apply.
claimFor natural numbers $k$ and $n$, $σ_k(n) = ∑_{d∣n} d^k$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic-function library, beginning with the Möbius function μ. The sigma function is the standard sum-of-powers-over-divisors arithmetic function. Upstream structures from J-cost minimization and spectral emergence employ analogous summation techniques in physical contexts, but the immediate setting remains the stabilization of basic divisor-sum interfaces before deeper Dirichlet algebra.
proof idea
The proof is a one-line wrapper that applies simp only to unfold the local sigma definition and invoke ArithmeticFunction.sigma_apply from Mathlib.
why it matters in Recognition Science
It supplies the evaluation rule required by the sibling theorems sigma_one and sigma_prime, which record the base cases σ_k(1) = 1 and σ_k(p) = 1 + p^k. This places the declaration inside the Möbius-footholds module whose stated goal is to stabilize elementary arithmetic-function interfaces before inversion results are layered on.
scope and limits
- Does not extend sigma to non-natural exponents k.
- Does not supply size estimates or asymptotic bounds on the sum.
- Does not encode multiplicative properties or Euler-product forms.
- Does not invoke or prove Möbius inversion.
Lean usage
simp [sigma_apply]formal statement (Lean)
178theorem sigma_apply {k n : ℕ} : sigma k n = ∑ d ∈ n.divisors, d ^ k := by
proof body
Term-mode proof.
179 simp only [sigma, ArithmeticFunction.sigma_apply]
180
181/-- σ_0(n) = number of divisors of n. -/