six_almost_prime_fourhundredsixteen
plain-language theorem explainer
416 factors as 2^5 times 13 and therefore satisfies Omega(416) = 6. Number theorists checking concrete almost-prime examples would reference this instance when testing bounds or generating test cases. The proof is a single native_decide call that evaluates the bigOmega definition on the literal input.
Claim. $416 = 2^5 · 13$ and therefore satisfies $Ω(416) = 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 and extending to bigOmega. A number is 6-almost prime precisely when bigOmega n equals 6, as defined by isSixAlmostPrime. The upstream result isSixAlmostPrime supplies the Boolean predicate bigOmega n = 6 that the present theorem evaluates at n = 416.
proof idea
The proof is a one-line wrapper that applies native_decide to compute the Boolean expression isSixAlmostPrime 416 directly from the definition bigOmega 416 = 6.
why it matters
This supplies a verified concrete example inside the arithmetic-functions library of the NumberTheory.Primes module. No downstream theorem depends on it, and the declaration does not engage the Recognition Science forcing chain, RCL identity, or phi-ladder mass formulas. It remains peripheral scaffolding for prime-related bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.