universalCost
plain-language theorem explainer
The universal cost spectrum assigns to each finitely supported multiplicity function f on an abstract prime set P the real number obtained by summing multiplicity k times J of the norm of p. Researchers unifying cost spectra across classical primes and function fields cite this definition when abstracting constructions in the Selberg class. It is introduced directly as the Finsupp sum of multiplicity times the prime cost function.
Claim. $c(f) := ∑_p f(p) · J(‖p‖)$ for $f : P →₀ ℕ$, where $J$ denotes the cost function and $‖·‖$ the norm supplied by a PrimeNormStructure on the prime set $P$.
background
The module abstracts the prime cost spectrum to any norm-equipped prime structure. A PrimeNormStructure P supplies a type P of primes together with a real norm ‖p‖ > 1 on each prime; both ordinary primes in ℕ and monic irreducibles in 𝔽_q[T] are instances. The upstream definition primeJcost p is Jcost applied to PrimeNormStructure.norm p, where Jcost is the Recognition Science cost function J(x) = (x + x^{-1})/2 - 1. The universal cost spectrum is then the cost-weighted sum on the multiplicative monoid generated by P.
proof idea
Direct definition via Finsupp.sum using the term (k : ℝ) * primeJcost p. No tactics or lemmas are applied inside the definition itself; it simply delegates to the Finsupp sum operator and the already-defined primeJcost.
why it matters
This definition is the central object of the Universal Cost Spectrum module and feeds directly into the elementary properties proved downstream: additivity (universalCost_add), non-negativity (universalCost_nonneg), positivity (universalCost_pos), and the master certificate (universal_cost_certificate). It supports the Cost-Reciprocity synthesis paper by showing that all cost-spectrum constructions across the Selberg class arise from the same abstract framework. In the Recognition Science chain it instantiates the J-cost on the multiplicative monoid generated by primes, consistent with the forcing chain T5–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.