sigma_zero_twohundredten
plain-language theorem explainer
The declaration establishes that the divisor counting function sigma 0 applied to 210 equals 16. Number theorists or Recognition Science modelers checking arithmetic properties of small integers would cite this result for verification purposes. The proof is a one-line native_decide invocation that computes the value directly from the definition of sigma.
Claim. $σ_0(210) = 16$, where $σ_0(n)$ denotes the number of positive divisors of the integer $n$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. The sigma function is the standard divisor-sum function σ_k(n), so that sigma 0 n returns the divisor count d(n). Upstream structures include J-cost minimization (strictly convex with unique minimum at x=1) and spectral emergence (forcing SU(3)×SU(2)×U(1) gauge content and exactly three generations).
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate sigma 0 210 directly.
why it matters
This supplies a verified arithmetic fact inside the module's Möbius footholds, supporting Dirichlet inversion and related number-theoretic infrastructure. It aligns with Recognition Science's discrete phi-ladder and eight-tick octave by providing an exact divisor count for the composite 210 = 2·3·5·7. No downstream uses are recorded, so it functions as a basic computational checkpoint rather than a parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.