Primes
plain-language theorem explainer
Primes collects all prime natural numbers into a set. Researchers building Euler products for zeta within the RS cost and carrier framework cite it to define prime sums, Hilbert-Schmidt norms, and finite ledgers. The declaration is a direct set comprehension over the standard primality predicate.
Claim. $P := { n ∈ ℕ | n is prime }$, the set of all prime numbers.
background
The module instantiates the abstract RS carrier/sensor framework from AnnularCost and CostCoveringBridge via the Euler product for ζ(s). Core objects include PrimeSum σ := ∑_p p^{-σ} (prime zeta), HilbertSchmidtNorm σ := ∑_p p^{-2σ}, and carrierLogSeries. The local setting proceeds from primes to A(s) Hilbert-Schmidt, det₂(I−A(s)) convergent, C(s) holomorphic nonvanishing on Re(s)>1/2, and cost-covering axioms yielding conditional RH.
proof idea
Direct definition via set comprehension using the prime predicate alias from Primes.Basic.
why it matters
This set supplies the concrete support for Euler carriers and finite ledgers in ConcreteEulerLedger, prime gap category counts in GoldbachFromRS, and mock-order characterizations in RamanujanBridge.CongruenceQ3Bridge. It anchors the primes → A(s) → det₂ → C(s) chain that satisfies EulerCarrier and RegularCarrier interfaces, linking to the RS forcing chain and recognition equilibria at unit cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.