isFourAlmostPrime
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not compute the explicit prime factorization of n.
- Does not establish primality or squarefreeness of n.
- Does not reference the Möbius function or inversion formulas.
- Does not connect to physical constants, the phi-ladder, or the Recognition Science forcing chain.
formal statement (Lean)
2219def isFourAlmostPrime (n : ℕ) : Bool := bigOmega n = 4
proof body
Definition body.
2220
2221/-- 16 = 2⁴ is 4-almost prime. -/
used by (17)
-
four_almost_prime_eightyeight -
four_almost_prime_eightyfour -
four_almost_prime_eightyone -
four_almost_prime_fiftyfour -
four_almost_prime_fiftysix -
four_almost_prime_forty -
four_almost_prime_ninety -
four_almost_prime_onehundred -
four_almost_prime_onehundredforty -
four_almost_prime_onehundredfour -
four_almost_prime_onehundredthirtysix -
four_almost_prime_onehundredthirtytwo -
four_almost_prime_onehundredtwentysix -
four_almost_prime_sixteen -
four_almost_prime_sixty -
four_almost_prime_thirtysix -
four_almost_prime_twentyfour