carrierDerivTerm_nonneg
plain-language theorem explainer
The result shows that for real part σ₀ exceeding 1/2 and any prime p the per-prime contribution to the logarithmic derivative of the Euler carrier remains nonnegative. Workers deriving the carrier derivative bound in the Euler instantiation of the RS cost structure cite it to confirm the series terms stay well-behaved before summing. The argument unfolds the explicit term and verifies positivity of each factor via real-analysis facts on exponents and logarithms.
Claim. For real number σ₀ > 1/2 and prime p, the quantity p^{-2σ₀} (log p) / (1 - p^{-σ₀}) is nonnegative.
background
The EulerInstantiation module embeds the classical Euler product for ζ(s) into the abstract RS carrier/sensor framework supplied by AnnularCost and CostCoveringBridge. Core objects include the per-prime term carrierDerivTerm p σ = p^{-2σ} log p / (1 - p^{-σ}) whose sum (scaled by 2) yields the carrier logarithmic derivative bound carrierDerivBound σ₀. This bound appears in the layer that produces a holomorphic nonvanishing C(s) on Re(s) > 1/2, satisfying the EulerCarrier interface and opening the cost-covering axiom route to conditional RH.
proof idea
The tactic proof first unfolds carrierDerivTerm. It then obtains σ₀ > 0 by linarith, p^{-2σ₀} > 0 by Real.rpow_pos_of_pos, log p > 0 by Real.log_pos after casting p > 1, and the denominator positive by invoking eigenvalue_lt_one together with linarith. The final positivity tactic assembles these facts into the required inequality.
why it matters
The lemma supplies the nonnegativity ingredient for the downstream theorems carrierDerivBound_pos and carrierDerivBound_summable. It therefore completes the concrete step in the module's instantiation chain that produces a finite logarithmic derivative bound, allowing the Euler product to satisfy the RegularCarrier interface and feed the cost-covering axiom. Within the Recognition Science framework this advances the carrier layer that links the Euler product to the forcing chain and the conditional Riemann hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.