bigOmega_apply
plain-language theorem explainer
The theorem equates the total number of prime factors of a natural number n counted with multiplicity to the length of its prime factors list. Number theorists using arithmetic functions inside the Recognition Science setup cite this when reducing Omega computations to explicit factorization data. The proof is a one-line wrapper that unfolds the definition of bigOmega and invokes the cardFactors apply lemma.
Claim. For every natural number $n$, the function $Omega(n)$ equals the length of the list of prime factors of $n$.
background
The module supplies thin wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to prime-counting variants. bigOmega is introduced as the arithmetic function cardFactors, which records the total number of prime factors counted with multiplicity. The local setting is a lightweight interface layer that defers deeper Dirichlet inversion until the basic maps stabilize; upstream structures on J-cost convexity and spectral emergence supply the surrounding Recognition Science context for these number-theoretic tools.
proof idea
The proof is a one-line wrapper. It unfolds the definition of bigOmega to cardFactors and then applies the cardFactors_apply lemma from the imported arithmetic-function library.
why it matters
The result is invoked directly by the theorems establishing Omega(1) equals zero, Omega of a prime power equals the exponent, and the value of the Liouville function at one. It supplies the basic reduction step for prime-factor counting inside the arithmetic-functions module, supporting later work on Möbius inversion and related identities in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.