three_almost_prime_sixtyeight
plain-language theorem explainer
68 factors as 2 squared times 17 and therefore satisfies Omega(68) equals 3. Number theorists checking concrete almost-prime instances for Recognition Science applications would cite this verification. The proof is a one-line native decision that evaluates the bigOmega definition directly.
Claim. $Omega(68) = 3$, where $Omega(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 and extending to bigOmega. A number n is declared 3-almost prime precisely when bigOmega n equals 3, as defined in isThreeAlmostPrime. This instance checks the concrete case n = 68 = 2² × 17.
proof idea
The proof is a term-mode application of native_decide that computes the equality isThreeAlmostPrime 68 = true by direct evaluation of bigOmega 68.
why it matters
This supplies a verified concrete example of a 3-almost prime at 68, noted as RS-relevant due to the prime factor 17. It supports downstream work on prime distributions within the Recognition Science number theory layer, though no immediate parent theorems depend on it yet. It aligns with the arithmetic function footholds needed for Möbius inversion and related tools.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.