six_almost_prime_onehundredsixty
plain-language theorem explainer
The declaration verifies that 160 factors as 2^5 times 5 and therefore carries exactly six prime factors counted with multiplicity, satisfying the 6-almost-prime criterion. Number theorists checking concrete cases inside Recognition Science arithmetic functions would cite this instance when populating the phi-ladder or mass formulas. The proof reduces to a single native_decide call that evaluates the bigOmega predicate directly.
Claim. $Omega(160) = 6$, where $Omega(n)$ denotes the total number of prime factors of $n$ counted with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. A number is 6-almost prime precisely when bigOmega n equals 6. The upstream definition isSixAlmostPrime encodes this criterion as a Bool-valued predicate on natural numbers.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the equality bigOmega 160 = 6.
why it matters
This concrete check supplies a verified data point for arithmetic-function usage in the NumberTheory.Primes section. It supports downstream mass-formula and phi-ladder constructions that rely on controlled prime-factor counts. No parent theorem is recorded in the used-by graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.