three_almost_prime_fifty
plain-language theorem explainer
50 factors as 2 times 5 squared and therefore carries exactly three prime factors counted with multiplicity. Number theorists building verified libraries of arithmetic functions would cite this as a concrete base case. The proof is a direct computational evaluation of the big-omega predicate via native_decide.
Claim. $50 = 2^1 5^2$ satisfies $Ω(50) = 3$, 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 3-almost prime precisely when its total prime factor count with multiplicity equals three, via the definition isThreeAlmostPrime n := bigOmega n = 3. The doc-comment records the explicit factorization 50 = 2 × 5² for this instance.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the boolean isThreeAlmostPrime 50 by direct computation of bigOmega.
why it matters
This supplies a verified concrete case inside the arithmetic functions module of the primes development. It does not yet feed any downstream theorems. The declaration remains isolated from the forcing chain landmarks T0-T8 and from physical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.