omega_twelve
plain-language theorem explainer
The theorem asserts that the distinct-prime-count function ω evaluates to 2 at the integer 12. Number theorists checking small cases in arithmetic identities or preparing Dirichlet-series arguments would cite this evaluation. The proof reduces the claim to a single native_decide call that computes the value directly from the imported definition.
Claim. The arithmetic function counting distinct prime factors satisfies $ω(12) = 2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The omega function denotes the count of distinct prime factors of a positive integer. No upstream lemmas are required; the result rests on the Basic and Squarefree imports together with Mathlib's native decidability for small integers.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the definition of omega at 12 and confirm equality with 2.
why it matters
This supplies a concrete base case inside the NumberTheory.Primes.ArithmeticFunctions hierarchy. It supports verification steps for sibling results such as mobius_prime and bigOmega_apply. No direct tie to the Recognition Science forcing chain or constants is present, leaving open later use in prime-ladder arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.