sigma_one_two_pow_one
plain-language theorem explainer
The declaration evaluates the sum-of-divisors function σ_1 at the prime power 2^1 and obtains the integer 3. Number theorists checking small cases or preparing Möbius inversion steps would reference this concrete instance. The proof proceeds by native_decide, which reduces the arithmetic expression directly to a decidable equality.
Claim. $σ_1(2) = 3$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and extending to the sum-of-divisors function σ_k. The local sigma is defined as the standard sum-of-divisors arithmetic function σ_k(n) = ∑_{d|n} d^k. An upstream definition in AbileneParadox uses the same name for a decision-theoretic charge (private versus public report gap), but the module-local abbrev overrides it for number-theoretic use. The doc-comment identifies the purpose as supplying concrete sigma values at small prime powers.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the sum-of-divisors expression for the argument 2 directly from the definition of sigma.
why it matters
The result supplies a base case for the arithmetic-functions layer inside NumberTheory.Primes, supporting later Dirichlet algebra and inversion work outlined in the module doc. No downstream theorems are recorded, so it functions as a verified constant rather than a lemma feeding a larger chain. It aligns with the framework's emphasis on explicit small-integer checks before scaling to prime-power ladders or recognition composition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.