divisors_prime_pow
plain-language theorem explainer
The theorem asserts that for a prime p and natural number k the divisors of p^k are exactly the powers p^0 through p^k. Researchers computing arithmetic functions such as divisor counts or sigma functions for prime powers within the Recognition Science framework would cite this result. The proof is a one-line wrapper that converts the local Prime predicate to Mathlib's Nat.Prime and delegates to the library theorem Nat.divisors_prime_pow.
Claim. Let $p$ be a prime number and $k$ a natural number. The set of positive divisors of $p^k$ equals exactly the set of powers $p^0, p^1, ..., p^k$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function. This declaration supplies the explicit form of the divisor set for a prime power, a basic building block for later arithmetic-function identities. Upstream structures such as PhiForcingDerived.of and SpectralEmergence.of supply the J-cost and discrete-state counting conventions that ultimately depend on such divisor facts for enumerating phi-ladder rungs.
proof idea
The term proof first applies the equivalence prime_iff to obtain Nat.Prime p from the hypothesis hp : Prime p, then invokes Nat.divisors_prime_pow directly on that converted prime and the exponent k.
why it matters
The result is invoked by card_divisors_prime_pow and sigma_zero_prime_pow in the same module, both of which conclude that the number of divisors of p^k equals k + 1. It supplies a foundational arithmetic step that supports discrete counting arguments in the Recognition Science framework, including those tied to the eight-tick octave and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.