sigma_zero_eighthundredforty
plain-language theorem explainer
The sum-of-divisors function evaluates to 32 at k=0 for the integer 840. Number theorists using the Recognition Science arithmetic-functions layer would cite this for verified divisor counts on 840. The proof is a one-line native_decide wrapper that reduces the expression directly from the Mathlib definition of sigma.
Claim. $σ_0(840) = 32$, where $σ_k(n)$ is the sum of the $k$th powers of the positive divisors of $n$.
background
The module supplies thin wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to the sum-of-divisors function. Here sigma is the abbreviation sigma (k : ℕ) := ArithmeticFunction.sigma k, so sigma 0 840 computes the number of positive divisors of 840. An upstream sibling result establishes ω(840) = 4 with prime factors 2, 3, 5, 7; the module doc notes these statements remain lightweight until deeper Dirichlet algebra is added.
proof idea
One-line wrapper that applies native_decide to evaluate sigma 0 840 by direct computation from the definition.
why it matters
The declaration supplies a concrete numerical anchor inside the arithmetic-functions module of NumberTheory.Primes. It supports later identities that may feed Recognition Science mass formulas or phi-ladder rung calculations, though no downstream theorems currently cite it. The value 32 is consistent with the divisor count for a number whose radical is 210 and whose prime factorization is 2^3 · 3 · 5 · 7.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.