sigma_one_two_pow_two
plain-language theorem explainer
The sum-of-divisors function sigma_1 evaluated at 4 equals 7. Number theorists verifying small instances of arithmetic functions cite this for implementation checks. The proof executes via native_decide for direct evaluation of the divisor sum.
Claim. Let $sigma_k(n)$ be the sum of the $k$th powers of the positive divisors of $n$. Then $sigma_1(4) = 7$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function mu. The relevant sigma is the local abbreviation sigma(k) := ArithmeticFunction.sigma k, which returns the sum-of-divisors function for exponent k. This sits inside the NumberTheory.Primes setup that prepares basic interfaces before Dirichlet algebra or inversion layers are added.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to compute the arithmetic function value directly.
why it matters
This supplies a concrete verification instance for the sum-of-divisors function inside the arithmetic functions module. No downstream theorems reference it in the current graph, so it functions as a standalone check rather than advancing Möbius properties or larger prime-number results. It does not touch the Recognition Science forcing chain, RCL, or phi-ladder constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.