universalCost_smul_single
plain-language theorem explainer
Scaling a single-prime Finsupp by natural number n multiplies its universal cost exactly by n. Researchers on abstract cost spectra or the Cost-Reciprocity synthesis would cite this when reducing multiples of prime elements to the base case. The proof rewrites the scalar multiplication on Finsupp via extensionality and case split, then applies the single-support theorem.
Claim. For any natural number $n$ and prime $p$ in a PrimeNormStructure $P$, the universal cost satisfies $c(n · δ_p) = n · J(‖p‖)$, where $c(f) = ∑_p f(p) · J(‖p‖)$ and $δ_p$ denotes the Finsupp single at $p$.
background
The module abstracts the prime cost spectrum to any PrimeNormStructure P: a type of primes equipped with a real norm ‖p‖ > 1. The universal cost is defined by c(f) := Σ_p f(p) · J(‖p‖) on finitely supported f : P →₀ ℕ. primeJcost p is the abbreviation for J(‖p‖). This setting draws on the J-cost structures from PhiForcingDerived and ObserverForcing, where cost is the derived cost of a recognition event or multiplicative comparator.
proof idea
The proof is a one-line wrapper. It rewrites n • Finsupp.single p 1 to Finsupp.single p n by extensionality: for each q it cases on q = p, substitutes and simplifies the single_apply values. It then applies the sibling theorem universalCost_single p n.
why it matters
The declaration completes the elementary scaling property inside the universal cost spectrum, feeding the master certificate universal_cost_certificate listed in the module doc. It supports the claim that all Selberg-class cost spectra arise from the same abstract framework. In Recognition Science terms it aligns with the J-cost being linear on the multiplicative monoid generated by primes, consistent with the forcing chain and RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.