universalCost_add
plain-language theorem explainer
Additivity holds for the universal cost spectrum on finitely supported multiplicity vectors over any PrimeNormStructure. Number theorists working on abstract cost functions for L-functions would cite this when establishing the elementary arithmetic properties. The proof unfolds the definition and applies Finsupp sum additivity via a direct rewrite.
Claim. Let $P$ carry a PrimeNormStructure. For $f,g:P\to_0\mathbb{N}$, the universal cost $c(f)=\sum_p f(p)\cdot J(\|p\|)$ satisfies $c(f+g)=c(f)+c(g)$.
background
The module abstracts prime cost spectra to any PrimeNormStructure $P$, a type equipped with a norm $|p|>1$. The function universalCost is the sum $f.\text{sum}(\lambda p,k,\Rightarrow,(k:\mathbb{R})\cdot\text{primeJcost }p)$, where primeJcost $p=J(|p|)$. This setting supports the Cost-Reciprocity synthesis paper by treating all such spectra as instances of one framework. The sole upstream dependency is the definition of universalCost.
proof idea
The proof unfolds universalCost, rewrites via Finsupp.sum_add_index', simplifies the first case with simp, and reduces the second case to ring after push_cast.
why it matters
The result is invoked inside universal_cost_certificate, the master certificate that bundles all elementary properties of the cost spectrum. It supplies the additivity clause listed among the main theorems in the module documentation, enabling the uniform treatment of cost spectra across Selberg-class constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.