isSixAlmostPrime
plain-language theorem explainer
A natural number n is 6-almost prime precisely when its total number of prime factors counted with multiplicity equals 6. Number theorists verifying concrete almost-prime instances for Recognition Science calculations would cite this definition. The declaration is a direct one-line abbreviation that delegates entirely to the upstream bigOmega function.
Claim. A natural number $n$ is called 6-almost prime when its total number of prime factors counted with multiplicity satisfies $Ω(n)=6$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to bigOmega. Upstream, bigOmega is the abbreviation for ArithmeticFunction.cardFactors, which returns the standard Ω(n) counting prime factors with multiplicity. This definition therefore translates the classical notion of 6-almost primality into the local arithmetic interface used by the rest of the NumberTheory.Primes hierarchy.
proof idea
one-line wrapper that applies bigOmega
why it matters
The definition is the common predicate for the family of downstream theorems that certify concrete 6-almost primes such as 528 = 2^4 × 3 × 11, 544 = 2^5 × 17 and 560 = 2^4 × 5 × 7. These instances feed the Recognition Science arithmetic pipeline that supports the phi-ladder mass formula and the eight-tick octave structure. It closes a small but frequently referenced interface between Mathlib's factor-counting primitives and the specific numerical checks required by the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.