universalCost_add
The universal cost spectrum is additive: the cost of the sum of two multiplicity vectors on the abstract primes equals the sum of their individual costs. Researchers abstracting cost functions across the Selberg class cite this to confirm the cost map is a monoid homomorphism from Finsupp to the reals. The proof is a direct unfolding of the sum definition followed by the Finsupp sum-additivity lemma and coefficient ring arithmetic.
claimLet $P$ carry a PrimeNormStructure. For any finitely supported $f, g : P →_0 ℕ$, the universal cost satisfies $c(f + g) = c(f) + c(g)$, where $c(h) := ∑_p h(p) · J(‖p‖)$ and $J$ denotes the J-cost function.
background
The module abstracts the prime cost spectrum from earlier PrimeCostSpectrum files to any PrimeNormStructure P, a typeclass supplying a real norm ‖p‖ > 1 on each prime p. The universal cost on a finitely supported multiplicity vector f : P →₀ ℕ is the weighted sum Σ_p f(p) · J(‖p‖), with J the J-cost appearing throughout the Recognition framework. This construction covers both classical primes (‖p‖ = p) and monic irreducibles in F_q[T] (‖P‖ = q^deg P), as stated in the module documentation.
proof idea
The proof unfolds the definition of universalCost to expose the Finsupp.sum. It rewrites via Finsupp.sum_add_index', which distributes the sum over pointwise addition of the two maps. The first subgoal is closed by simp; the second is closed by push_cast followed by ring to verify the coefficient identity.
why it matters in Recognition Science
This theorem is invoked by the master certificate universal_cost_certificate, which packages all elementary properties of the cost spectrum to support the Cost-Reciprocity synthesis paper. It supplies the additivity step required to treat the cost map as a monoid homomorphism, a prerequisite for showing that cost-spectrum constructions across the Selberg class are instances of one abstract framework. The result therefore closes one of the elementary properties listed in the module documentation.
scope and limits
- Does not assume any concrete form for the norm beyond the PrimeNormStructure axioms.
- Does not address multiplicativity or other operations on the monoid.
- Does not extend to functions with infinite support.
- Does not compute numerical values for specific primes or norms.
Lean usage
example (f g : P →₀ ℕ) : universalCost (f + g) = universalCost f + universalCost g := universalCost_add f gformal statement (Lean)
114theorem universalCost_add (f g : P →₀ ℕ) :
115 universalCost (f + g) = universalCost f + universalCost g := by
proof body
Term-mode proof.
116 unfold universalCost
117 rw [Finsupp.sum_add_index']
118 · intro p; simp
119 · intro p i j; push_cast; ring
120