four_almost_prime_sixteen
plain-language theorem explainer
The declaration verifies that 16 equals 2 to the fourth power and therefore satisfies the 4-almost-prime condition via the bigOmega count of prime factors with multiplicity. Number theorists maintaining arithmetic-function interfaces or checking base cases in the Recognition Science primes layer would reference this fact. The proof reduces to a single native_decide evaluation of the constant.
Claim. $16 = 2^4$ and therefore satisfies the 4-almost-prime condition, i.e., the total number of prime factors counted with multiplicity equals 4.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to bigOmega. The sibling definition states that a natural number n is 4-almost prime precisely when bigOmega n equals 4. This sits inside the NumberTheory.Primes section, which stabilizes basic interfaces before deeper Dirichlet algebra is added.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate bigOmega 16 directly against the constant 4.
why it matters
This supplies a concrete base-case check for the 4-almost-prime predicate inside the arithmetic-functions module. It supports the primes toolkit that may later feed Möbius inversions or factorization arguments, though no downstream uses are recorded. The result aligns with the module's stated goal of keeping statements lightweight while the interfaces stabilize.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.