six_almost_prime_onehundredfortyfour
plain-language theorem explainer
The theorem verifies that 144, with prime factorization 2^4 times 3^2, has total prime factor count exactly six. Number theorists using arithmetic functions in the Recognition Science setting would cite this as a concrete instance check. The proof is a direct native decision procedure that evaluates the big-Omega predicate.
Claim. $Ω(144) = 6$, where $Ω(n)$ counts the prime factors of $n$ with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. A number is 6-almost prime precisely when its total number of prime factors counted with multiplicity equals six, via the definition bigOmega n = 6. This verification belongs to a collection of small explicit checks that stabilize the basic interfaces before deeper Dirichlet algebra is layered on.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the equality directly.
why it matters
This instance supports the 6-almost-prime definition inside the arithmetic-functions module and contributes to the number-theoretic footholds used across the Recognition Science framework. It has no listed downstream dependencies, so it functions as a standalone verification rather than a lemma feeding a larger parent theorem. The check aligns with the lightweight style of the module, which keeps statements minimal until the basic interfaces stabilize.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.