isFiveAlmostPrime
A natural number n is 5-almost prime when the total number of its prime factors counted with multiplicity equals five. Number theorists classifying integers by the big-Omega function would cite this predicate for concrete checks. It is realized as a direct one-line abbreviation that invokes the existing bigOmega arithmetic function.
claimA natural number $n$ is 5-almost prime when $Ω(n)=5$, 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 sibling bigOmega is defined as the standard Ω(n) via ArithmeticFunction.cardFactors, which tallies prime factors with multiplicity. Upstream results include the bigOmega abbreviation itself together with peripheral structures from option programs and simplicial ledgers that do not affect the present definition.
proof idea
The declaration is a one-line wrapper that directly equates isFiveAlmostPrime n to the equality bigOmega n = 5.
why it matters in Recognition Science
This predicate feeds the family of concrete theorems five_almost_prime_eighty, five_almost_prime_fortyeight, five_almost_prime_onehundredeight and their siblings that verify specific 5-almost primes such as 176 = 2^4 × 11. The prime 11 appears in RS-relevant contexts; the definition therefore supplies a small but reusable interface inside the arithmetic scaffolding that may later connect to the phi-ladder and mass formulas.
scope and limits
- Does not prove any specific integer is 5-almost prime.
- Does not relate Ω to the J-cost or Recognition forcing chain.
- Does not supply bounds or Dirichlet-series estimates.
Lean usage
theorem five_almost_prime_176 : isFiveAlmostPrime 176 = true := by native_decideformal statement (Lean)
2434def isFiveAlmostPrime (n : ℕ) : Bool := bigOmega n = 5
proof body
Definition body.
2435
2436/-- 32 = 2⁵ is 5-almost prime. -/
used by (14)
-
five_almost_prime_eighty -
five_almost_prime_fortyeight -
five_almost_prime_onehundredeight -
five_almost_prime_onehundredeighty -
five_almost_prime_onehundredseventysix -
five_almost_prime_onehundredsixtytwo -
five_almost_prime_onehundredtwelve -
five_almost_prime_onehundredtwenty -
five_almost_prime_seventytwo -
five_almost_prime_thirtytwo -
five_almost_prime_twohundred -
five_almost_prime_twohundredeight -
five_almost_prime_twohundredfortythree -
five_almost_prime_twohundredseventytwo