three_almost_prime_seventy
plain-language theorem explainer
70 factors as 2 × 5 × 7 and therefore carries exactly three prime factors counted with multiplicity. Number theorists checking small cases of almost-prime counts would cite this explicit verification. The proof reduces to a direct computational evaluation of the bigOmega predicate via native_decide.
Claim. $Ω(70) = 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 as a foothold for later Dirichlet work. A number $n$ is 3-almost prime precisely when bigOmega $n$ equals 3; the upstream definition states this predicate directly as isThreeAlmostPrime $(n : ℕ) : Bool := bigOmega n = 3$. The local setting remains confined to these basic arithmetic interfaces without invoking inversion formulas.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate isThreeAlmostPrime 70 directly from the bigOmega definition.
why it matters
This supplies a verified concrete instance inside the arithmetic-functions layer of the NumberTheory module. It supports downstream checks on prime factorizations without introducing hypotheses or linking to the Recognition Science forcing chain, phi-ladder, or constants such as $c=1$ and $G=φ^5/π$. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.