six_almost_prime_ninetysix
plain-language theorem explainer
96 factors as 2^5 times 3, yielding exactly six prime factors counted with multiplicity and therefore satisfying the 6-almost-prime predicate. Number theorists consulting the Recognition Science arithmetic-function library would cite the result for explicit small-integer checks. The proof is a direct native computation of the underlying bigOmega definition.
Claim. $96 = 2^5 3$ and therefore $Omega(96) = 6$, where $Omega(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 and extending to bigOmega. A number is declared 6-almost prime precisely when bigOmega n equals 6. The local setting is therefore a collection of small, computable predicates on natural numbers that can later support Dirichlet inversion or prime-counting arguments.
proof idea
The proof is a one-line wrapper that applies native_decide to the definition isSixAlmostPrime n := bigOmega n = 6 evaluated at n = 96.
why it matters
The declaration supplies a concrete, fully proved instance inside the NumberTheory.Primes.ArithmeticFunctions module. It supports downstream use of the 6-almost-prime predicate without introducing new hypotheses or open scaffolding. No direct connection to the T0-T8 forcing chain or Recognition Composition Law appears in the surrounding results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.