carrier_zeta_identity
plain-language theorem explainer
The carrier logarithm for real σ > 1 equals twice the sum over primes of the determinant-two log factor. Researchers instantiating the Recognition Science cost structure via the Euler product for zeta cite this when equating the abstract carrier to its explicit prime-sum form. The equality holds by reflexivity from the definition of carrierLog.
Claim. For real σ > 1, the carrier logarithm satisfies carrierLog(σ) = 2 ∑_{p prime} det₂LogFactor(p, σ).
background
The Euler Product Instantiation module realizes the abstract RS carrier/sensor framework from AnnularCost and CostCoveringBridge through the Euler product of ζ(s). Core objects include PrimeSum σ := ∑_p p^{-σ} (convergent for σ > 1), HilbertSchmidtNorm σ := ∑_p p^{-2σ}, carrierLogSeries σ := ∑_p [2 log(1-p^{-σ}) + 2p^{-σ}], and carrierDerivBound σ. The local setting shows primes → A(s) Hilbert–Schmidt → det₂(I−A(s)) convergent → C(s) holomorphic and nonvanishing on Re(s) > 1/2, enabling the cost-covering axiom and conditional RH.
proof idea
The proof is a one-line reflexivity that follows directly from the definition of carrierLog as the prime-factor sum.
why it matters
This identity anchors the concrete Euler product realization of the RS carrier, supporting the module chain from primes through Hilbert–Schmidt convergence and nonvanishing of C(s) on Re(s) > 1/2 to the EulerCarrier interface. It fills the Layer 3 step in the instantiation architecture that feeds euler_instantiation and euler_regular_carrier, closing the path to conditional RH via the cost-covering axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.