four_almost_prime_forty
plain-language theorem explainer
40 factors as 2 cubed times 5 and therefore carries exactly four prime factors counted with multiplicity. Number theorists building tables of small almost-primes for sieve or factorization arguments would cite the explicit check. The proof is a one-line native_decide that evaluates the boolean predicate directly on the concrete integer.
Claim. $40 = 2^3 5$ satisfies $Ω(40) = 4$, 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 isFourAlmostPrime n is defined by the equality bigOmega n = 4, where bigOmega implements the standard total prime-factor function Ω. This concrete verification belongs to a collection of small-integer checks that confirm the predicate behaves correctly before heavier Dirichlet or inversion machinery is layered on top.
proof idea
The proof is a one-line wrapper that applies native_decide to reduce the boolean equality isFourAlmostPrime 40 = true directly in the kernel.
why it matters
The declaration supplies an explicit base-case instance confirming that 40 lies in the 4-almost-prime class. It anchors the arithmetic-functions layer inside the NumberTheory.Primes development that later supports prime-counting and square-free arguments. No immediate downstream theorems are recorded, so the result functions as a verified data point rather than a lemma feeding a larger chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.