phase5_current_state
plain-language theorem explainer
The theorem records that the Riemann zeta function has no zeros for real part at least 1 and that the existence of the named strip bridge implies a logarithmic zero-free region for large imaginary part. Researchers tracing the Recognition Science zeta program would cite it as the Phase 5 state that separates proven boundary results from the remaining analytic bridge. The proof is a direct term-mode pairing of the half-plane lemma with the bridge implication.
Claim. The Riemann zeta function satisfies $r(s) = 0$ for no $s$ with real part at least 1. If the strip zero-free bridge holds, then there exist $c > 0$ and $T > 1$ such that $r(s) = 0$ is impossible whenever $|$imaginary part of $s| > T$ and real part of $s$ exceeds $1 - c / $log of that imaginary part.
background
Phase 5 of the RS-native zeta program records the proven zero-free region on Re(s) >=1 and names the logarithmic strip as the next bridge object. The StripZeroFreeBridge is the proposition that a LogZeroFreeStrip exists, which supplies the classical de la Vallee-Poussin shape. The module does not assert the full critical-strip result but packages the bridge so that later steps can see the irreducible analytic content needed for RH-quality closure.
proof idea
The proof is a one-line term that constructs the conjunction by feeding the half-plane result riemannZeta_ne_zero_re_ge_one into the first slot and the bridge-derived implication riemannZeta_ne_zero_in_log_strip into the second slot.
why it matters
This declaration marks the current unconditional results available to the Recognition Science zeta program and feeds the critical-strip zero-free bridge required for closure of the recovered RH chain. It isolates the gap between the boundary region Re >=1 and the open right half of the critical strip, noting that the full strip theorem follows from Mathlib's formal Riemann hypothesis but is not inhabited here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.