four_almost_prime_twentyfour
plain-language theorem explainer
24 equals 2 cubed times 3 and therefore carries exactly four prime factors counted with multiplicity, satisfying the four-almost-prime predicate. Number theorists building arithmetic-function examples inside the Recognition framework cite this as a verified base case. The proof reduces immediately to native decision on the definition of bigOmega applied to the concrete integer 24.
Claim. $Omega(24) = 4$, 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. The predicate isFourAlmostPrime is defined by the equation bigOmega n = 4. The immediate upstream result is the sibling definition isFourAlmostPrime itself, which unfolds the predicate to the bigOmega arithmetic function.
proof idea
The proof is a one-line wrapper that invokes native_decide on the boolean equality isFourAlmostPrime 24 = true.
why it matters
This instance supplies a concrete proved example inside the arithmetic-functions layer of NumberTheory.Primes. It supports the module's preparation of Möbius footholds for later Dirichlet algebra, though it does not invoke the forcing chain T5-T8 or the Recognition Composition Law. No downstream uses appear in the current dependency graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.