sigma_zero_thirty
plain-language theorem explainer
The sum-of-divisors function evaluated at exponent zero for argument 30 returns exactly 8, matching the divisor count of 30. Number theorists verifying arithmetic function implementations or using divisor counts as base cases would reference this result. The proof reduces to a single native_decide invocation that computes the value directly from the definition.
Claim. $σ_0(30) = 8$, where $σ_k(n)$ is the sum of the $k$-th powers of all positive divisors of $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, with emphasis on the Möbius function as a starting point for Dirichlet algebra. The local sigma abbreviation defines the standard sum-of-divisors function $σ_k$ via ArithmeticFunction.sigma. This supplies a concrete numerical instance for $k=0$.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate sigma 0 30 from its definition as the divisor count.
why it matters
This supplies an explicit numerical anchor for the divisor function inside the arithmetic functions module that supports Möbius footholds and prime calculations. No downstream theorems are recorded yet, so the result functions as a verified base fact rather than a lemma feeding a larger chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.