dvd_prime_pow_iff
plain-language theorem explainer
For a prime p the natural number i divides p^m precisely when i equals p^k for some k at most m. Number theorists in the Recognition framework cite this wrapper to keep downstream proofs independent of Mathlib API shifts. The proof is a one-line term that invokes Nat.dvd_prime_pow after a simpa that unfolds the Prime predicate.
Claim. Let $p$ be prime. For natural numbers $i$ and $m$, $i$ divides $p^m$ if and only if there exists $k$ with $k ≤ m$ such that $i = p^k$.
background
The declaration sits inside the Mathlib wrappers module for the prime toolkit. That module supplies stable repo-local names for a small set of high-value prime theorems so that downstream code can depend on IndisputableMonolith.NumberTheory.Primes names rather than chasing Mathlib changes. The local statement classifies the divisors of a prime power as themselves prime powers.
proof idea
One-line wrapper that applies Nat.dvd_prime_pow after a simpa tactic that unfolds the Prime predicate.
why it matters
The wrapper supplies a stable interface for divisor properties inside the prime toolkit. It supports the Recognition Science number-theory layer used for mass ladders and phi-based counting, even though no downstream uses are recorded in the current graph. The result aligns with the framework's reliance on elementary arithmetic facts to anchor higher-level constructions such as the eight-tick octave and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.