five_almost_prime_twohundredeight
plain-language theorem explainer
208 factors as 2^4 times 13 and therefore carries exactly five prime factors counted with multiplicity. Number theorists checking small almost-prime cases for arithmetic tables or Recognition Science ladder verifications would reference this explicit instance. The proof reduces the claim to a direct computational decision on the total prime-factor count.
Claim. $Ω(208) = 5$, where $Ω(n)$ is 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 and extending to big-Omega, the sum of exponents in the prime factorization. A number satisfies the five-almost-prime predicate exactly when this sum equals five. The local setting is therefore a collection of small, decidable checks that can later feed Dirichlet inversion or prime-counting arguments.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the equality directly from the definition of big-Omega.
why it matters
The result supplies a concrete, machine-verified data point inside the arithmetic-function layer that supports later prime-distribution work. It sits downstream of the isFiveAlmostPrime definition and aligns with the need for explicit small-case anchors before scaling to phi-ladder mass formulas or eight-tick octave counts. No downstream theorems yet consume it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.