four_almost_prime_onehundred
plain-language theorem explainer
100 factors as 2² × 5² and therefore satisfies Ω(100) = 4. Number theorists checking concrete values of arithmetic functions would cite the result as an explicit instance. The proof is a one-line wrapper that applies native_decide to the definition of bigOmega.
Claim. The integer 100 satisfies Ω(100) = 4, where Ω counts all prime factors with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. A number is 4-almost prime precisely when its big-Omega value equals 4, as defined by isFourAlmostPrime n := bigOmega n = 4. This instance confirms the property for 100, which factors as 2 squared times 5 squared.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate isFourAlmostPrime 100 directly from the definition bigOmega 100 = 4.
why it matters
This theorem supplies a verified concrete case inside the arithmetic functions module that supports Möbius-based tools. It does not feed any downstream results. The declaration aligns with the number-theoretic foundations required for prime-related calculations in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.