primeJcost_nonneg
plain-language theorem explainer
Non-negativity of the J-cost on each abstract prime follows directly from its strict positivity. Researchers formalizing the universal cost spectrum in Recognition Science cite this when proving that the cost function c(f) is nonnegative on all finitely supported multiplicity vectors over the primes. The proof is a one-line wrapper that invokes the positivity result and applies le_of_lt.
Claim. For every prime $p$ in a PrimeNormStructure $P$, $0 ≤ J(‖p‖)$, where $J$ denotes the Recognition Science cost function and $‖p‖ > 1$ is the given norm.
background
The UniversalCostSpectrum module abstracts the prime cost spectrum to any PrimeNormStructure P, a typeclass supplying a type P of primes together with a real norm ‖p‖ > 1. The sibling definition primeJcost p is then J(‖p‖), the J-cost of that norm. The universal cost on a finitely supported multiplicity vector f : P →₀ ℕ is the weighted sum Σ_p f(p) · J(‖p‖). This construction recovers both the classical prime case (‖p‖ = p) and the monic-irreducible case over F_q[T]. Upstream results include the positivity theorem primeJcost_pos establishing 0 < primeJcost p, together with the cost definitions in CostAlgebra and ObserverForcing that guarantee J-costs are nonnegative.
proof idea
The proof is a one-line wrapper that applies the lemma primeJcost_pos p and then uses le_of_lt to obtain the non-strict inequality from strict positivity.
why it matters
This result is invoked directly by universalCost_nonneg and universalCost_pos, which establish that the universal cost c(f) satisfies 0 ≤ c(f) and 0 < c(f) whenever f ≠ 0. It supplies the elementary non-negativity step required for the cost spectrum to serve as a well-defined arithmetic function on the multiplicative monoid generated by P. In the Recognition Science framework it contributes to the universal cost arithmetic function that abstracts J-cost constructions across the Selberg class, consistent with the non-negativity of recognition costs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.