Omega
plain-language theorem explainer
Omega defines the arithmetic function Ω(n) as the sum of all exponents in the prime factorization of n. Researchers deriving upper bounds on the cost spectrum c(n) or establishing additivity properties cite this when working with completely additive functions in the Recognition framework. The definition is realized as a direct one-line extraction from the exponents in the factorization map.
Claim. $Ω(n) := ∑ k$, where the sum runs over all exponents k appearing in the prime factorization of the natural number n.
background
The module extends the Recognition Science cost function J from positive reals to natural numbers by setting c(n) equal to the sum over each prime power p^k exactly dividing n of k · J(p). This construction yields a completely additive arithmetic function satisfying c(m n) = c(m) + c(n). Omega supplies the auxiliary sum of those exponents k, which enters bounds such as c(n) ≤ Ω(n) · J(n) for n ≥ 2.
proof idea
One-line definition that applies the sum operation directly to the range of the factorization map on n.
why it matters
Omega feeds the bound costSpectrumValue_le_omega_mul_jcost and the master certificate cost_spectrum_certificate. It supplies the multiplicity count needed to reformulate classical prime-counting functions inside the cost spectrum, supporting the lift of J-cost to arithmetic functions and downstream spectral-density constructions in gravity models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.