three_almost_prime_fortytwo
plain-language theorem explainer
42 satisfies the 3-almost-prime condition because its factorization into three distinct primes gives bigOmega 42 equal to 3. Number theorists inside the Recognition Science arithmetic layer cite this concrete check when populating small cases for Möbius inversion or phi-ladder constructions. The proof is a one-line native decision that evaluates the predicate directly from its definition.
Claim. $42$ is 3-almost prime, i.e., the total number of prime factors counted with multiplicity satisfies $Ω(42)=3$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. A number $n$ is defined to be 3-almost prime precisely when bigOmega $n$ equals 3. This instance checks the concrete case $n=42=2·3·7$ whose prime factors are all distinct and total three in count.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the boolean equality isThreeAlmostPrime 42 directly from the upstream definition bigOmega n = 3.
why it matters
This verification populates the arithmetic-functions file that supports Möbius inversion and square-free checks inside the Recognition Science number-theory layer. It supplies a concrete foothold aligned with the T0-T8 forcing chain for later mass formulas on the phi-ladder. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.