three_almost_prime_sixtysix
plain-language theorem explainer
66 factors as 2 × 3 × 11 and therefore satisfies Ω(n) = 3. Researchers checking small cases inside the Recognition Science arithmetic-function layer would cite the result when building tables of 3-almost primes or verifying RS-relevant factors such as 11. The proof is a one-line native_decide wrapper that evaluates the Boolean equality by direct computation.
Claim. $66 = 2 × 3 × 11$ and therefore $Ω(66) = 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 n is declared 3-almost prime precisely when its total prime factor count with multiplicity equals three, as encoded in the definition isThreeAlmostPrime n := bigOmega n = 3. This instance for 66 supplies a concrete data point whose prime 11 is flagged as RS-relevant in the surrounding comments.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the Boolean equality directly.
why it matters
This concrete verification populates the list of small 3-almost primes used in the Recognition Science number-theoretic scaffolding. It connects to the broader arithmetic-function interface that supports Möbius inversion and square-free checks elsewhere in the module. No downstream theorems currently depend on it, leaving its role as a verified example rather than a lemma in a larger chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.