six_almost_prime_sixhundredtwentyfour
plain-language theorem explainer
624 factors as 2^4 times 3 times 13 and therefore carries exactly six prime factors counted with multiplicity. Number theorists verifying explicit values inside the arithmetic functions library would cite this result for direct checks. The proof reduces to a single native_decide call that evaluates the bigOmega predicate by computation.
Claim. $Ω(624) = 6$, 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 6-almost prime precisely when its total prime factor count with multiplicity equals six, via the definition isSixAlmostPrime n := bigOmega n = 6. This instance checks the concrete factorization 624 = 2^4 × 3 × 13.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the equality directly from the definition of isSixAlmostPrime.
why it matters
This declaration supplies a verified concrete case for the six-almost-prime predicate. It anchors explicit numerical checks inside the arithmetic functions library, consistent with the module's role of providing Möbius footholds before deeper Dirichlet algebra. No parent theorems appear in the current dependency graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.