bigOmega_def
The theorem equates the Recognition Science bigOmega function to Mathlib's cardFactors arithmetic function by reflexivity. Number theorists using prime factor counts with multiplicity in the framework cite this for simp-based reductions in arithmetic proofs. The proof is a direct one-line reflexivity matching the upstream abbreviation.
claimLet $Ω$ be the arithmetic function that counts the prime factors of a natural number $n$ with multiplicity. Then $Ω$ equals the standard arithmetic function cardFactors, so $Ω(n)$ is the length of the prime factors list of $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and extending to related maps. The upstream result introduces bigOmega as the abbreviation for the total prime factor count with multiplicity. This keeps the interface minimal before adding Dirichlet inversion or other algebra.
proof idea
The proof is a one-line wrapper that applies reflexivity to the abbreviation bigOmega, confirming it matches ArithmeticFunction.cardFactors exactly.
why it matters in Recognition Science
This supplies the definitional equality that enables simp lemmas for prime-factor arithmetic in the Recognition Science number theory layer. It aligns the custom Ω with Mathlib conventions inside the arithmetic functions module, supporting later manipulations even though no downstream theorems are recorded yet.
scope and limits
- Does not compute explicit values of Ω at concrete integers.
- Does not relate Ω to the Möbius function or other arithmetic maps.
- Does not establish multiplicativity or other functional equations.
formal statement (Lean)
75@[simp] theorem bigOmega_def : bigOmega = ArithmeticFunction.cardFactors := rfl
proof body
Term-mode proof.
76
77/-- `Ω(n) = n.primeFactorsList.length`. -/