four_almost_prime_eightyfour
plain-language theorem explainer
84 factors as 2 squared times 3 times 7 and therefore satisfies Omega(84) equals 4, confirming it is a 4-almost prime. Researchers using arithmetic functions for prime-counting arguments would cite this explicit verification. The proof is a one-line wrapper that invokes native_decide on the definition of isFourAlmostPrime.
Claim. $84 = 2^2 3 7$ satisfies $Omega(84) = 4$, hence is a 4-almost prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function mu. A 4-almost prime is introduced via the predicate isFourAlmostPrime n, which returns true exactly when bigOmega n equals 4. The upstream definition states: A number is 4-almost prime if Omega(n) = 4.
proof idea
This is a one-line wrapper that applies native_decide to evaluate isFourAlmostPrime 84 directly from its definition bigOmega n = 4.
why it matters
The declaration supplies a concrete instance check inside the arithmetic-functions module whose parent goal is to stabilize basic interfaces before layering Dirichlet inversion. No downstream uses are recorded, so the result currently serves only as a verified data point for later number-theoretic constructions in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.