eulerRegularCarrier
plain-language theorem explainer
The definition constructs a RegularCarrier instance for the Euler product of the zeta function at any real number greater than one half. Number theorists working on conditional proofs of the Riemann hypothesis via Recognition Science cost-covering axioms would cite this construction. It assembles the structure by setting the logarithmic derivative bound to the explicit prime sum and the radius to the distance to the critical line.
Claim. For any real number $σ_0 > 1/2$, the Euler product defines a regular carrier whose logarithmic derivative is bounded by the sum over primes of $2 (log p) p^{-2σ_0}/(1 - p^{-σ_0})$ and whose radius equals $σ_0 - 1/2$.
background
The module demonstrates that the Euler product for the Riemann zeta function realizes the abstract carrier framework from AnnularCost and CostCoveringBridge. Core objects are the prime sum as the sum over primes of $p^{-σ}$, the Hilbert-Schmidt norm squared as the sum of $p^{-2σ}$, the carrier log series, and the carrier derivative bound as twice the sum of $(log p) p^{-2σ}/(1 - p^{-σ})$.
proof idea
The definition populates the regular carrier record by assigning the logarithmic derivative bound to the prime-sum derivative expression at the input point, its positivity to the corresponding positivity result, the radius to the input real part minus one half, and proving the radius positivity by linear arithmetic.
why it matters
This supplies the concrete carrier for the theorem that the regular carrier covers the strip, the certificate constructor, and the sensor carrier compatibility theorem. It completes the instantiation chain from primes through Hilbert-Schmidt convergence to a regular carrier on disks centered above the critical line, enabling the cost-covering axiom for a conditional Riemann hypothesis. It addresses the bridge from analytic number theory to the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.