five_almost_prime_fortyeight
plain-language theorem explainer
Verification that 48 factors as 2^4 times 3 and therefore satisfies the 5-almost-prime condition appears here. Number theorists maintaining explicit tables of small almost-primes would cite the instance. The proof consists of a single native decision step on the big-Omega predicate.
Claim. $Omega(48) = 5$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. bigOmega n returns the total number of prime factors of n counted with multiplicity, and isFiveAlmostPrime n holds exactly when this count equals five. The local setting keeps statements minimal pending deeper Dirichlet algebra.
proof idea
One-line wrapper that applies native_decide to the equality bigOmega 48 = 5.
why it matters
This supplies a concrete verified instance inside the arithmetic functions module. It contributes to the collection of small almost-prime facts but carries no listed downstream uses. No direct tie to the Recognition Science forcing chain or constants is present.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.