four_almost_prime_onehundredfour
plain-language theorem explainer
The declaration confirms that 104 factors as 2 cubed times 13 and therefore carries exactly four prime factors counted with multiplicity. Number theorists inspecting concrete almost-prime instances inside the Recognition Science arithmetic-functions module would cite this check. The proof reduces to a single native_decide evaluation of the big-Omega predicate.
Claim. $104 = 2^3 · 13$ satisfies $Ω(104) = 4$, where $Ω$ counts all prime factors with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. A number n is defined to be 4-almost prime precisely when its big-Omega value equals 4. The upstream definition isFourAlmostPrime implements this as bigOmega n = 4, with the present theorem supplying a concrete instance for n = 104.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the Boolean expression isFourAlmostPrime 104 directly.
why it matters
This concrete check populates the arithmetic functions layer that supports Möbius inversion and prime counting within Recognition Science. It supplies an explicit 4-almost prime example (104 = 2^3 × 13) that can be referenced when building higher-level statements about almost-prime distributions. No downstream theorems currently depend on it, leaving its role as a verified data point rather than a lemma in a larger chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.