sensor_carrier_compatible
plain-language theorem explainer
The theorem shows that any DefectSensor at a hypothetical zero with real part σ₀ > 1/2 admits a RegularCarrier of radius exactly σ₀ − 1/2 that remains inside Re(s) > 1/2 and is holomorphic nonvanishing on the disk. Researchers closing the Euler-product instantiation of the RS cost-covering framework would cite it to confirm carrier compatibility before invoking the conditional RH axiom. The proof is a direct exact construction that invokes the Euler regular carrier builder and checks radius positivity by linear arithmetic on the strip-membersip
Claim. Let σ₀ > 1/2 be the real part of a hypothetical zero ρ. There exists a regular carrier whose radius equals σ₀ − 1/2 and is strictly positive, so that the disk D(ρ, σ₀ − 1/2) lies inside {Re(s) > 1/2} with the carrier holomorphic and nonvanishing throughout the disk.
background
The Euler Product Instantiation module realizes the abstract RS carrier/sensor framework of AnnularCost and CostCoveringBridge by means of the zeta-function Euler product. A DefectSensor encodes the location of a hypothetical zero together with its membership in the half-plane Re(s) > 1/2. A RegularCarrier is a holomorphic nonvanishing function defined on a disk that covers the annular region between the critical line and the sensor’s real part.
proof idea
The proof is a one-line exact tactic. It constructs the carrier by applying eulerRegularCarrier to the sensor’s real part and its strip-membership hypothesis, then verifies the radius equality and the strict positivity 0 < radius by rewriting the inequality and discharging it with linarith on the strip fact.
why it matters
This result supplies the carrier_compatible field of the EulerTraceAdmissible structure in UnifiedRH, which in turn completes the Euler instantiation certificate that licenses the cost-covering axiom and yields conditional RH. It therefore closes the concrete-to-abstract bridge in the chain primes → Hilbert–Schmidt operator → det₂ convergence → holomorphic nonvanishing carrier → cost-covering applicability.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.