sigma_zero_prime_pow
plain-language theorem explainer
The declaration proves that the divisor-counting function σ_0 applied to a prime power p^k equals k+1. Number theorists working with arithmetic functions would cite this when evaluating divisor counts on prime powers. The short proof reduces the statement by converting the Prime predicate, applying the sigma-zero cardinality identity, rewriting the explicit divisor set of p^k, and simplifying the resulting cardinality.
Claim. For a prime number $p$ and natural number $k$, let $σ_0(n)$ denote the number of positive divisors of $n$. Then $σ_0(p^k) = k + 1$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to the sum-of-divisors family. Here sigma k abbreviates ArithmeticFunction.sigma k, while sigma_zero_apply states that σ_0(n) equals the cardinality of the divisors of n. Upstream, divisors_prime_pow records that the divisors of p^k are exactly the set {p^0, p^1, ..., p^k}. The local setting keeps statements minimal so that deeper Dirichlet algebra can be added once the basic interfaces stabilize.
proof idea
The proof first converts the local Prime predicate to Nat.Prime via the equivalence prime_iff. It applies sigma_zero_apply to replace σ_0(p^k) with the cardinality of the divisors. A rewrite then substitutes the explicit form given by divisors_prime_pow. Simplification yields the integer k+1.
why it matters
This identity supplies the concrete evaluation of σ_0 on prime powers inside the arithmetic-functions layer. It supports the number-theory scaffolding that Recognition Science uses for discrete structures such as the phi-ladder and mass formulas. No downstream uses are recorded, yet the result aligns with the framework's requirement for exact divisor counts when handling prime-power contributions to the eight-tick octave and spatial dimension D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.