radical_prime_pow
plain-language theorem explainer
The result asserts that the radical of a prime power p^k equals p itself for any prime p and positive integer k. Number theorists simplifying expressions in arithmetic functions or preparing Möbius inversion over prime powers would cite this identity. The proof is a direct one-line simplification that unfolds the radical definition together with the prime factorization of p^k.
Claim. If $p$ is prime and $k$ is a positive integer, then the radical of $p^k$ equals $p$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The radical function extracts the square-free kernel of an integer by taking the product of its distinct prime factors. This theorem supplies a basic fact needed before the von Mangoldt sum identity that follows in the same file. Upstream results include the identity maps in cost algebras and forcing structures that calibrate the underlying J-cost framework.
proof idea
The proof is a one-line wrapper that applies the definition of radical, the lemma on prime factors of p^k, the singleton product, and the identity map.
why it matters
This identity anchors the prime-power case inside the arithmetic-functions layer that supports Möbius inversion and von Mangoldt sums. It fills a standard number-theoretic fact within the Recognition Science arithmetic scaffolding, preparing later steps that connect to the phi-ladder and complexity measures. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.