eulerPrimeLogDerivTermComplex_summable
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish summability for real part of s at most 1/2.
- Does not supply explicit constants or decay rates.
- Does not address the pole at s=1 or other singularities.
- Does not prove the Riemann hypothesis.
formal statement (Lean)
535theorem eulerPrimeLogDerivTermComplex_summable {s : ℂ} (hs : 1/2 < s.re) :
536 Summable (fun p : Nat.Primes => eulerPrimeLogDerivTermComplex p s) := by
proof body
Term-mode proof.
537 refine Summable.of_norm ?_
538 exact (carrierDerivBound_summable hs).of_nonneg_of_le
539 (fun _ => norm_nonneg _)
540 (fun p => norm_eulerPrimeLogDerivTermComplex_le_carrierDerivTerm (by linarith) p)
541
542/-! ### §5d. Meromorphic order of ζ⁻¹ and quantitative factorization -/
543
544/-- `riemannZeta` is analytic at every `s ≠ 1`. Uses `DifferentiableOn.analyticAt`
545from Mathlib's complex Cauchy integral theory. -/