carrierDerivBound
plain-language theorem explainer
The carrier logarithmic derivative bound defines M_C(σ₀) explicitly as twice the sum over primes of (log p) p^{-2σ₀} / (1 - p^{-σ₀}). Analysts working on the Riemann hypothesis via Euler-product carriers in the Recognition Science cost framework cite this as the concrete bound on |C'/C| for the derived carrier function. The definition is a direct one-line unfolding of the sum of per-prime derivative terms.
Claim. $M_C(σ_0) := 2 ∑_{p prime} (log p) · p^{-2σ_0} / (1 - p^{-σ_0})$
background
This module instantiates the abstract RS carrier/sensor framework from AnnularCost and CostCoveringBridge using the Euler product of ζ(s). Core objects include the prime zeta PrimeSum σ := ∑_p p^{-σ}, the Hilbert-Schmidt norm squared HilbertSchmidtNorm σ := ∑_p p^{-2σ}, the carrier log series carrierLogSeries σ := ∑_p [2 log(1-p^{-σ}) + 2p^{-σ}], and the derivative bound defined here. The local setting layers an abstract cost framework through a carrier axiom to a conditional RH, with the Euler product supplying a concrete C(s) = det₂² that is holomorphic and nonvanishing for Re(s) > 1/2.
proof idea
One-line definition that unfolds carrierDerivBound σ₀ directly to twice the sum over Nat.Primes of the per-prime term carrierDerivTerm p σ₀.
why it matters
It supplies the explicit logDerivBound value used in eulerCarrierInstance to satisfy the EulerCarrier interface and in ZeroFreeCriterion to witness logDeriv_bounded_on_strip. This completes the carrier_deriv_finite step in the module's instantiation chain, allowing the cost-covering axiom to apply and yielding conditional RH from the Euler product. It sits inside the Recognition Science architecture that derives analytic estimates from the prime factorization of the carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.