natPrimesInstance
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove any new arithmetic properties of primes beyond the norm assignment.
- Does not extend to other number fields or function fields without additional instances.
- Does not address convergence of associated L-functions or Dirichlet series.
formal statement (Lean)
187instance natPrimesInstance : PrimeNormStructure Nat.Primes where
188 norm := fun p => (p.val : ℝ)
proof body
Definition body.
189 norm_gt_one := fun p => by exact_mod_cast p.prop.one_lt
190
191example (p : Nat.Primes) : 0 < primeJcost p := primeJcost_pos p
192
193/-! ## Function-field instance (parameterized) -/
194
195/-- The function-field prime norm structure: monic irreducible polynomials
196 in `F[X]` with norm `q^deg P` where `q = Fintype.card F`. Parameterized
197 by the field `F` (so it cannot be a global instance). -/