carrierDerivBound_pos
plain-language theorem explainer
The result establishes that the explicit bound on the logarithmic derivative of the Euler carrier remains strictly positive for all real σ₀ > 1/2. Analysts building zero-free criteria for the zeta function via the Euler product would cite it when populating the logDerivBound_pos field of a BudgetedCarrier. The argument isolates the positive term for the prime 2, verifies its sign by elementary inequalities on powers and logs, then invokes summability of the nonnegative series to conclude positivity of the full sum.
Claim. Let $M(σ₀) := 2 ∑_{p prime} (log p) ⋅ p^{-2σ₀} / (1 - p^{-σ₀})$. For every real $σ₀ > 1/2$, one has $M(σ₀) > 0$.
background
The module instantiates the abstract RS carrier/sensor framework by replacing the generic annular cost with the concrete Euler product for the reciprocal zeta function. Core objects include the prime zeta sum, the Hilbert-Schmidt norm squared of the associated operator, the carrier log series, and the carrier derivative bound $M(σ₀)$ defined above. The local setting is the three-layer chain: abstract cost axioms, conditional RH via cost-covering, and concrete Euler data satisfying the carrier interface on Re(s) > 1/2.
proof idea
The tactic proof first obtains σ₀ > 0 by linarith. It fixes the prime 2, unfolds the term, and confirms positivity of the power, the logarithm, and the denominator 1 - 2^{-σ₀} by rpow inequalities. It then applies the upstream lemma carrierDerivBound_summable together with carrierDerivTerm_nonneg to deduce that the tail sum is positive, and finally uses positivity on the unfolded definition of carrierDerivBound.
why it matters
The positivity supplies the logDerivBound_pos witness required by eulerBudgetedCarrier and by the three zeroFreeCriterion_of_* bridges in AnalyticTrace. Those bridges in turn feed the ZeroFreeCriterion interface used for conditional RH. The declaration therefore closes the concrete-to-abstract link in the Euler instantiation chain, directly supporting the cost-covering axiom that yields the zero-free region.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.