universal_cost_certificate
The universal cost certificate bundles the six elementary arithmetic properties of the cost function c(f) = sum f(p) J(norm p) over any prime norm structure P: strict positivity on primes, vanishing at zero support, additivity, singleton evaluation, non-negativity, and strict positivity on nonzero supports. Researchers on the Cost-Reciprocity synthesis paper cite it for the complete elementary arithmetic of the abstract cost spectrum. The proof is a term that packages the six component lemmas establishing each property separately.
claimLet $P$ carry a prime norm structure with real norm greater than 1 on each prime. The universal cost $c$ on finitely supported functions $f : P →₀ ℕ$ satisfies: $0 < J(‖p‖)$ for every prime $p$; $c(0) = 0$; $c(f + g) = c(f) + c(g)$ for all such $f, g$; $c$ of the singleton with multiplicity $k$ at $p$ equals $k · J(‖p‖)$; $c(f) ≥ 0$ for every $f$; and $c(f) > 0$ whenever $f ≠ 0$.
background
The module abstracts the prime cost spectrum framework to any PrimeNormStructure P, consisting of a type of primes equipped with a real-valued norm strictly greater than 1. The universal cost is then defined by summing f(p) times J of the norm of p over the support of any finitely supported function f from P to the naturals. This supplies the arithmetic foundation for the Cost-Reciprocity synthesis paper, which treats all cost-spectrum constructions across the Selberg class as instances of the same abstract setup.
proof idea
The proof is a term-mode package that directly assembles the six component lemmas: primeJcost positivity, the zero value at the empty support, additivity under support addition, the singleton evaluation formula, non-negativity of the sum, and strict positivity on nonzero supports.
why it matters in Recognition Science
This declaration collects the main theorems of the module and supplies the bundled certificate referenced in the Cost-Reciprocity synthesis paper. It rests on the J-cost definition from the recognition forcing chain and provides the elementary arithmetic that lets every concrete cost spectrum be viewed as an instance of the same structure. No scaffolding or open questions remain, since every component is fully proved with zero sorry.
scope and limits
- Does not derive the explicit functional form of J.
- Does not instantiate the structure for classical primes or polynomial rings.
- Does not address analytic continuation or L-function properties.
- Does not connect to mass ladders or physical constants.
formal statement (Lean)
163theorem universal_cost_certificate :
164 -- (1) Every prime cost is strictly positive.
165 (∀ (p : P), 0 < primeJcost p) ∧
166 -- (2) Cost is zero at the trivial Finsupp (the unit element).
167 (universalCost (0 : P →₀ ℕ) = 0) ∧
168 -- (3) Cost is additive.
169 (∀ (f g : P →₀ ℕ),
170 universalCost (f + g) = universalCost f + universalCost g) ∧
171 -- (4) Cost on a singleton: c(single p k) = k · J(‖p‖).
172 (∀ (p : P) (k : ℕ),
173 universalCost (Finsupp.single p k) = (k : ℝ) * primeJcost p) ∧
174 -- (5) Cost is nonneg.
175 (∀ (f : P →₀ ℕ), 0 ≤ universalCost f) ∧
176 -- (6) Cost is strictly positive on non-trivial Finsupps.
177 (∀ {f : P →₀ ℕ}, f ≠ 0 → 0 < universalCost f) :=
proof body
Term-mode proof.
178 ⟨primeJcost_pos,
179 universalCost_zero,
180 universalCost_add,
181 universalCost_single,
182 universalCost_nonneg,
183 @universalCost_pos P _ _⟩
184
185/-! ## Instance: Integer primes -/
186