sigma_one_five_pow_one
plain-language theorem explainer
The sum-of-divisors function evaluates to 6 at the integer 5. Number theorists constructing tables of arithmetic functions inside the Recognition framework would cite this as a verified base case for later multiplicative arguments. The proof is a one-line native decision that directly computes the divisor sum without intermediate lemmas.
Claim. $σ_1(5) = 6$, where $σ_1(n)$ is the sum of the positive divisors of $n$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic-function library, beginning with the Möbius function and extending to maps such as the divisor sum. Sigma denotes the standard sum-of-divisors function. The local setting keeps statements minimal so that deeper Dirichlet algebra can be added once the basic interfaces stabilize, as stated in the module documentation.
proof idea
The proof is a one-line term that invokes native_decide to evaluate the arithmetic expression directly.
why it matters
This supplies a concrete verified instance for the sigma function inside the primes arithmetic module. It supports later development of multiplicative properties and Dirichlet series within the Recognition framework, though no downstream uses are recorded yet. It aligns with the lightweight interface goal stated in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.