six_almost_prime_twohundredforty
plain-language theorem explainer
240 factors as 2^4 times 3 times 5 and therefore carries exactly six prime factors counted with multiplicity, satisfying the predicate that defines a 6-almost prime. Number theorists maintaining the arithmetic layer of Recognition Science would cite this concrete case when checking small instances against the bigOmega count. The proof is a one-line wrapper that invokes native_decide to expand the factorization and verify the equality directly.
Claim. $240 = 2^4 3 5$ and therefore satisfies $bigOmega(240) = 6$, where $bigOmega(n)$ is the total number of prime factors of $n$ counted with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to bigOmega. A number is defined as 6-almost prime precisely when bigOmega n equals 6. This instance for 240 builds on the upstream definition of isSixAlmostPrime, which directly encodes that condition as a Boolean predicate.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate isSixAlmostPrime 240 and confirm it equals true by direct computation of the prime factorization.
why it matters
This declaration supplies a concrete verified instance supporting the arithmetic functions layer in NumberTheory.Primes. It fills an explicit slot by confirming an RS-relevant 6-almost prime, consistent with the module's focus on Möbius footholds and bigOmega applications. No parent theorems appear in the used_by graph, indicating it functions as a terminal example rather than an intermediate lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.