sigma_zero_six
plain-language theorem explainer
The declaration verifies that the zero-order sum-of-divisors function at 6 equals 4, matching the count of positive divisors of 6. Researchers using arithmetic functions within the Recognition Science number theory module would cite this for basic checks. The proof relies on a native decision procedure that evaluates the expression directly.
Claim. The sum-of-divisors function satisfies $σ_0(6) = 4$.
background
This module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The sigma abbreviation is defined as sigma (k : ℕ) := ArithmeticFunction.sigma k, which yields the standard sum-of-divisors function σ_k(n) = ∑_{d|n} d^k. For k = 0 this reduces to the divisor counting function d(n). The module documentation states that statements remain lightweight pending deeper Dirichlet algebra.
proof idea
The proof is a one-line wrapper that applies native_decide to compute the value of sigma 0 6 directly.
why it matters
This basic verification supports the arithmetic functions infrastructure in the primes module. It fills a small step in the number theory foundations described in the module documentation, though no downstream uses are recorded. It relates to the Möbius footholds but does not yet connect to the forcing chain landmarks such as J-uniqueness or the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.