universalCost_single
The result states that the universal cost of a Finsupp supported at a single prime p with multiplicity k equals k times the J-cost of that prime. Workers on abstract cost spectra for multiplicative monoids or Selberg-class L-functions cite it to reduce general finite-support costs to prime contributions. The proof is a one-line term wrapper that unfolds the sum definition of universalCost and applies the Finsupp single-index simplification.
claimLet $P$ be a PrimeNormStructure with norm function $‖·‖ > 1$ on each prime. For any prime $p ∈ P$ and natural number $k$, the universal cost spectrum satisfies $c(f) = k · J(‖p‖)$, where $f$ is the finitely supported function that takes value $k$ at $p$ and $0$ elsewhere, and $J$ denotes the Recognition Science cost function.
background
The module UniversalCostSpectrum abstracts the prime cost spectrum to any type $P$ equipped with a PrimeNormStructure instance. This structure supplies a real norm $‖p‖ > 1$ for each prime; both ordinary primes in $ℕ$ and monic irreducibles over finite fields are instances. The auxiliary definition primeJcost p is then $J(‖p‖)$, where $J$ is the Recognition Science cost function. The main definition universalCost f for $f : P →₀ ℕ$ is the weighted sum $∑_p f(p) · primeJcost p$, which interprets $f$ as the multiplicity vector of an element in the multiplicative monoid generated by $P$.
proof idea
The proof is a one-line term wrapper. It unfolds the definition of universalCost, which expands to the Finsupp sum, then applies the simp lemma Finsupp.sum_single_index to reduce the sum over a single-support function to the explicit scalar multiple.
why it matters in Recognition Science
This theorem supplies one of the elementary properties listed in the module documentation and is invoked by the master certificate universal_cost_certificate, which bundles positivity, additivity, and the single-prime case. It also feeds the simp lemma universalCost_single_one and the scaling result universalCost_smul_single. Within the Recognition Science framework it realizes the cost-arithmetic function on the monoid generated by abstract primes, consistent with the universal cost spectrum construction that supports the Cost-Reciprocity synthesis paper.
scope and limits
- Does not assume any concrete value for the norm beyond $‖p‖ > 1$.
- Does not extend the cost function to infinite-support maps.
- Does not compute numerical values for specific classical primes.
- Does not address convergence questions for associated Dirichlet series.
Lean usage
rw [universalCost_single]formal statement (Lean)
104theorem universalCost_single (p : P) (k : ℕ) :
105 universalCost (Finsupp.single p k) = (k : ℝ) * primeJcost p := by
proof body
Term-mode proof.
106 unfold universalCost
107 simp [Finsupp.sum_single_index]
108