six_almost_prime_twohundredsixteen
plain-language theorem explainer
216 equals 2 cubed times 3 cubed and therefore has total prime factor count with multiplicity exactly six. Number theorists checking concrete instances of almost-prime counts inside the Recognition Science arithmetic functions library would cite this verification. The proof applies a native decision procedure that evaluates the big omega count by direct factorization.
Claim. $Ω(216) = 6$, 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 big omega function returns the total number of prime factors counted with multiplicity, and isSixAlmostPrime n holds precisely when this count equals six. The local setting keeps statements minimal so that deeper Dirichlet algebra can be added later once interfaces stabilize.
proof idea
This is a one-line term proof that invokes native_decide to compute the factorization 216 = 2³ × 3³ and confirm the multiplicity sum is six.
why it matters
The declaration supplies a concrete 6-almost-prime instance inside the NumberTheory.Primes.ArithmeticFunctions section. It fills a basic verification slot with no downstream uses recorded. The result sits alongside other small checks that support later work on prime factorization ladders without touching the forcing chain or physical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.