primeCost_nonneg
plain-language theorem explainer
For any positive integer n the prime cost, obtained by summing J-costs of its prime factors weighted by multiplicities, is nonnegative. Number theorists extending the Recognition Science cost spectrum to integers cite this to anchor nonnegativity of the arithmetic cost function. The proof is a one-line wrapper that unfolds the definition, casts n to a positive real, and invokes the Jcost nonnegativity lemma.
Claim. For every positive integer $n$, let $c(n) := 0$ when $n=1$ and $c(n) := 2^{-1} (n-1)^2 n^{-1}$ otherwise. Then $c(n) 0$.
background
The Prime Cost Spectrum module extends the J-cost from positive reals to natural numbers via prime factorization. For $n 1$ the cost is $c(n) := p v_p(n) J(p)$, rendering $c$ completely additive so that $c(m n) = c(m) + c(n)$ for positive $m,n$. This permits reformulation of Chebyshev and prime-counting functions in cost terms.
proof idea
Unfold primeCost to reach the underlying Jcost expression. Cast the hypothesis $0 < n$ to a positive real via exact_mod_cast. Apply the lemma Jcost_nonneg, which rewrites Jcost x as $(x-1)^2/(2x)$ and concludes nonnegativity by positivity of the square and the denominator.
why it matters
This result supplies the nonnegativity base for the cost spectrum theorems in the module, including costSpectrumValue_nonneg. It aligns with the nonnegativity of recognition-event costs in ObserverForcing and the derived cost in MultiplicativeRecognizerL4. The construction is consistent with the J-function nonnegativity that follows from the Recognition Composition Law and the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.