bigOmega_prime
plain-language theorem explainer
The theorem states that the total number of prime factors with multiplicity, denoted Ω(p), equals 1 whenever p is prime. Number theorists using arithmetic functions in the Recognition Science setting would cite this as the base evaluation of the big omega function. The proof converts the local primality hypothesis to Mathlib's Nat.Prime via an equivalence and then applies the cardFactors prime lemma directly.
Claim. If $p$ is a prime natural number, then the arithmetic function counting prime factors with multiplicity satisfies $Ω(p) = 1$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and including bigOmega as the cardFactors function. This function returns the number of prime factors of its argument, counting multiplicity, and is denoted Ω(n). The Prime predicate is defined as a transparent alias for Nat.Prime, with the equivalence prime_iff identifying the two predicates exactly.
proof idea
The term proof first obtains a Nat.Prime instance by applying the left direction of the prime_iff equivalence to the hypothesis. It then invokes the exact tactic on the Mathlib lemma ArithmeticFunction.cardFactors_apply_prime applied to that instance, which yields the required equality.
why it matters
This supplies the base case Ω(p) = 1 for the big omega function on primes, as recorded in the declaration comment. It supports subsequent arithmetic-function identities in the module, including those involving the Möbius function. Within the Recognition Science framework the result anchors number-theoretic primitives that feed into the forcing chain and constant derivations, though no direct citation to T0-T8 appears here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.