universalCost_zero
plain-language theorem explainer
The theorem states that the universal cost spectrum on the zero Finsupp vanishes for any PrimeNormStructure. Researchers abstracting cost functions across Selberg-class L-functions cite it as the zero-element base case before additivity and positivity. The proof is a one-line simp wrapper that unfolds the sum definition of universalCost.
Claim. $c(0) = 0$, where $c(f) := f.sum (fun p k => (k : ℝ) * J(‖p‖))$ for $f : P →₀ ℕ$ and $P$ any type equipped with a norm $‖·‖ > 1$.
background
The Universal Cost Spectrum module abstracts the prime cost framework to any PrimeNormStructure P, a typeclass supplying a real norm strictly greater than 1 on each prime. The universal cost is then the weighted sum $c(f) = Σ_p f(p) · J(‖p‖)$ over the finitely supported multiplicity function f. This construction supports the Cost-Reciprocity synthesis by treating classical primes and monic irreducibles in Fq[T] as instances of the same abstract arithmetic function.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definition of universalCost, reducing the claim directly to the sum over the empty support.
why it matters
universalCost_zero supplies the zero case inside the master certificate universal_cost_certificate, which bundles the elementary properties required by the Cost-Reciprocity paper. It sits at the base of the additive and positivity chain that lets the J-cost spectrum be transported across any norm-equipped prime structure, consistent with the Recognition Science J-function and forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.