LogZeroFreeStrip
plain-language theorem explainer
LogZeroFreeStrip encodes the classical Hadamard-de la Vallée-Poussin zero-free region for the Riemann zeta function as a structure with parameters c and T. Number theorists bridging analytic estimates to the Recognition Science zeta program cite this object when separating the unconditional boundary result from the deeper strip needed for Phase 5 closure. The declaration is a bare structure definition that records the required analytic input without supplying a proof.
Claim. A logarithmic zero-free strip consists of real constants $c > 0$ and $T > 1$ such that for every complex $s$ with $|Im(s)| ≥ T$, if $Re(s) > 1 - c / log|Im(s)|$, then the Riemann zeta function satisfies $ζ(s) ≠ 0$.
background
This structure sits in the StripZeroFreeRegion module, Phase 5 of the RS-native zeta program. The module records the unconditional zero-free result on the half-plane Re(s) ≥ 1 and packages the deeper logarithmic strip as the next bridge object. Upstream results include the positivity of the de la Vallée-Poussin trigonometric kernel and the boundary zero-free certification, which together justify the classical strip shape stated in the doc-comment.
proof idea
The declaration is a structure definition that directly encodes the zero-free condition as a field. No lemmas are applied; it serves as the target type for the classical input supplied by DeLaValleePoussinZeroFreeRegion.
why it matters
LogZeroFreeStrip supplies the exact shape required by the Phase 5 bridge in the Recognition Science zeta program, feeding directly into StripZeroFreeBridge and phase5_current_state. It connects the classical Hadamard-de la Vallée-Poussin theorem to the RS framework, where the logarithmic strip is the missing analytic step toward RH-quality closure. The parent theorem phase5_current_state uses it to separate the proven boundary region from the conditional strip.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.