universalCost_nonneg
plain-language theorem explainer
Universal cost non-negativity holds for every finitely supported multiplicity function over a prime norm structure. Researchers working on abstract Selberg-class cost spectra cite the result to confirm the spectrum defines a valid non-negative measure. The term proof reduces the defining sum to non-negative summands by invoking Finsupp sum non-negativity together with componentwise multiplication of a cast natural and a prime J-cost.
Claim. Let $P$ be a prime norm structure. For every finitely supported $f : P →_0 ℕ$, the universal cost $c(f) := ∑_p f(p) · J(‖p‖)$ satisfies $0 ≤ c(f)$.
background
The Universal Cost Spectrum module abstracts prime cost constructions to any PrimeNormStructure P, a type equipped with a norm ‖p‖ > 1. The definition universalCost f computes the sum of multiplicities times primeJcost p, where primeJcost p equals J of the norm. This setting unifies classical primes and monic irreducibles for the Cost-Reciprocity synthesis paper.
proof idea
The proof applies Finsupp.sum_nonneg to the sum in universalCost. Each summand is handled by mul_nonneg on the cast of the natural multiplicity (non-negative by zero_le) and primeJcost_nonneg p (itself from primeJcost_pos). The argument is therefore a direct reduction to the already-established non-negativity of individual J-costs.
why it matters
The theorem supplies the non-negativity clause inside the master certificate universal_cost_certificate, which bundles all elementary properties of the universal cost spectrum. It completes the verification that cost spectra remain non-negative measures, supporting the claim that every cost-spectrum construction across the Selberg class arises from this single abstract framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.