sigma_one_eight
plain-language theorem explainer
The sum-of-divisors function σ₁ evaluated at 8 equals 15. Number theorists verifying small arithmetic-function instances or building divisor-sum tables would cite this result. The proof is a one-line term that invokes native_decide to evaluate the divisor sum directly.
Claim. $σ_1(8) = 15$, where $σ_k(n)$ denotes the sum of the k-th powers of the positive divisors of n.
background
The ArithmeticFunctions module supplies lightweight wrappers around Mathlib's arithmetic-function library. The relevant sigma is the abbrev sigma (k : ℕ) : ArithmeticFunction ℕ := ArithmeticFunction.sigma k, documented as the sum-of-divisors function σ_k. The module's local setting focuses on Möbius footholds and keeps statements minimal pending deeper Dirichlet algebra. The unrelated sigma from AbileneParadox (agent preference gap) appears in the import graph but is not referenced in this declaration.
proof idea
The proof is a one-line term that applies native_decide to compute the value of the sum-of-divisors function at the concrete arguments k=1 and n=8.
why it matters
This supplies a verified concrete instance of σ₁(8) inside the NumberTheory.Primes.ArithmeticFunctions primitives. It supports downstream arithmetic calculations in the primes module even though no immediate used_by edges are recorded. The result stays within basic number-theoretic scaffolding and does not yet connect to Recognition Science landmarks such as the forcing chain T0-T8, the Recognition Composition Law, or the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.