three_almost_prime_fortytwo
plain-language theorem explainer
The statement records that 42 factors as 2·3·7 and therefore satisfies Ω(42)=3. Number theorists checking small cases inside the Recognition Science arithmetic layer would cite the result when validating the isThreeAlmostPrime predicate. The proof is a one-line native_decide term that evaluates the Boolean definition directly.
Claim. $Ω(42)=3$, where $Ω(n)$ counts the prime factors of $n$ with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The predicate isThreeAlmostPrime is defined by the equality bigOmega n = 3, where bigOmega implements the total prime-factor count Ω. The local setting is therefore a collection of small verification lemmas that stabilize the arithmetic interface before deeper Dirichlet or inversion results are added.
proof idea
The proof is a term-mode native_decide that reduces the Boolean expression obtained from the definition of isThreeAlmostPrime to a direct evaluation.
why it matters
The declaration supplies a concrete verification point for the arithmetic-functions interface in the NumberTheory.Primes layer. It supports later Recognition Science constructions that rely on exact integer checks, although no downstream use is recorded in the current graph. The result aligns with the framework's need for verified small cases when building toward the phi-ladder and mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.