primeJcost
plain-language theorem explainer
primeJcost assigns to each abstract prime p the real value J applied to its norm under any PrimeNormStructure. Researchers building cost spectra over generalized primes or synthesizing L-function costs cite this definition as the atomic building block. It is a direct one-line definition that extracts the norm from the typeclass and feeds it to Jcost.
Claim. For a type $P$ equipped with a PrimeNormStructure (a norm function satisfying $1 < ||p||$ for all $p$), the cost of an abstract prime is defined by $J(||p||)$, where $J$ denotes the J-cost function from the Recognition framework.
background
PrimeNormStructure is the typeclass that equips an arbitrary type P with a real-valued norm obeying norm p > 1 for every element p; this abstracts both ordinary integer primes and monic irreducibles in F_q[T]. Jcost itself is the cost function induced by a multiplicative recognizer or observer forcing event, satisfying Jcost(x) > 0 whenever x ≠ 1 (see upstream results such as Jcost_pos_of_ne_one and derivedCost). The module UniversalCostSpectrum lifts the classical prime-cost construction to this abstract setting so that the universal cost c(f) = Σ_p f(p) · J(||p||) can be defined uniformly on finitely supported multiplicity functions f : P →₀ ℕ.
proof idea
This is a one-line definition that applies the Jcost function directly to the norm field supplied by the PrimeNormStructure typeclass instance.
why it matters
primeJcost supplies the atomic term that universalCost sums over Finsupp supports, enabling the master certificate universal_cost_certificate and the positivity and additivity theorems that follow. It instantiates the J-cost landmark of the Recognition forcing chain (T5) inside the cost-spectrum synthesis, allowing the same arithmetic to cover both classical primes and polynomial irreducibles while preserving the RCL identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.