five_almost_prime_onehundredtwenty
plain-language theorem explainer
120 equals 2 cubed times 3 times 5 and therefore satisfies Omega of 120 equals 5, confirming it as five-almost-prime. Number theorists building tables of almost primes within the Recognition Science arithmetic layer would cite this concrete check. The proof is a one-line native_decide evaluation of the defining boolean equality.
Claim. $120 = 2^3 3 5$ satisfies $Omega(120) = 5$, where $Omega(n)$ counts the total number of prime factors of $n$ with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. The predicate isFiveAlmostPrime holds for n precisely when bigOmega n equals 5. This theorem records the case n = 120, whose factorization yields exactly five prime factors counting multiplicity.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the boolean equality bigOmega 120 = 5.
why it matters
The declaration supplies a verified RS-relevant instance of a five-almost-prime. It populates the arithmetic functions layer that supports later Möbius inversion and prime-distribution work in the NumberTheory.Primes module. No downstream uses are recorded, leaving the result as a concrete data point for potential application in the phi-ladder or mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.