isFourAlmostPrime
plain-language theorem explainer
Natural numbers n are 4-almost primes precisely when the total count of prime factors with multiplicity equals 4. Number theorists working with arithmetic functions and concrete composite checks cite this predicate for examples such as 40, 54, 81, and 88. The definition is a direct one-line wrapper that delegates the count to the bigOmega function.
Claim. A natural number $n$ is 4-almost prime if and only if $Omega(n)=4$, where $Omega(n)$ denotes the number of prime factors of $n$ counted with multiplicity.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function. The upstream bigOmega abbreviation is defined as ArithmeticFunction.cardFactors and computes the standard $Omega(n)$, the total number of prime factors with multiplicity. This local setting keeps statements lightweight before any deeper Dirichlet algebra is added.
proof idea
The definition is a one-line wrapper that applies the bigOmega function and checks equality to 4.
why it matters
This predicate supports the family of downstream verification theorems for specific 4-almost primes including 40 = 2^3 * 5, 54 = 2 * 3^3, 81 = 3^4, and 88 = 2^3 * 11. It supplies the basic predicate inside the NumberTheory.Primes.ArithmeticFunctions module. No direct connection to the J-function, forcing chain, or phi-ladder appears here, but the predicate enables the arithmetic checks used in prime-related arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.