omega_prime
plain-language theorem explainer
For any prime number p, the arithmetic function omega that counts distinct prime factors satisfies omega(p) = 1. Number theorists applying prime factorization counts or preparing Möbius inversion steps would cite this elementary property. The proof is a short term-mode reduction that converts the local Prime hypothesis via an equivalence and invokes the standard Mathlib cardinality fact for primes.
Claim. If $p$ is prime, then $ω(p) = 1$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Here omega denotes the arithmetic function ω(n) that counts the number of distinct prime factors of n. The local Prime predicate is defined as an alias for Nat.Prime, with the equivalence prime_iff providing the bridge to Mathlib's library. Upstream, the structure for in UniversalForcingSelfReference supplies meta-realization context, though the immediate dependencies are the Prime alias and its equivalence.
proof idea
The proof first converts the hypothesis hp : Prime p into Nat.Prime p using prime_iff. It then simplifies the definition of omega and applies the Mathlib lemma ArithmeticFunction.cardDistinctFactors_apply_prime to conclude that the count is 1.
why it matters
This establishes a foundational property of the omega function for primes, supporting later developments in arithmetic functions such as Möbius inversion within the Recognition Science framework. It aligns with the number-theoretic underpinnings needed for the phi-ladder and mass formulas, though no direct downstream uses are recorded yet. It fills a basic slot in the primes arithmetic functions module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.