omega_prime_pow
plain-language theorem explainer
The declaration shows that the arithmetic function counting distinct prime factors evaluates to one on any prime power. Researchers handling Möbius inversion or Dirichlet series over prime powers in Recognition Science would reference this reduction. The short proof converts the custom Prime predicate to the standard library version, confirms the exponent is nonzero, and delegates to Mathlib's cardDistinctFactors lemma for prime powers.
Claim. Let $p$ be a prime number and let $k$ be a positive integer. Then the number of distinct prime factors satisfies $ω(p^k)=1$.
background
This theorem sits in the module supplying lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Here ω denotes the distinct-prime-factor counter, realized as ArithmeticFunction.cardDistinctFactors. The hypothesis Prime p is converted to Nat.Prime via the prime_iff lemma from the Basic submodule. The module documentation notes that deeper Dirichlet algebra can be layered once these basic interfaces stabilize.
proof idea
The proof obtains Nat.Prime p from the Prime hypothesis via prime_iff, derives k ≠ 0 from the positivity assumption using Nat.pos_iff_ne_zero, simplifies the definition of omega, and applies the library fact ArithmeticFunction.cardDistinctFactors_apply_prime_pow.
why it matters
This identity supplies a standard reduction for arithmetic functions on prime powers inside the Recognition Science number-theory layer. It supports the Möbius footholds described in the module documentation and prepares for later prime-power calculations. No direct link to the T0-T8 forcing chain or phi-ladder is present, yet the result closes a basic gap before Dirichlet inversion is developed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.