six_almost_prime_sixtyfour
plain-language theorem explainer
64 equals 2 to the sixth power and therefore carries exactly six prime factors counted with multiplicity, satisfying the predicate that marks a 6-almost prime. Number theorists maintaining arithmetic-function interfaces inside the Recognition Science codebase would cite the result as a verified base case. The proof reduces to a single native_decide call that evaluates the equality by direct computation.
Claim. $Ω(64) = 6$, where $Ω(n)$ counts the total number of prime factors of $n$ with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. The predicate isSixAlmostPrime is defined directly as bigOmega n = 6. The upstream definition of isSixAlmostPrime encodes the 6-almost-prime condition via the big-Omega arithmetic function that tallies prime factors with multiplicity.
proof idea
The proof is a one-line term that applies native_decide to confirm that bigOmega 64 evaluates to 6.
why it matters
The declaration supplies a concrete base-case verification inside the arithmetic-functions module. It supports prime-related calculations that may later feed into Recognition Science constructions such as the phi-ladder or mass formulas, although no downstream use is recorded. It aligns with the framework's pattern of explicit computational checks for small integers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.