bigOmega_six
plain-language theorem explainer
The declaration establishes that the arithmetic function Ω evaluates to 2 at the integer 6. Researchers computing prime factor counts for small composites would invoke this fact when verifying basic cases in Dirichlet series or inversion formulas. The proof is a direct native_decide evaluation of the cardFactors definition.
Claim. $Ω(6) = 2$, where $Ω(n)$ denotes the total number of prime factors of $n$ counted with multiplicity.
background
The module supplies lightweight wrappers around Mathlib's arithmetic functions, beginning with the Möbius function and extending to Ω(n). The function bigOmega is defined as the cardinality of prime factors with multiplicity, i.e., Ω(n) equals the sum of exponents in the prime factorization of n. This sits upstream of more advanced number-theoretic constructions such as Dirichlet convolution and inversion.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the definition of bigOmega at 6 directly.
why it matters
This basic evaluation supports the arithmetic function infrastructure used in prime-related lemmas within the Recognition Science number theory layer. It provides a concrete anchor point for Ω(n) computations that may feed into Möbius function applications or squarefree checks downstream. No open questions are directly addressed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.