carrierDerivBound_summable
plain-language theorem explainer
The series summing carrier derivative terms over primes converges for every real σ₀ > 1/2. Analysts instantiating the Recognition Science carrier via the Euler product cite this to obtain a uniform bound on the logarithmic derivative of C(s). The proof introduces ε = σ₀ - 1/2, builds an explicit majorant K · p^{-(σ₀ + 1/2)}, and verifies term-by-term domination via log p ≤ p^ε/ε together with p ≥ 2 comparisons in the denominator.
Claim. For every real number σ₀ > 1/2 the series ∑_{p prime} p^{-2σ₀} (log p) / (1 - p^{-σ₀}) converges.
background
The EulerInstantiation module embeds the Euler product of ζ(s) into the abstract RS carrier/sensor framework defined in AnnularCost and CostCoveringBridge. Core objects include the prime sum, the Hilbert-Schmidt norm squared ∑ p^{-2σ}, the carrier log series, and the carrier derivative bound whose individual terms are p^{-2σ₀} log p / (1 - p^{-σ₀}). The module proves that the resulting C(s) = det₂²(I - A(s)) is holomorphic and non-vanishing for Re(s) > 1/2, thereby satisfying the EulerCarrier interface and enabling the cost-covering axiom.
proof idea
Define ε := σ₀ - 1/2 and K := (1/ε) · (1 - 2^{-σ₀})^{-1}. First invoke Nat.Primes.summable_rpow to obtain summability of ∑ p^{-(σ₀ + 1/2)} and scale by K. For each prime p apply Real.log_le_rpow_div to bound log p by p^ε/ε, use rpow monotonicity to replace p^{-σ₀} by 2^{-σ₀} in the denominator, and rearrange the resulting expression algebraically to match K · p^{-(σ₀ + 1/2)}. The comparison is completed by gcongr and ring tactics.
why it matters
This theorem supplies the finiteness of the carrier logarithmic derivative bound required for the instantiation chain primes → Hilbert-Schmidt convergence → det₂ convergence → C(s) holomorphic and non-vanishing on Re(s) > 1/2 → bounded |C'/C|. It is invoked directly by carrierDerivBound_pos and by eulerPrimeLogDerivTermComplex_summable to lift the bound to complex s. Within the Recognition Science framework the result closes the step from EulerCarrier to the cost-covering axiom, supporting the conditional Riemann hypothesis while remaining consistent with the eight-tick octave and phi-ladder structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.