four_almost_prime_fiftyfour
plain-language theorem explainer
The declaration verifies that 54 has exactly four prime factors counted with multiplicity. Number theorists checking small cases in arithmetic function libraries would reference this concrete instance. The proof reduces to a native decision procedure that directly evaluates the bigOmega count on 54 and confirms the equality.
Claim. $Ω(54) = 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 is 4-almost prime precisely when its total prime factor count with multiplicity equals 4, via the definition isFourAlmostPrime n := bigOmega n = 4. This instance confirms the property for 54, which factors as 2 × 3³.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the boolean equality isFourAlmostPrime 54 = true by direct computation of bigOmega.
why it matters
This concrete verification populates the arithmetic functions toolkit in the Recognition Science monolith. It supports downstream number theory constructions that rely on almost-prime classifications before Dirichlet algebra is layered on. No immediate parent theorem is listed among the used-by edges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.