PrimeSum
plain-language theorem explainer
PrimeSum defines the sum over all primes p of p to the power minus sigma, serving as the real part of the prime zeta function in the Euler product instantiation of the Recognition Science cost structure. Researchers verifying carrier convergence for the conditional Riemann hypothesis would cite this definition when building the Hilbert-Schmidt norm of the prime operator. It is realized directly as an infinite sum over the set of primes.
Claim. Let $P(σ) = ∑_p p^{-σ}$ for real $σ$, where the sum runs over all prime numbers $p$.
background
The EulerInstantiation module embeds the classical Euler product for the zeta function into the Recognition Science carrier/sensor framework. PrimeSum(σ) is defined as the sum over primes of p^{-σ}, providing the real part of the prime zeta function. This serves as the starting point for the Hilbert-Schmidt norm squared (sum of p^{-2σ}) and the carrier log series in the module's core objects list.
proof idea
This is a direct definition realized as the infinite sum over the primes using the summation operator on Nat.Primes.
why it matters
This definition supplies the concrete prime sum that instantiates the abstract carrier in the Euler product chain. It enables the Hilbert-Schmidt convergence for σ > 1/2 and the subsequent verification that the determinant C(s) is holomorphic and nonvanishing on Re(s) > 1/2, supporting the conditional Riemann hypothesis through the cost-covering axiom. The module documentation positions it as the Layer 3 concrete object leading to the EulerCarrier interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.