PrimeNormStructure
plain-language theorem explainer
PrimeNormStructure equips any abstract type P of primes with a real-valued norm strictly larger than one on each element, permitting a uniform definition of the universal cost spectrum c(f) across integers and function fields. Number theorists working on cost spectra within the Selberg class would cite this interface to treat classical primes and monic irreducibles on equal footing. The declaration is a direct typeclass with two fields and no computational content.
Claim. A type $P$ carries a PrimeNormStructure when it is equipped with a function $||·||:P→ℝ$ such that $||p||>1$ for every $p∈P$.
background
The module UniversalCostSpectrum abstracts the prime cost spectrum to any norm-equipped prime structure. A PrimeNormStructure P consists of a type P together with a real norm strictly exceeding one; both ℕ primes (norm equal to the integer value) and monic irreducibles over finite fields (norm q^deg) become instances. The universal cost on a finitely supported function f:P→₀ℕ is then defined by c(f):=Σ_p f(p)·J(||p||), where J is the Recognition Science cost function J(x)=(x+x^{-1})/2-1 drawn from the PhiForcingDerived structure of J-cost and the MultiplicativeRecognizerL4 cost construction.
proof idea
The declaration is a direct typeclass definition specifying the norm map and the strict lower bound; no lemmas or tactics are applied.
why it matters
This interface supplies the common substrate for the universal cost spectrum used in the Cost-Reciprocity synthesis paper. It is instantiated by natPrimesInstance for natural-number primes and by funcFieldNormStructure for function-field primes, and it directly enables the downstream definitions primeJcost and the certificate universal_cost_certificate. The construction sits inside the Recognition Science forcing chain through the J-cost derived from ObserverForcing and PhiForcingDerived, supporting the claim that all cost spectra in the Selberg class arise from the same abstract arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.