carrierDerivBound_finite
plain-language theorem explainer
The result shows that any real number σ₀ exceeding 1/2 is necessarily positive. Researchers instantiating the Recognition Science carrier via the Euler product of ζ(s) would cite this to anchor the half-plane domain for the logarithmic derivative. The proof is a one-line application of linear arithmetic on the reals.
Claim. If $σ_0 > 1/2$, then $σ_0 > 0$.
background
The Euler Product Instantiation module shows that the Euler product of ζ(s) instantiates the abstract RS carrier/sensor framework. Core objects include PrimeSum σ := ∑_p p^{−σ}, HilbertSchmidtNorm σ := ∑_p p^{−2σ}, carrierLogSeries σ := ∑_p [2 log(1−p^{−σ}) + 2p^{−σ}], and carrierDerivBound σ := 2∑_p (log p)·p^{−2σ}/(1−p^{−σ}). Key results establish Hilbert-Schmidt convergence, log C(s) convergence, nonvanishing of C(s), and the derivative bound on Re(s) > 1/2, enabling the cost-covering axiom and conditional RH.
proof idea
The proof is a one-line wrapper that applies the linarith tactic to the hypothesis 1/2 < σ₀.
why it matters
This step supports the carrier_deriv_finite claim within the Euler instantiation chain, which feeds the RegularCarrier interface and cost-covering axiom. It secures the positivity needed for the derivative bound to remain finite on σ₀ > 1/2, linking the prime zeta sums to the Recognition Science cost structure and the path toward conditional RH.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.