carrierDerivTerm
plain-language theorem explainer
The per-prime term in the carrier logarithmic derivative bound is defined by the explicit real expression p to the power of minus two sigma times log p over one minus p to the power of minus sigma. Analysts establishing finite bounds on the logarithmic derivative of the determinant factor within the Euler product instantiation of the RS cost structure cite this term when proving summability and positivity for sigma greater than one half. The definition is a direct algebraic expression with no auxiliary lemmas.
Claim. For prime $p$ and real $σ$, the per-prime contribution to the logarithmic derivative of the determinant factor is $p^{-2σ} · (log p) / (1 - p^{-σ})$. This supplies each summand in the bound $M_C(σ_0) = 2 ∑_p (log p) · p^{-2σ_0} / (1 - p^{-σ_0})$ on the real axis.
background
The module instantiates the abstract RS carrier framework by showing that the Euler product for ζ(s) produces a concrete carrier C(s) = det₂² that is holomorphic and nonvanishing for Re(s) > 1/2. Core objects include the prime zeta PrimeSum σ := ∑_p p^{-σ}, the Hilbert-Schmidt norm squared HilbertSchmidtNorm σ := ∑_p p^{-2σ}, the carrier log series, and the derivative bound carrierDerivBound σ := 2 ∑_p (log p) p^{-2σ}/(1-p^{-σ}). The per-prime term supplies the summand for the last of these. The local setting proceeds from primes to Hilbert-Schmidt convergence of A(s), to convergence of log C(s), to bounded logarithmic derivative, enabling the EulerCarrier and RegularCarrier interfaces and the cost-covering axiom.
proof idea
The definition is the direct real-axis expression for the per-prime logarithmic derivative contribution. No lemmas or tactics are invoked; the body is the explicit formula matching the doc-comment description of d/dσ [log det₂_factor].
why it matters
This term is the atomic building block for carrierDerivBound and its immediate consequences carrierDerivBound_pos, carrierDerivBound_summable, carrierDerivTerm_nonneg, and the comparison theorems norm_eulerPrimeLogDerivTermComplex_le_carrierDerivTerm and norm_form_eq_carrierDerivTerm. It completes the step in the instantiation chain where the logarithmic derivative is shown finite, allowing C(s) to satisfy the EulerCarrier interface and thereby the cost-covering axiom that yields conditional RH. Within the Recognition framework it supplies the concrete Euler-product realization of the abstract carrier/sensor layer required for the recognition composition law applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.