natPrimesInstance
plain-language theorem explainer
The declaration equips the set of natural-number primes with the PrimeNormStructure typeclass by defining the norm of each prime p as its integer value viewed in the reals. Researchers working on cost spectra or Selberg-class constructions would cite this instance to obtain the concrete case of the universal cost arithmetic function on classical primes. It is realized as a direct one-line assignment of the norm field, with the required norm-greater-than-one property following from the standard fact that every natural prime exceeds one.
Claim. The set of natural-number primes carries a PrimeNormStructure in which the norm of each prime $p$ equals its value as a real number.
background
A PrimeNormStructure on a type P consists of a real-valued norm function satisfying norm p > 1 for every p. This abstracts the notion of primes from integer primes to other structures such as monic irreducibles over finite fields. The module defines the universal cost on finitely supported functions f : P →₀ ℕ by summing f(p) · J(‖p‖), where J is the J-cost function. Upstream, the definition of Nat.Primes as the set of prime numbers in ℕ supplies the concrete type, and primeJcost computes J(norm p) for any such structure.
proof idea
The instance is a one-line definition that assigns the norm map to the coercion of the prime value into the reals. The accompanying norm_gt_one property is discharged by casting the known fact that every natural prime exceeds one.
why it matters
This instance instantiates the abstract PrimeNormStructure for classical primes, enabling the universalCost function and the bundled certificate theorem that collects the elementary properties of the cost spectrum. It supports the Cost-Reciprocity synthesis by providing the concrete case for integer primes within the single abstract framework. The construction ties directly to the Recognition Science forcing chain through the J-cost function appearing in the prime costs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.