isThreeAlmostPrime
plain-language theorem explainer
A natural number n is 3-almost prime precisely when the total count of its prime factors, with multiplicity, equals three. Number theorists classifying factorizations or working on arithmetic functions in the Recognition Science setting would cite this predicate for checks on numbers such as 8, 18, and 45. The definition is a direct one-line equality against the big-Omega function.
Claim. A natural number $n$ is 3-almost prime if and only if $Ω(n)=3$, 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 μ. The upstream bigOmega abbreviation is defined as the cardinality of prime factors counted with multiplicity. This local setting keeps statements minimal so that deeper Dirichlet inversion can be added once the basic interfaces stabilize.
proof idea
The definition is a one-line wrapper that applies the bigOmega function and checks equality to three.
why it matters
This predicate feeds the family of theorems that verify concrete 3-almost primes such as 8=2³, 18=2×3², 45=3²×5 (noted as an RS constant), and 50=2×5². It occupies the arithmetic-function layer of the NumberTheory.Primes module and supplies the classification tool used in those downstream checks. No direct tie to the forcing chain or phi-ladder is stated, but the predicate supports factorization counts that appear in later Recognition Science calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.