five_almost_prime_onehundredsixtytwo
plain-language theorem explainer
162 satisfies the 5-almost-prime condition because its total number of prime factors with multiplicity equals five. Researchers verifying small-integer cases on the Recognition Science phi-ladder would cite this result when confirming arithmetic properties of candidate masses. The proof consists of a single native_decide application that computes bigOmega directly from the definition.
Claim. $Ω(162) = 5$, where $Ω(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 is defined by equality of bigOmega n to 5. bigOmega counts the total number of prime factors with multiplicity, as referenced in the sibling definitions. Upstream results include the definition of isFiveAlmostPrime itself, which reduces the predicate to bigOmega n = 5.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the boolean expression arising from the definition of isFiveAlmostPrime.
why it matters
This instance supports verification of small 5-almost-primes relevant to the Recognition Science mass formula on the phi-ladder. It connects to the broader arithmetic functions module that prepares Möbius inversion tools. No direct downstream use is recorded yet, but it fills a concrete check in the number-theoretic scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.