sigma_one_apply
plain-language theorem explainer
sigma_one_apply establishes that the sum-of-divisors function at exponent 1 equals the explicit sum over the positive divisors of n. Number theorists working with arithmetic functions on primes would cite it when reducing sigma_1 computations to direct divisor enumeration. The proof is a one-line wrapper that reduces the claim to the standard library definition via simplification.
Claim. For every natural number $n$, the sum-of-divisors function satisfies $sigma_1(n) = sum_{d | n} d$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to divisor sums. Sigma denotes the standard sum-of-powers divisor function, here specialized to exponent 1. The local setting keeps statements minimal to permit later layering of Dirichlet algebra and inversion formulas. Upstream, the definition of sigma draws on the multiplicative property of J-automorphisms from CostAlgebra, which preserves the relevant algebraic structure under multiplication.
proof idea
The proof is a one-line wrapper that applies simplification using the definition of sigma together with the standard sigma_one_apply lemma from the arithmetic functions library.
why it matters
This result supplies the base identity needed for the downstream theorem sigma_one_prime, which states sigma_1(p) = p + 1 for prime p. It fills a standard arithmetic-function step in the NumberTheory.Primes module, supporting divisor-based calculations that appear in Recognition Science mass formulas and phi-ladder constructions. No open scaffolding questions are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.