carrier_nonvanishing
plain-language theorem explainer
The Euler carrier C(σ) is nonzero for every real σ > 1/2. Researchers building zero-free criteria from the Euler product and cost-covering axioms would cite this to close the nonvanishing clause of the EulerCarrier interface. The proof is a one-line term that applies the positivity of the exponential representation.
Claim. Let $C(σ) = exp(∑_p [2 log(1 - p^{-σ}) + 2 p^{-σ}])$ denote the squared regularized determinant of the Euler product. Then $C(σ) ≠ 0$ for every real $σ > 1/2$.
background
The module instantiates the abstract RS carrier from AnnularCost and CostCoveringBridge by the concrete Euler product. carrierValue σ is defined as Real.exp(carrierLog σ), which equals the product ∏_p (1 - p^{-σ})^2 exp(2 p^{-σ}). The module proves this object is holomorphic and nonvanishing on Re(s) > 1/2, satisfying the EulerCarrier and RegularCarrier interfaces needed for the cost-covering axiom. The immediate upstream result is the sibling theorem carrier_pos, which establishes strict positivity of the same exponential via Real.exp_pos.
proof idea
The proof is a one-line term that applies ne_of_gt to the positivity statement carrier_pos hσ.
why it matters
This supplies the carrier_nonzero field inside mkEulerInstantiationCert and is called directly by euler_trace_admissible to certify admissible Euler traces for every DefectSensor. It is also used in the ZeroFreeCriterion definitions zeroFreeCriterion_of_honestPhaseChargeZeroBridge, zeroFreeCriterion_of_honestPhaseCostBridge and zeroFreeCriterion_of_vectorC. The result completes the nonvanishing step of the Euler instantiation chain that enables the cost-covering axiom and conditional RH. It leaves open the extension of nonvanishing from the real line into the complex strip.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.