three_almost_prime_sixtyeight
plain-language theorem explainer
68 = 2² × 17 satisfies Ω(n) = 3. Number theorists checking small composites against Recognition Science constants would cite this instance when validating the prime 17 in the phi-ladder. The proof is a one-line native decision procedure that evaluates the bigOmega predicate on the concrete input.
Claim. $Ω(68) = 3$, where $Ω(n)$ denotes 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. A number is three-almost-prime precisely when bigOmega n equals 3, as defined by the sibling predicate isThreeAlmostPrime. The local setting is a collection of small verification statements for primes and almost-primes that can later support Dirichlet inversion or Recognition Science mass formulas.
proof idea
The proof is a one-line native_decide application that evaluates the boolean isThreeAlmostPrime 68 directly.
why it matters
This instance confirms that 68 meets the three-almost-prime criterion with the factor 17 flagged as RS-relevant. It supports verification steps inside NumberTheory.Primes.ArithmeticFunctions but records no downstream uses. It touches the program of checking small composites against constants such as the alpha band and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.