sigma_zero_ten
plain-language theorem explainer
The order-zero divisor function evaluates to 4 at 10, matching the explicit list of positive divisors 1, 2, 5 and 10. Number theorists checking small instances of arithmetic functions would cite the equality as a verified base case. The proof reduces to a single native_decide call that computes the value without manual expansion of the divisor set.
Claim. The order-zero sum-of-divisors function satisfies $σ_0(10) = 4$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to the sum-of-divisors function σ_k. The local sigma abbreviation is defined as ArithmeticFunction.sigma k, which returns the sum of the k-th powers of the divisors of its argument. The upstream sigma declaration in Decision.AbileneParadox defines an unrelated σ-charge measuring the gap between private preference and public vote for an agent.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the concrete equality.
why it matters
This supplies a concrete base case inside the arithmetic-functions section of the primes module. It supports later development of Dirichlet algebra and inversion once the basic interfaces stabilize, without feeding any downstream theorems in the current dependency graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.