carrier_log_convergent
plain-language theorem explainer
The theorem establishes convergence of the carrier logarithmic series derived from the Euler product for real parts exceeding 1/2. Researchers instantiating the Recognition Science cost-covering bridge via zeta-function Euler products would cite it to secure holomorphy of the carrier. The proof reduces directly to a single application of the product convergence result.
Claim. For every real number $σ > 1/2$, the series $∑_{p prime} [2 log(1 - p^{-σ}) + 2 p^{-σ}]$ converges.
background
The module supplies the concrete Euler-product layer that realizes the abstract RS carrier framework. Core objects include the prime sum $P(σ) = ∑_p p^{-σ}$, the squared Hilbert-Schmidt norm $∑_p p^{-2σ}$, the carrier log series $∑_p [2 log(1-p^{-σ}) + 2p^{-σ}]$, and the derivative bound $2∑_p (log p) p^{-2σ}/(1-p^{-σ})$. The three-layer architecture runs from the abstract cost axioms in AnnularCost through the conditional RH bridge to this Euler instantiation.
proof idea
The proof is a one-line wrapper that applies the det2 product convergence lemma to the hypothesis σ > 1/2.
why it matters
The result occupies the listed key slot for carrier log convergence and feeds the euler_instantiation theorem that verifies the EulerCarrier interface. It supplies the summability required for the logarithmic derivative bound, enabling the cost-covering axiom and conditional Riemann hypothesis within the Recognition Science chain from Hilbert-Schmidt convergence to holomorphic nonvanishing carrier on Re(s) > 1/2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.