four_almost_prime_sixty
plain-language theorem explainer
60 factors as 2² × 3 × 5 and therefore satisfies Ω(60) = 4. Number theorists checking small almost-prime instances in the Recognition Science arithmetic library would cite this specific evaluation. The proof reduces to a single native_decide tactic that computes bigOmega 60 directly from its definition.
Claim. The integer 60 satisfies $Ω(60) = 4$, 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 4-almost prime precisely when bigOmega n equals 4. This instance confirms the property for n = 60 by direct evaluation.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic to evaluate the boolean expression isFourAlmostPrime 60.
why it matters
This theorem supplies a concrete small-case verification for the 4-almost-prime predicate in the arithmetic functions module. It supports downstream checks in prime-related constructions within Recognition Science, though no immediate parent theorems are listed. It aligns with the framework's use of small integers for ladder checks but does not invoke the forcing chain or RCL directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.