four_almost_prime_ninety
plain-language theorem explainer
The declaration verifies that 90 factors as 2 times 3 squared times 5 and therefore has total prime factor count exactly four under the bigOmega definition. Number theorists applying arithmetic functions within Recognition Science would cite this as a concrete check. The proof reduces to a direct native computation of the equality.
Claim. The integer 90 satisfies $Ω(90)=4$, where $Ω(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. A number satisfies the 4-almost-prime predicate when bigOmega n equals 4, where bigOmega returns the total number of prime factors counted with multiplicity. The upstream definition isFourAlmostPrime n := bigOmega n = 4 supplies the predicate used here.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the boolean equality directly from the bigOmega computation.
why it matters
This supplies a verified example inside the arithmetic functions module that supports concrete checks on bigOmega and related predicates. No downstream theorems are listed. It illustrates the 4-almost-prime notion without touching the main forcing chain or Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.