sigma_two_five
plain-language theorem explainer
Sigma_2(5) equals 26 as the sum of squares of the divisors of 5. Number theorists verifying small instances of the sum-of-divisors function would cite this check. The proof applies the native_decide tactic to evaluate the arithmetic function definition directly.
Claim. $sigma_2(5) = 26$, where $sigma_k(n)$ is the sum of $d^k$ over all positive divisors $d$ of $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to the sum-of-divisors function. The local sigma abbreviation maps each natural number k to ArithmeticFunction.sigma k, providing the standard divisor-sum operator. An unrelated sigma definition in the AbileneParadox module tracks agent preference gaps, but the number theory version is the one invoked here.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to compute the value of sigma 2 applied to 5.
why it matters
This theorem supplies a concrete verification for the sigma definition inside the arithmetic functions module. It does not feed any downstream results and remains separate from the Recognition Science forcing chain T0-T8 or constants such as phi. The module context emphasizes Möbius footholds for later Dirichlet algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.