sigma_two_one
plain-language theorem explainer
The sum-of-divisors function σ₂ applied to 1 equals 1. Number theorists building arithmetic function identities or verifying small cases for multiplicative properties would cite this base result. The proof is a one-line wrapper that invokes native_decide to compute the value directly from the definition.
Claim. $σ_2(1) = 1$, where $σ_k(n)$ is the sum of the $k$-th powers of all positive divisors of $n$.
background
The module supplies thin wrappers around Mathlib arithmetic functions, starting from the Möbius function μ and extending to the sum-of-divisors function. The local sigma abbreviation is defined as sigma (k : ℕ) := ArithmeticFunction.sigma k, so sigma 2 denotes σ₂. The surrounding context is preparation for Dirichlet convolution and inversion once the basic interfaces stabilize. The upstream sigma from AbileneParadox is a separate real-valued charge on agent reports and is not used here.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate sigma 2 1 by direct computation of the divisor sum.
why it matters
This supplies the trivial base case σ₂(1) = 1 inside the arithmetic-functions layer of the primes module. It supports later constructions that rely on the divisor function at small arguments, such as explicit checks before invoking Möbius inversion or square-free properties. No downstream theorems currently cite it, and it touches none of the T0–T8 forcing chain or Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.