carrierLog
plain-language theorem explainer
carrierLog supplies the explicit logarithmic expression for the carrier C(σ) in the Euler product instantiation of the RS cost structure. Researchers deriving holomorphic properties of C(s) on Re(s) > 1/2 or applying the cost-covering axiom would cite this definition. It is realized directly as twice the sum over the prime set of the per-prime log-determinant factor.
Claim. $\log C(\sigma) := 2 \sum_{p \in \Primes} \bigl( \log(1 - p^{-\sigma}) + p^{-\sigma} \bigr)$, where the sum runs over the set of primes and $\Primes$ is the set of prime numbers.
background
The EulerInstantiation module realizes the abstract RS carrier from AnnularCost and CostCoveringBridge via the Euler product of ζ(s). Core objects include PrimeSum σ := ∑p p^{-σ} and the per-prime factor det2LogFactor(p, σ) := log(1 − p^{-σ}) + p^{-σ}, whose series form is −∑{m≥2} (p^{-σ})^m / m. The module doc states the instantiation chain: primes → A(s) Hilbert–Schmidt → det₂(I−A(s)) convergent → C(s) = det₂² holomorphic nonvanishing on Re(s) > 1/2 → logarithmic derivative bounded → EulerCarrier + RegularCarrier satisfied.
proof idea
This definition is a direct one-line abbreviation that sums det2LogFactor over the set Nat.Primes and multiplies by 2.
why it matters
carrierLog is invoked by carrierValue to recover C(σ) = exp(carrierLog σ) and by the carrier_zeta_identity theorem, which states that for σ > 1 the equality holds by reflexivity. It supplies the concrete Euler-product side of Layer 3 in the module architecture, enabling the cost-covering axiom and conditional RH. The construction connects the prime zeta function to the RS carrier without invoking the J-uniqueness or eight-tick octave steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.