sigma_def
The theorem supplies a simplification rule identifying the module-local sum-of-divisors function sigma k with Mathlib's standard ArithmeticFunction.sigma k. Number theorists extending prime-arithmetic results in Lean would cite it to inherit library lemmas without name clashes. The proof is a one-line reflexivity that holds because sigma is introduced as an abbreviation aliasing the library definition.
claimFor each natural number $k$, the arithmetic function denoted sigma $k$ coincides exactly with the standard sum-of-divisors function sigma $k$ from the arithmetic-functions library.
background
The module supplies lightweight wrappers around Mathlib's arithmetic-function library, beginning with the Möbius function and extending to the sum-of-divisors function. The local sigma is introduced by the sibling abbreviation sigma (k : ℕ) : ArithmeticFunction ℕ := ArithmeticFunction.sigma k, so that sigma k stands for the function n ↦ ∑_{d∣n} d^k. The upstream AbileneParadox.sigma definition (a real-valued charge measuring private-public preference mismatch) is unrelated and appears only as a name collision in the import graph.
proof idea
The proof is a one-line wrapper that applies reflexivity. Because the left-hand side is literally defined to be the right-hand side, rfl closes the goal immediately.
why it matters in Recognition Science
The declaration installs a simp lemma that lets downstream proofs invoke standard properties of the sum-of-divisors function without qualification. It occupies the arithmetic-functions layer that supports later prime-counting and divisor-sum arguments inside the NumberTheory.Primes hierarchy. No used-by edges are recorded yet, leaving open whether it will be invoked in explicit mass-ladder or phi-ladder calculations.
scope and limits
- Does not prove any multiplicative or additive identities for sigma.
- Does not compute explicit values or closed forms for particular k.
- Does not invoke or derive Möbius inversion formulas.
- Does not relate the sum-of-divisors function to the Recognition Science phi-ladder or mass formula.
formal statement (Lean)
175@[simp] theorem sigma_def (k : ℕ) : sigma k = ArithmeticFunction.sigma k := rfl
proof body
Term-mode proof.
176
177/-- σ_k(n) = ∑ d ∣ n, d^k. -/