sigma_two_two
plain-language theorem explainer
The declaration verifies that the sum-of-divisors function sigma_2 at argument 2 equals 5. Number theorists working with arithmetic functions would cite this as a direct evaluation of the definition. The proof is a one-line term that applies native_decide to compute the sum 1^2 + 2^2.
Claim. $σ_2(2) = 5$, where $σ_k(n)$ is the sum of the $k$-th powers of all positive divisors of $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. The sigma abbreviation is defined as ArithmeticFunction.sigma k, the standard sum-of-divisors function. This sits inside the primes arithmetic-functions file whose module documentation emphasizes basic interfaces before deeper Dirichlet algebra.
proof idea
The proof is a one-line term wrapper that invokes native_decide on the sigma definition to evaluate the concrete case directly.
why it matters
This supplies a concrete numerical check for the sigma function inside the arithmetic-functions module. It supports downstream number-theoretic constructions in the Recognition Science framework by confirming the basic sum-of-divisors behavior at small arguments. No parent theorems are listed among the used-by edges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.