omega_eight
plain-language theorem explainer
The theorem asserts that the distinct prime factor counting function omega evaluates to 1 at the input 8. Number theorists using the Recognition Science arithmetic wrappers cite it as a verified base case for powers of the smallest prime. The proof is a one-line wrapper that applies native_decide to evaluate the definition directly.
Claim. $ω(8) = 1$, where $ω(n)$ denotes the number of distinct prime factors of the positive integer $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. It defines omega and bigOmega to track the count of distinct prime factors and the total number of prime factors counted with multiplicity. The upstream theorem and from CirclePhaseLift supplies an explicit log-derivative bound M on the disk, making the angular Lipschitz constant logDerivBound = M * r a concrete value for downstream circle-phase arguments.
proof idea
The proof is a one-line wrapper that applies native_decide to compute the value of omega 8 from its definition as the cardinality of the prime divisors of 8.
why it matters
This supplies a verified base case for the omega function on 2^3 inside the NumberTheory.Primes.ArithmeticFunctions module. It supports later arithmetic calculations that rely on small integer checks for prime-related properties, consistent with the framework's use of explicit evaluations before layering Dirichlet inversion or Möbius relations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.