carrierValue
The carrier value C(σ) for real σ is defined by exponentiating the carrier logarithm series from the Euler product over primes. Researchers on the recognition science cost-covering bridge cite it when verifying nonvanishing and derivative bounds on Re(s) > 1/2. The definition is a direct one-line wrapper applying the real exponential to the summed det2LogFactor terms.
claim$C(σ) := exp(2 ∑_p [log(1 - p^{-σ}) + p^{-σ}]), equivalently the product ∏_p (1 - p^{-σ})^2 exp(2 p^{-σ}).
background
The EulerInstantiation module instantiates the abstract RS carrier/sensor framework from AnnularCost and CostCoveringBridge via the Euler product of ζ(s). Core objects include PrimeSum σ := ∑_p p^{-σ}, HilbertSchmidtNorm σ := ∑_p p^{-2σ}, carrierLogSeries σ := ∑_p [2 log(1-p^{-σ}) + 2p^{-σ}], and carrierDerivBound σ. The module shows 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
One-line wrapper that applies the real exponential to the output of carrierLog σ.
why it matters in Recognition Science
This definition supplies the concrete carrier value used in the EulerInstantiationCert structure, which packages the full chain from Euler product to cost-covering applicability. It feeds ZeroFreeCriterion for the analytic route and appears in carrier_nonvanishing, carrier_pos, and zeros_in_continuation. In the Recognition framework it realizes the abstract carrier from the T5 J-uniqueness and RCL, enabling conditional RH via the cost-covering axiom.
scope and limits
- Does not establish convergence of the defining series.
- Does not extend the definition to complex s.
- Does not bound the logarithmic derivative.
- Does not connect explicitly to the prime zeta function P(s).
formal statement (Lean)
189noncomputable def carrierValue (σ : ℝ) : ℝ :=
proof body
Definition body.
190 Real.exp (carrierLog σ)
191
192/-- The carrier log-series converges on Re(s) > 1/2. -/