sigma_zero_apply
plain-language theorem explainer
sigma_zero_apply establishes that the zero-order divisor sum equals the cardinality of the divisor set for any natural number n. Number theorists citing Recognition Science arithmetic functions would use this when reducing divisor counts for primes. The proof proceeds by direct simplification using the definition of sigma.
Claim. For any natural number $n$, the arithmetic function satisfies $σ_0(n)$ equals the number of positive divisors of $n$.
background
This module supplies lightweight wrappers for arithmetic functions from Mathlib, beginning with the Möbius function and extending to divisor sums. The sigma function is the standard sum-of-divisors arithmetic function, with $σ_k(n)$ the sum of $k$-th powers of divisors, so that $σ_0(n)$ reduces to the divisor counting function $d(n)$. The local setting is to provide footholds for Dirichlet algebra and inversion in the Recognition framework. Upstream structures include the J-cost minimization from PhysicsComplexityStructure, which underpins the convex optimization used in forcing chains, and the spectral emergence structure forcing SU(3) × SU(2) × U(1) gauge content together with three particle generations.
proof idea
The proof is a one-line wrapper that invokes the definition of the sigma arithmetic function together with the standard Mathlib fact on sigma zero apply.
why it matters
This result serves as the base case for theorems on the divisor count of primes and prime powers, such as sigma_zero_prime which states $σ_0(p) = 2$ and sigma_zero_prime_pow which states $σ_0(p^k) = k + 1$. It supports the number-theoretic machinery needed for mass formulas on the phi-ladder in Recognition Science. It connects to the eight-tick octave and D = 3 dimensions through the broader framework, though no direct link is made here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.