carrierLog
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 in Recognition Science
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.
scope and limits
- Does not prove convergence of the infinite sum.
- Does not extend the definition to complex σ.
- Does not derive any relation to the Riemann zeta function itself.
- Does not supply numerical evaluations or bounds.
Lean usage
noncomputable def carrierValue (σ : ℝ) : ℝ := Real.exp (carrierLog σ)formal statement (Lean)
184noncomputable def carrierLog (σ : ℝ) : ℝ :=
proof body
Definition body.
185 2 * ∑' (p : Nat.Primes), det2LogFactor p σ
186
187/-- The carrier value: C(σ) = exp(log C(σ)).
188 This represents C(s) = ∏_p (1−p^{−s})² exp(2p^{−s}). -/