sigma_apply
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.