three_almost_prime_twentyseven
plain-language theorem explainer
27 equals 3 cubed and therefore satisfies the predicate that its total number of prime factors counted with multiplicity equals exactly three. Number theorists using arithmetic functions inside the Recognition Science framework would cite this as a verified concrete instance. The proof is a one-line wrapper that invokes native_decide to evaluate the boolean result of the bigOmega definition.
Claim. $Ω(27) = 3$, where $Ω(n)$ denotes 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 number is 3-almost prime precisely when bigOmega n equals 3, i.e., the sum of exponents in its prime factorization is three. The upstream definition isThreeAlmostPrime (n : ℕ) : Bool := bigOmega n = 3 supplies the predicate used here; the local setting keeps statements minimal pending deeper Dirichlet inversion.
proof idea
One-line wrapper that applies the native_decide tactic to evaluate the boolean equality directly from the bigOmega definition.
why it matters
This supplies a proved base-case verification inside the arithmetic-functions layer that supports Möbius footholds for later inversion work. It aligns with Recognition Science number-theory scaffolding that checks small cases on the phi-ladder before scaling to mass formulas or prime-related constants. No downstream theorems yet reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.