four_almost_prime_eightyone
plain-language theorem explainer
81 equals 3 to the fourth power, so its total prime factor count with multiplicity is exactly four and the predicate holds. Researchers applying arithmetic functions to small factorizations would cite the explicit check. The proof is a direct computational evaluation via the native_decide tactic.
Claim. $81 = 3^4$ satisfies $bigOmega(81) = 4$, where $bigOmega(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. The definition states that a number is 4-almost prime precisely when $bigOmega(n) = 4$. This theorem records the concrete case $n = 81 = 3^4$. Upstream results include the isFourAlmostPrime definition itself together with structural predicates from foundation modules that enforce algebraic tautologies or collision-free properties.
proof idea
The declaration is a one-line wrapper that applies the native_decide tactic to evaluate the boolean predicate directly.
why it matters
This supplies a verified instance of the 4-almost-prime definition inside the arithmetic-functions module. It supports the number-theoretic scaffolding that prepares for Dirichlet inversion and prime-counting tools in the Recognition Science framework. No downstream uses are recorded yet, and the result does not touch the forcing chain or physical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.