criticalStripZeroFreeBridge_of_riemannHypothesis
plain-language theorem explainer
Mathlib's Riemann hypothesis implies the critical-strip zero-free bridge in the Recognition Science zeta program. Researchers closing phase 7 of the RS-native zeta function cite this link to connect classical RH to the framework's certification objects. The proof is a one-line term construction that packages the zero-free conclusion derived from the hypothesis into the required bridge structure.
Claim. If the Riemann hypothesis holds, then the critical-strip zero-free bridge exists, i.e., the open right half-strip is zero-free for the Riemann zeta function.
background
The StripZeroFreeRegion module handles phase 5 of the RS-native zeta program. It records the already-proved zero-free region for Re(s) >= 1 and defines the critical-strip bridge as the named target CriticalStripZeroFreeBridge, which is the proposition Nonempty CriticalStripZeroFree. The module explicitly avoids asserting the full strip theorem as proved and instead packages the conditional statement that Mathlib's RiemannHypothesis implies the open right half-strip is zero-free.
proof idea
This is a one-line term proof. It constructs the CriticalStripZeroFreeBridge structure by setting the zero_free field to the result of applying criticalStrip_zero_free_of_riemannHypothesis to the supplied RiemannHypothesis assumption.
why it matters
The theorem shows that the critical-strip bridge follows from the classical Riemann hypothesis and is used directly in stripPhase7Cert to record the honest phase-7 state: boundary region proved, critical-strip bridge named and conditional on RH. It marks the boundary between established zero-free results on Re(s) >= 1 and the remaining RH-quality closure needed for the RS zeta program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.