universal_cost_certificate
plain-language theorem explainer
The universal cost certificate bundles the six elementary arithmetic properties of the cost function c(f) = sum f(p) J(norm p) over any prime norm structure P: strict positivity on primes, vanishing at zero support, additivity, singleton evaluation, non-negativity, and strict positivity on nonzero supports. Researchers on the Cost-Reciprocity synthesis paper cite it for the complete elementary arithmetic of the abstract cost spectrum. The proof is a term that packages the six component lemmas establishing each property separately.
Claim. Let $P$ carry a prime norm structure with real norm greater than 1 on each prime. The universal cost $c$ on finitely supported functions $f : P →₀ ℕ$ satisfies: $0 < J(‖p‖)$ for every prime $p$; $c(0) = 0$; $c(f + g) = c(f) + c(g)$ for all such $f, g$; $c$ of the singleton with multiplicity $k$ at $p$ equals $k · J(‖p‖)$; $c(f) ≥ 0$ for every $f$; and $c(f) > 0$ whenever $f ≠ 0$.
background
The module abstracts the prime cost spectrum framework to any PrimeNormStructure P, consisting of a type of primes equipped with a real-valued norm strictly greater than 1. The universal cost is then defined by summing f(p) times J of the norm of p over the support of any finitely supported function f from P to the naturals. This supplies the arithmetic foundation for the Cost-Reciprocity synthesis paper, which treats all cost-spectrum constructions across the Selberg class as instances of the same abstract setup.
proof idea
The proof is a term-mode package that directly assembles the six component lemmas: primeJcost positivity, the zero value at the empty support, additivity under support addition, the singleton evaluation formula, non-negativity of the sum, and strict positivity on nonzero supports.
why it matters
This declaration collects the main theorems of the module and supplies the bundled certificate referenced in the Cost-Reciprocity synthesis paper. It rests on the J-cost definition from the recognition forcing chain and provides the elementary arithmetic that lets every concrete cost spectrum be viewed as an instance of the same structure. No scaffolding or open questions remain, since every component is fully proved with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.