StripZeroFreeBridge
plain-language theorem explainer
StripZeroFreeBridge defines the proposition that a logarithmic zero-free strip exists, serving as the named bridge object in Phase 5 of the RS-native zeta program. Number theorists tracking the Riemann hypothesis closure in this framework cite it to separate the proven Re(s) >= 1 zero-free region from the required strip result. The definition is a direct one-line abbreviation asserting non-emptiness of the LogZeroFreeStrip structure.
Claim. Let LogZeroFreeStrip denote the structure consisting of constants $c > 0$ and $T > 1$ such that for all $s$ with $|Im(s)| >= T$, if $Re(s) > 1 - c / log|Im(s)|$ then the Riemann zeta function satisfies zeta(s) != 0. Then StripZeroFreeBridge is the proposition that this structure is nonempty.
background
Phase 5 of the RS-native zeta program records the proven zero-free result on Re(s) >= 1 from Mathlib and packages the remaining strip theorem as a bridge. The LogZeroFreeStrip structure specifies a classical Hadamard-de la Vallee-Poussin zero-free region: for |Im(s)| >= T the half-plane Re(s) > 1 - c / log(|Im(s)|) contains no zeros of the Riemann zeta function, with c_pos and T_gt_one ensuring positivity and size. This module imports WeakZeroFreeRegion and ZetaFromTheta to support the boundary certificate while leaving the strip as an open named object.
proof idea
The definition is a one-line wrapper that directly equates StripZeroFreeBridge to the proposition Nonempty LogZeroFreeStrip.
why it matters
This declaration earns its place by naming the missing classical zero-free strip input required for RH-quality results in the RS program. It is used by riemannZeta_ne_zero_in_log_strip to derive the zero-free conclusion from the bridge, by phase5_current_state to state the current unconditional status, and by StripPhase5Cert to bundle the boundary certificate with the open strip bridge. The de la Vallee-Poussin theorem, once formalized, would inhabit this bridge via stripZeroFreeBridge_of_deLaValleePoussin.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.