CriticalStripZeroFreeBridge
plain-language theorem explainer
The declaration names the proposition that a witness exists asserting the Riemann zeta function has no zeros in the open strip 1/2 < Re(s) < 1. Researchers closing the RS-native zeta program toward the Riemann hypothesis cite it as the remaining analytic target. It is realized as a one-line wrapper around the nonempty type of the CriticalStripZeroFree structure.
Claim. The proposition that there exists a witness such that the Riemann zeta function satisfies $riemannZeta(s) ≠ 0$ for every complex $s$ with $1/2 < Re(s) < 1$.
background
This definition appears in the StripZeroFreeRegion module, which constitutes Phase 5 of the RS-native zeta program. The module records the already-proved zero-free result on the half-plane Re(s) ≥ 1 and packages the open critical-strip statement as a named bridge object rather than an asserted theorem. CriticalStripZeroFree is the structure whose single field encodes the zero-free condition on 1/2 < Re(s) < 1. The surrounding context treats the boundary region as settled while leaving the interior strip as the explicit target for later closure steps.
proof idea
This is a one-line definition that directly asserts Nonempty CriticalStripZeroFree, where the structure CriticalStripZeroFree supplies the universal quantification over the open strip.
why it matters
It functions as the target object consumed by downstream results including criticalStripBridge_of_pickPositive (which derives the bridge from finite Pick positivity plus the Schur no-poles principle) and criticalStripZeroFreeBridge_of_riemannHypothesis (which shows that Mathlib's RiemannHypothesis directly yields the bridge). StripPhase7Cert records that the bridge is no stronger than the Riemann hypothesis itself. Within the broader Recognition framework the declaration marks the precise analytic gap between the proved boundary zero-free region and full RH-quality closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.