four_almost_prime_onehundredtwentysix
plain-language theorem explainer
Verification that 126 satisfies the 4-almost-prime condition follows from its prime factorization 2 × 3² × 7 yielding Ω(126) = 4. Number theorists in the Recognition Science project cite such instances to validate the bigOmega implementation. Native decision procedures discharge the equality in a single step.
Claim. 126 is 4-almost prime, meaning Ω(126) = 4.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. The bigOmega function counts the total number of prime factors with multiplicity. The isFourAlmostPrime predicate holds precisely when this count equals 4.
proof idea
A term-mode proof applies native_decide directly to the goal after the definition of isFourAlmostPrime unfolds to bigOmega 126 = 4.
why it matters
The result provides a basic verified instance supporting arithmetic function usage in the NumberTheory.Primes section. It contributes to the foundation for more advanced Dirichlet algebra and inversion techniques mentioned in the module documentation. No immediate parent theorems depend on it, but it exemplifies the concrete checks needed for the Recognition Science number theory toolkit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.