sigma_one_three_pow_two
plain-language theorem explainer
The sum-of-divisors function σ₁ evaluated at 9 equals 13. Number theorists checking basic arithmetic function values would cite this as a verification instance. The proof is a one-line native decision procedure that computes the divisor sum directly.
Claim. $σ_1(9) = 13$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and extending to the sum-of-divisors σ_k. Here sigma is the abbreviation sigma (k : ℕ) := ArithmeticFunction.sigma k, so sigma 1 denotes the standard divisor-sum function σ₁. The upstream AbileneParadox sigma is a separate decision-theoretic charge and does not apply.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic to evaluate the equality by direct computation of the divisors of 9.
why it matters
This supplies a concrete numerical check for σ₁ inside the arithmetic-functions module. It has no recorded downstream uses and does not feed any parent theorem in the Recognition framework. It remains a basic verification step unrelated to the forcing chain, RCL, or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.