carrierLog
plain-language theorem explainer
carrierLog(σ) supplies the logarithm of the Euler-product carrier C(σ) as twice the sum over primes of the per-prime log-determinant factors. Researchers working on the Recognition Science cost-covering bridge cite it to link the concrete zeta Euler product to the abstract carrier axioms. The definition is a direct one-line wrapper that folds det2LogFactor over the prime set.
Claim. $log C(σ) = 2 ∑_{p prime} [log(1 - p^{-σ}) + p^{-σ}]$, equivalently $log C(σ) = -2 ∑_{m≥2} P(mσ)/m$ for real σ, where P denotes the prime zeta sum.
background
The EulerInstantiation module shows that the Euler product of ζ(s) instantiates the abstract RS carrier/sensor framework from AnnularCost and CostCoveringBridge. Layer 3 of the architecture maps primes to a Hilbert-Schmidt operator A(s), then to the convergent det₂(I - A(s)), yielding the holomorphic nonvanishing carrier C(s) on Re(s) > 1/2. Core objects include PrimeSum σ := ∑_p p^{-σ} and the per-prime factor whose log is supplied by det2LogFactor.
proof idea
This is a one-line definition that applies the sum over the set Primes of det2LogFactor p σ, where det2LogFactor(p, σ) expands as log(1 - p^{-σ}) + p^{-σ}.
why it matters
carrierLog feeds directly into carrierValue, which recovers C(σ) = exp(carrierLog σ), and into the carrier_zeta_identity theorem that equates the sum to the prime-factor expression for σ > 1. It completes the instantiation step primes → A(s) Hilbert-Schmidt → det₂ convergent → C(s) holomorphic nonvanishing, enabling the cost-covering axiom and conditional RH. The construction sits inside the RS framework's Euler product realization of the carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.