eulerPrimeLogDerivTermComplex
plain-language theorem explainer
eulerPrimeLogDerivTermComplex defines the complex per-prime logarithmic derivative contribution (log p) p^{-2s} / (1 - p^{-s}) for each prime p. Number theorists instantiating the Euler product inside the Recognition Science carrier framework cite this term when lifting real derivative bounds to the complex plane for perturbation budgets on sampled circles. The definition is a direct algebraic quotient using the prime logarithm and the squared Euler prime power complex factor.
Claim. For a prime $p$ and complex $s$, the per-prime term is given by $ (log p) p^{-2s} / (1 - p^{-s}) $, where $p^{-s}$ denotes the complex power and the expression supplies the natural prime-level quantity whose norm enters the perturbation budget.
background
The module EulerInstantiation shows how the Euler product for zeta(s) realizes the abstract RS carrier and sensor framework from AnnularCost and CostCoveringBridge. Primes is the set of all prime natural numbers. Core objects include the prime sum P(sigma) = sum_p p^{-sigma}, the Hilbert-Schmidt norm squared sum_p p^{-2sigma}, the carrier log series sum_p [2 log(1 - p^{-sigma}) + 2 p^{-sigma}], and the carrier derivative bound 2 sum_p (log p) p^{-2sigma} / (1 - p^{-sigma}). Upstream results supply the reciprocal automorphism from CostAlgebra, the 8-tick phases, the defect functional from the law of existence, and the reciprocal event from LedgerForcing.
proof idea
The definition is a direct one-line algebraic expression that multiplies the complexified prime logarithm by the square of the Euler prime power complex term and divides by one minus that term.
why it matters
This term is invoked by eulerPrimeLogDerivTermComplex_summable to establish summability on Re(s) > 1/2 and by the norm comparison theorems that dominate the real carrier derivative bound. It supports verification of the EulerCarrier interface and carrier_deriv_finite, advancing the conditional Riemann hypothesis through the cost-covering axiom. The construction sits inside the T0-T8 forcing chain and the Recognition Composition Law, with the eight-tick octave and D = 3 dimensions providing the broader structural setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.