eulerPrimeLogDerivTermComplex_summable
plain-language theorem explainer
The declaration shows that the series of complex Euler log-derivative terms over all primes converges whenever the real part of s exceeds 1/2. Researchers building the Recognition Science carrier framework from the Euler product for zeta would cite it to secure convergence of the logarithmic derivative on the half-plane. The proof is a one-line wrapper that applies a norm bound to reduce the complex case to the real carrier derivative summability already established in the module.
Claim. Let $P$ denote the set of primes. For $s$ complex with real part greater than $1/2$, the series $sum_{p in P} t_p(s)$ is summable, where $t_p(s)$ is the complex log-derivative term contributed by the prime $p$ in the Euler product expansion of the reciprocal zeta function.
background
The module instantiates the abstract RS carrier/sensor framework from AnnularCost and CostCoveringBridge by substituting the concrete Euler product for zeta. Core objects include the prime sum $P(sigma) = sum_p p^{-sigma}$, the squared Hilbert-Schmidt norm $sum_p p^{-2sigma}$, the carrier log series $sum_p [2 log(1-p^{-sigma}) + 2p^{-sigma}]$, and the carrier derivative bound $2 sum_p (log p) p^{-2sigma}/(1-p^{-sigma})$. The local setting is the chain primes to $A(s)$ Hilbert-Schmidt to $det_2(I-A(s))$ convergent to $C(s)$ holomorphic and nonvanishing on Re(s) > 1/2, which yields a bounded logarithmic derivative and satisfies the EulerCarrier and RegularCarrier interfaces.
proof idea
The proof is a one-line wrapper. It invokes Summable.of_norm on the real summability carrierDerivBound_summable at the given s, then applies the pointwise domination norm_eulerPrimeLogDerivTermComplex_le_carrierDerivTerm (valid for Re(s) > 1/2) together with nonnegativity of the norm to transfer the bound to the complex terms.
why it matters
The result feeds directly into zetaReciprocal_local_factorization, which extracts a local meromorphic factorization of zetaReciprocal at hypothetical zeros. It completes the Euler product instantiation step that guarantees the logarithmic derivative remains bounded on Re(s) > 1/2, thereby making the cost-covering axiom applicable and supporting the conditional Riemann hypothesis inside the Recognition Science framework. The underlying cost definitions tie back to the phi-ladder and J-cost structures from PhiForcingDerived.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.