universalCost_single
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.