carrierValue
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.