five_almost_prime_seventytwo
plain-language theorem explainer
72 factors as 2 cubed times 3 squared and therefore satisfies Omega of 72 equals 5. Researchers checking concrete almost-prime counts inside the Recognition Science arithmetic-functions library would reference this verified instance. The proof is a direct native decision that evaluates the big-Omega definition on 72.
Claim. $Omega(72) = 5$, where $Omega(n)$ counts the total number of prime factors of $n$ with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. The predicate isFiveAlmostPrime n holds exactly when bigOmega n equals 5. The upstream definition of isFiveAlmostPrime is the direct source for the predicate, while sibling declarations supply the bigOmega implementation and its relation to square-free checks.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the boolean equality isFiveAlmostPrime 72 = true by direct computation of bigOmega 72.
why it matters
This supplies a concrete verified case of a 5-almost prime that can anchor further arithmetic-function statements in the Recognition Science number-theory layer. It sits alongside Möbius and bigOmega wrappers but records no downstream uses yet, leaving open its role in larger prime-distribution or forcing-chain arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.