sigma_two_twelve
plain-language theorem explainer
The sum-of-divisors function σ₂ applied to 12 equals 210. Number theorists verifying small instances of arithmetic functions would cite this for quick checks. The proof proceeds by direct native computation of the divisor sum.
Claim. $σ_2(12) = 210$
background
This module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function. The sigma abbrev defines the sum-of-divisors function σ_k as the map sending k to ArithmeticFunction.sigma k, which sums the k-th powers of all positive divisors of its argument. The local setting keeps statements lightweight to stabilize basic interfaces before layering Dirichlet algebra and inversion.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate sigma 2 12 by direct computation.
why it matters
This supplies a verified numerical fact inside the arithmetic functions module. It supports the module's aim of providing stable footholds for later inversion work. It does not engage the Recognition Science forcing chain, the phi fixed point, or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.