five_almost_prime_eighty
plain-language theorem explainer
80 factors as 2^4 times 5, yielding total prime factor count with multiplicity exactly five. Researchers checking small-integer instances of arithmetic predicates would cite this explicit verification. The proof reduces to a single native_decide call that evaluates the defining Boolean expression directly.
Claim. $Ω(80)=5$, where $Ω(n)$ counts the total number of prime factors of $n$ counted with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The predicate isFiveAlmostPrime is introduced by the definition isFiveAlmostPrime n := bigOmega n = 5, where bigOmega is the standard total prime-factor counting function. This concrete instance confirms the predicate for the integer 80.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the Boolean expression bigOmega 80 = 5.
why it matters
The declaration supplies a verified small-case instance for the 5-almost-prime predicate inside the arithmetic-functions module. It supports explicit checks before Dirichlet algebra is layered on, consistent with the module's stated goal of keeping statements lightweight. No downstream theorems currently depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.