five_almost_prime_twohundred
plain-language theorem explainer
200 factors as 2^3 times 5^2 and therefore carries exactly five prime factors counted with multiplicity, satisfying the 5-almost-prime predicate. Number theorists building arithmetic-function libraries or concrete factorization checks inside Recognition Science would reference this instance. The proof reduces to a single native_decide evaluation of the bigOmega predicate.
Claim. Let $n=200=2^3 5^2$. Then the total number of prime factors of $n$ counted with multiplicity equals 5.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. The predicate isFiveAlmostPrime is defined directly by the equality bigOmega n = 5, where bigOmega counts prime factors with multiplicity. The upstream definition of isFiveAlmostPrime encodes this condition without additional hypotheses.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate isFiveAlmostPrime 200.
why it matters
This theorem supplies a verified concrete case of a 5-almost prime inside the arithmetic-functions module that supports Möbius footholds. It contributes a small verified datum to the number-theoretic layer of Recognition Science without feeding any recorded downstream theorems. No open scaffolding remains for this specific integer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.