bigOmega_six
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 in Recognition Science
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.
scope and limits
- Does not generalize the result to arbitrary integers.
- Does not connect to analytic number theory estimates.
- Does not incorporate multiplicity distinctions beyond the definition.
formal statement (Lean)
808theorem bigOmega_six : bigOmega 6 = 2 := by native_decide
proof body
Term-mode proof.
809
810/-- ω(6) = 2 (distinct prime factors: 2, 3). -/