bigOmega_one
Ω(1) evaluates to zero under the total prime factor count with multiplicity. Number theorists working with arithmetic functions cite this as the base case for Ω on the unit. The proof reduces immediately via simplification on the apply lemma for the definition.
claim$Ω(1) = 0$, where $Ω(n)$ denotes the total number of prime factors of $n$ counted with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function and extending to Ω. bigOmega is the abbreviation for the arithmetic function that counts prime factors with multiplicity. The upstream lemma bigOmega_apply states that Ω(n) equals the length of the list of prime factors of n.
proof idea
The proof is a one-line wrapper that applies bigOmega_apply to the case n=1.
why it matters in Recognition Science
This base case anchors the arithmetic functions module for primes, which supports number-theoretic scaffolding in the Recognition framework. It aligns with the self-reference structures from UniversalForcingSelfReference by supplying a concrete evaluation at the unit. No direct downstream uses are recorded.
scope and limits
- Does not extend the evaluation to any n greater than 1.
- Does not relate Ω to the Möbius function or other arithmetic functions.
- Does not address prime powers or composite numbers explicitly.
formal statement (Lean)
438theorem bigOmega_one : bigOmega 1 = 0 := by
proof body
Term-mode proof.
439 simp [bigOmega_apply]
440
441/-- σ_k(1) = 1 for any k. -/