logZeroFreeStrip_of_deLaValleePoussin
plain-language theorem explainer
The definition converts a classical de la Vallée-Poussin zero-free region structure into the logarithmic zero-free strip format required by the Phase 5 bridge. Number theorists formalizing the Riemann hypothesis closure cite this conversion when supplying the Hadamard-de la Vallée-Poussin input to the Recognition Science number theory layer. It is realized as a direct field assignment from the input structure.
Claim. Given a de la Vallée-Poussin zero-free region $Z$ with constants $c>0$, $T>1$ and the predicate that the Riemann zeta function satisfies $Z(s)≠0$ whenever $T≤|Im(s)|$ and $Re(s)>1-c/ log|Im(s)|$, the associated logarithmic zero-free strip is the structure carrying exactly the same $c$, $T$, positivity of $c$, $T>1$, and zero-free predicate.
background
The ClassicalZeroFreeRegion module tracks track B1 of the RH unconditional-closure plan. Mathlib supplies only the boundary result riemannZeta_ne_zero_of_one_le_re; the module therefore isolates the precise analytic input whose proof would inhabit LogZeroFreeStrip and supplies the conversion to StripZeroFreeBridge. DeLaValleePoussinZeroFreeRegion is the structure holding width parameter $c$, height $T$, the positivity $0<c$, the inequality $1<T$, and the zero-free condition on zeta in the indicated strip. Upstream results include the positivity lemmas c_pos for the speed of light in RS-native units from Constants, ConstantDerivations, and Codata, together with the fundamental period abbreviation T from Breath1024.
proof idea
This is a definition that constructs LogZeroFreeStrip by direct projection of the fields c, T, c_pos, T_gt_one, and zero_free from the supplied DeLaValleePoussinZeroFreeRegion structure. No lemmas beyond the structure accessors are invoked.
why it matters
The definition supplies the concrete inhabitant for LogZeroFreeStrip that is wrapped into StripZeroFreeBridge by the downstream theorem stripZeroFreeBridge_of_deLaValleePoussin. It advances the B1 track toward unconditional closure of the Riemann hypothesis by providing the conversion from the classical zero-free region. The module comment states that supplying an inhabitant for DeLaValleePoussinZeroFreeRegion constitutes the real Mathlib-grade analytic work involving logarithmic derivative estimates for zeta and control of the pole at s=1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.