bigOmega_eight
plain-language theorem explainer
The theorem records that the arithmetic function counting prime factors with multiplicity evaluates to exactly 3 at the integer 8. Number theorists checking concrete instances of Omega in factorization tables would cite this evaluation. The proof is a direct native decision that reduces the claim to the definition of bigOmega as cardFactors.
Claim. $Omega(8) = 3$, 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 related counting functions. bigOmega is introduced as the arithmetic function that returns the number of prime factors counted with multiplicity, implemented via ArithmeticFunction.cardFactors. The local setting keeps statements minimal so that Dirichlet inversion and related algebra can be added once the basic interfaces are stable.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the arithmetic function definition directly on the concrete input 8.
why it matters
This supplies a verified small case for the bigOmega function inside the primes arithmetic-functions module. It supports later constructions that rely on explicit prime-factor counts, although no immediate dependents appear in the current graph. The result sits in the number-theoretic layer that Recognition Science uses to handle discrete structures before lifting to the forcing chain and J-cost relations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.