riemannZeta_ne_zero_in_log_strip
plain-language theorem explainer
Any StripZeroFreeBridge yields constants c and T such that the Riemann zeta function has no zeros in the region Re(s) > 1 - c / log|Im(s)| for |Im(s)| >= T. Researchers advancing the Recognition Science zeta program toward Riemann-hypothesis closure would cite this as the direct implication of the bridge object. The proof is a one-line extraction that unpacks the bridge structure to obtain the constants and the zero-free predicate.
Claim. If a StripZeroFreeBridge exists, then there exist real numbers $c > 0$ and $T > 1$ such that for every complex $s$ with $|Im(s)| >= T$, the condition $Re(s) > 1 - c / log|Im(s)|$ implies zeta(s) != 0.
background
The StripZeroFreeRegion module constitutes Phase 5 of the RS-native zeta program. It records the proven zero-free result on the half-plane Re(s) >= 1 while packaging the stronger logarithmic strip as the named bridge object StripZeroFreeBridge, defined to be the nonemptiness of LogZeroFreeStrip. The module documentation states that the strip theorem is not asserted as proved but is instead presented as a bridge whose existence would immediately deliver the corresponding zero-free conclusion.
proof idea
The proof is a one-line wrapper. It destructures the bridge hypothesis to extract the fields c, T, c_pos, T_gt_one and zero_free from the underlying LogZeroFreeStrip structure and assembles them into the required existential statement.
why it matters
This theorem supplies the conditional half of the conjunction that appears in the downstream phase5_current_state theorem, which records the present unconditional zero-free region available to the RS zeta program. It fills the explicit role of the named bridge for the genuine strip-zero-free theorem still required for RH-quality closure, as described in the module documentation. The construction keeps the proven boundary result separate from the open strip step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.