universalCost_single_one
plain-language theorem explainer
The theorem states that the universal cost of a single-prime Finsupp with multiplicity one equals the J-cost of that prime. Researchers abstracting cost spectra across number fields or function fields would cite it as the generator case for the additive cost function. The proof reduces directly to the general single-support formula and finishes with ring simplification.
Claim. For any prime $p$ in a PrimeNormStructure $P$, let $c(f)$ be the universal cost spectrum $c(f) = f.sum (k,p)mapsto k·J(‖p‖)$. Then $c(Finsupp.single p 1) = J(‖p‖)$.
background
The module abstracts the prime cost spectrum to any type $P$ equipped with a norm $‖p‖>1$ via the PrimeNormStructure typeclass. The universal cost is the function $c(f) := ∑_p f(p)·J(‖p‖)$ on finitely supported $f:P→₀ℕ$, where $J$ is the Recognition Science cost function. primeJcost p is defined as $J(‖p‖)$ and universalCost is the corresponding sum. The upstream universalCost_single theorem gives the general formula $c(Finsupp.single p k)=(k:ℝ)·primeJcost p$ for arbitrary multiplicity $k$.
proof idea
One-line wrapper that applies the general universalCost_single theorem and then invokes the ring tactic to specialize the coefficient from $k$ to 1.
why it matters
This supplies the base generator case for the cost spectrum on the free monoid generated by $P$. It feeds the additivity and positivity results (universalCost_add, universalCost_pos) that underwrite the Cost-Reciprocity synthesis paper. In the Recognition framework it instantiates the J-cost for abstract primes, consistent with J-uniqueness (T5) and the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.