five_almost_prime_onehundredeight
plain-language theorem explainer
108 factors as 2 squared times 3 cubed and therefore carries total prime factor multiplicity five, satisfying the five-almost-prime predicate. Number theorists verifying concrete values of arithmetic functions would cite this explicit instance. The proof reduces to a single native_decide invocation that evaluates the bigOmega count directly.
Claim. $108$ satisfies $Ω(108)=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. A number is five-almost-prime precisely when its total prime factor count with multiplicity equals five, via the definition isFiveAlmostPrime n := bigOmega n = 5. The upstream definition states: 'A number is 5-almost prime if Ω(n) = 5.'
proof idea
The declaration is a one-line wrapper that applies native_decide to evaluate the boolean equality by direct computation of bigOmega 108.
why it matters
This supplies a verified concrete case inside the arithmetic functions module that supports prime-related calculations. It contributes to the number-theoretic scaffolding used in Recognition Science, where explicit factor counts enter mass formulas on the phi-ladder. No immediate downstream theorems reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.