PrimeSum
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish convergence of the sum for any value of σ.
- Does not extend the definition to complex σ.
- Does not reference the J-cost, phi-ladder, or forcing chain.
- Does not address the eight-tick octave or spatial dimension D=3.
formal statement (Lean)
60noncomputable def PrimeSum (σ : ℝ) : ℝ :=
proof body
Definition body.
61 ∑' (p : Nat.Primes), (p : ℝ) ^ (-σ)
62
63/-- The Hilbert–Schmidt norm squared of the prime operator A(s):
64 ‖A(s)‖₂² = ∑_p |p^{−s}|² = ∑_p p^{−2σ}.
65 This is the key convergence condition. -/