sigma_zero_prime_pow
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not extend the equality to composite bases.
- Does not compute σ_k for any k greater than zero.
- Does not address multiplicative or Dirichlet-convolution properties.
- Does not supply asymptotic estimates or bounds.
formal statement (Lean)
515theorem sigma_zero_prime_pow {p k : ℕ} (hp : Prime p) : sigma 0 (p ^ k) = k + 1 := by
proof body
Term-mode proof.
516 have hp' : Nat.Prime p := (prime_iff p).1 hp
517 simp only [sigma_zero_apply]
518 rw [Nat.divisors_prime_pow hp' k]
519 simp
520
521/-- Concrete sigma values at small prime powers. -/