sigma_zero_ten
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not establish a general closed form for σ_0(n).
- Does not relate to the σ-charge defined for agents in the Abilene paradox module.
- Does not invoke squarefreeness or the Möbius function.
formal statement (Lean)
983theorem sigma_zero_ten : sigma 0 10 = 4 := by native_decide
proof body
Term-mode proof.
984
985/-- σ_1(10) = 18 (sum: 1 + 2 + 5 + 10 = 18). -/