three_almost_prime_eight
plain-language theorem explainer
The declaration records that 8 factors as 2 cubed and therefore meets the exact count of three prime factors with multiplicity. Number theorists populating small-integer tables for Recognition Science arithmetic functions would cite this check when verifying base cases ahead of Dirichlet inversion or mass-ladder constructions. The proof is a one-line native_decide evaluation of the defining equality bigOmega 8 = 3.
Claim. $Omega(8) = 3$, 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 isThreeAlmostPrime is introduced by the equation bigOmega n = 3. The upstream definition of bigOmega supplies the standard total-prime-factor count with multiplicity, so the present statement simply records that the integer 8 satisfies this count. The local theoretical setting remains the arithmetic-function layer that will later support Dirichlet inversion once the basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies native_decide to the Boolean equality isThreeAlmostPrime 8 = true. This tactic evaluates the definition bigOmega 8 = 3 by direct kernel computation of the prime factorization.
why it matters
This concrete instance populates the arithmetic-functions layer that supports later prime-counting and inversion arguments inside the Recognition Science number-theory stack. It supplies a verified data point for the 3-almost-prime classification that appears in mass-ladder constructions. No downstream theorems yet reference it, leaving open its eventual use in explicit phi-ladder formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.