three_almost_prime_thirty
plain-language theorem explainer
Verification that 30 has exactly three prime factors counted with multiplicity confirms it meets the 3-almost-prime predicate. Number theorists referencing arithmetic functions in Recognition Science would cite this as a base case for small-integer checks. The proof is a one-line native_decide evaluation of the defining equality.
Claim. $30$ satisfies $Ω(30)=3$, where $Ω(n)$ is 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. A 3-almost prime is defined by the predicate isThreeAlmostPrime n := bigOmega n = 3, where bigOmega counts prime factors with multiplicity. This theorem checks the concrete case n=30, which factors as 2×3×5.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the boolean equality directly from the definition of bigOmega.
why it matters
This instance supports the arithmetic functions layer that builds Möbius footholds for Dirichlet algebra in the NumberTheory.Primes module. It supplies a verified base case aligned with Recognition Science number-theoretic predicates used in mass formulas and phi-ladder steps. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.