zeros_in_continuation
plain-language theorem explainer
The theorem asserts that the carrier value stays positive for every real σ exceeding 1 inside the Euler product instantiation. Researchers applying the cost-covering bridge to obtain a conditional Riemann hypothesis would cite this non-vanishing fact on the right half-plane. The proof is a one-line wrapper that applies the carrier positivity lemma after a linear arithmetic reduction of the hypothesis.
Claim. For every real number σ satisfying σ > 1, the carrier value at σ is positive.
background
The module shows that the Euler product of ζ(s) supplies a concrete carrier that satisfies the abstract RS carrier/sensor axioms from AnnularCost and CostCoveringBridge. Core objects are PrimeSum σ := ∑_p p^{-σ}, HilbertSchmidtNorm σ := ∑_p p^{-2σ}, carrierLogSeries σ := ∑_p [2 log(1 - p^{-σ}) + 2 p^{-σ}], and the associated derivative bound. The local setting constructs C(s) := det₂² as holomorphic and nonvanishing on Re(s) > 1/2, with the present result securing positivity on the stricter region Re(s) > 1 that precedes the natural boundary at Re(s) = 1.
proof idea
The term proof introduces σ and the assumption 1 < σ, then applies the carrier_pos lemma whose hypotheses are discharged by linarith.
why it matters
The result supplies the non-vanishing step required for the Euler instantiation chain (primes → Hilbert-Schmidt convergence → det₂ product → C(s) nonvanishing → euler_instantiation), which in turn feeds the cost-covering axiom toward conditional RH. It directly encodes the statement that exp(2P(s)) has no zeros for Re(s) > 1 while its continuation C(s)·ζ(s)² acquires the zeros of ζ at doubled order. The declaration therefore closes one interface between the number-theoretic carrier and the upstream J-cost and defect structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.