six_almost_prime_twohundredtwentyfour
plain-language theorem explainer
224 factors as 2^5 times 7 and therefore carries exactly six prime factors counted with multiplicity, satisfying the 6-almost-prime predicate. Researchers checking concrete integers against the Recognition Science phi-ladder mass formulas would cite this verification. The proof is a one-line native_decide computation that evaluates the bigOmega count directly.
Claim. $Omega(224) = 6$, 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. isSixAlmostPrime is defined by the equality bigOmega n = 6, where bigOmega is the standard total prime-factor count with multiplicity. The theorem verifies the concrete case 224 = 2^5 × 7. The upstream definition of isSixAlmostPrime supplies the direct link to bigOmega.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the equality bigOmega 224 = 6 directly.
why it matters
This supplies a verified instance of a 6-almost prime inside the arithmetic-functions module. It supports Recognition Science checks for numbers appearing on the phi-ladder, consistent with the framework's use of specific integers such as 64 = 2^6. No downstream theorems depend on it, so it functions as a terminal verification step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.