sigma_one_two_pow_three
plain-language theorem explainer
The sum-of-divisors function σ_1 applied to 8 equals 15. Number theorists checking concrete values of divisor sums in prime-power cases would reference this evaluation. The proof is a direct computational check via native decision procedure on the arithmetic expression.
Claim. $σ_1(8) = 15$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and extending to related tools such as the sum-of-divisors function. Here sigma denotes the abbrev sigma (k : ℕ) := ArithmeticFunction.sigma k, so that sigma 1 n computes the ordinary sum of divisors of n. The local setting is basic number-theoretic infrastructure for later Dirichlet algebra and inversion steps.
proof idea
One-line wrapper that applies native_decide to evaluate sigma 1 (2 ^ 3) directly.
why it matters
This supplies a concrete numerical check for the sum-of-divisors wrapper inside the arithmetic-functions module. No downstream theorems are listed, so it functions as a basic verification point rather than a link in a larger chain. It does not touch the Recognition forcing chain, RCL, or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.