universalCost_smul_single
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not compute the cost for Finsupp with multiple distinct primes in the support.
- Does not prove non-negativity or positivity of the cost.
- Does not relate the abstract cost to specific physical constants or the phi-ladder.
- Does not establish uniqueness of the cost function among possible arithmetic functions.
formal statement (Lean)
151theorem universalCost_smul_single (n : ℕ) (p : P) :
152 universalCost (n • Finsupp.single p 1) = (n : ℝ) * primeJcost p := by
proof body
Term-mode proof.
153 rw [show n • Finsupp.single p (1 : ℕ) = Finsupp.single p n by
154 ext q; by_cases hpq : q = p
155 · subst hpq; simp
156 · simp [Finsupp.single_apply, hpq]]
157 exact universalCost_single p n
158
159/-! ## Universal certificate -/
160
161/-- Master certificate: the elementary properties of the universal
162 cost spectrum. -/