costSpectrumValue_le_omega_mul_jcost
plain-language theorem explainer
The cost spectrum value c(n) for integers n ≥ 2 satisfies c(n) ≤ Ω(n) · J(n), where c(n) sums k · J(p) over the prime factorization of n and Ω(n) counts those factors with multiplicity. Number theorists deriving asymptotic upper bounds on additive arithmetic functions in Recognition Science would cite this inequality. The proof bounds each summand via monotonicity of J on [1, ∞) then applies the finite sum inequality.
Claim. For every integer $n ≥ 2$, let $c(n)$ be the cost spectrum value $∑ k · J(p)$ summed over the prime factorization of $n$. Then $c(n) ≤ Ω(n) · J(n)$, where $Ω(n)$ is the total number of prime factors counted with multiplicity.
background
This module extends the Recognition Science cost function J from positive reals to natural numbers via prime factorization. The cost spectrum value c(n) is defined as the sum over each prime power p^k dividing n of k times J(p), yielding a completely additive arithmetic function. Omega(n) is the sum of the exponents in that factorization, i.e., the total prime factor count with multiplicity.
proof idea
The proof first obtains n > 0 and 1 ≤ n in reals. For each prime p in the factorization support it verifies p ≤ n, applies the monotonicity lemma jcost_strictMono_on_one_le to get J(p) ≤ J(n), and multiplies by the nonnegative exponent. It rewrites the target right-hand side as the sum of k · J(n) using the definition of Omega and Finsupp sum properties, then invokes Finset.sum_le_sum on the per-summand bounds.
why it matters
This inequality feeds the master certificate theorem cost_spectrum_certificate that collects the elementary properties of the cost spectrum for the companion paper. It supplies a concrete upper bound for asymptotic work on the arithmetic extension of J. The argument rests on the monotonicity of J on [1, ∞), a property that traces back to the forcing chain T5–T6 and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.