hilbert_schmidt_convergent
plain-language theorem explainer
The theorem proves convergence of the sum over primes p of p^{-2σ} for real σ > 1/2. Researchers instantiating the Euler product inside the Recognition Science carrier framework cite it to confirm that the Hilbert-Schmidt norm of the operator A(s) remains finite on the half-plane Re(s) > 1/2. The proof is a one-line wrapper that invokes the known summability of the prime zeta function once the hypothesis forces the exponent above 1.
Claim. For every real number σ satisfying σ > 1/2, the series ∑_{p prime} p^{-2σ} converges.
background
The EulerInstantiation module embeds the classical Euler product for ζ(s) into the abstract RS carrier/sensor framework defined in AnnularCost and CostCoveringBridge. Core objects include PrimeSum σ := ∑_p p^{-σ} and HilbertSchmidtNorm σ := ∑_p p^{-2σ}, the squared Hilbert-Schmidt norm of the carrier operator A(s). The local setting requires these sums to converge so that the regularized determinant det₂(I - A(s)) is holomorphic and non-vanishing for Re(s) > 1/2, enabling the cost-covering axiom and a conditional Riemann hypothesis.
proof idea
The proof is a one-line wrapper that applies Nat.Primes.summable_rpow. The hypothesis 1/2 < σ immediately yields 2σ > 1 by linarith, so the known summability of ∑_p p^{-r} for r > 1 supplies the result.
why it matters
This is the opening link in the instantiation chain primes → A(s) Hilbert-Schmidt → det₂ convergent. It is invoked by det2_log_summable to obtain absolute convergence of the logarithmic factors. In the Recognition Science framework it supplies the finiteness needed for the Euler carrier to satisfy the RegularCarrier interface on Re(s) > 1/2, closing the path from the abstract cost-covering axiom to the conditional Riemann hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.