sigma_one_twelve
plain-language theorem explainer
The sum-of-divisors function evaluates σ_1(12) to 28. Number theorists verifying small cases of divisor sums would cite this result. The proof is a direct native computation that confirms the arithmetic sum of the divisors of 12.
Claim. $σ_1(12) = 28$, where $σ_k(n)$ denotes the sum of the $k$-th powers of the positive divisors of $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The relevant definition here is the abbreviation sigma(k : ℕ) that maps to ArithmeticFunction.sigma k, the standard sum-of-divisors operator. An unrelated sigma appears in the AbileneParadox module as an agent charge measuring the gap between private preference and public vote, but the present theorem operates entirely within the arithmetic setting.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the divisor sum directly.
why it matters
This supplies a concrete numerical check inside the arithmetic-functions module that supports Möbius footholds for later Dirichlet algebra. It fills a basic verification step in the NumberTheory.Primes.ArithmeticFunctions section of the Recognition framework. No downstream uses are recorded, so its integration into larger prime or inversion arguments remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.