DeLaValleePoussinZeroFreeRegion
plain-language theorem explainer
The DeLaValleePoussinZeroFreeRegion structure encodes the classical Hadamard-de la Vallee-Poussin zero-free strip for the Riemann zeta function. Number theorists formalizing unconditional results toward the Riemann hypothesis would cite it as the exact analytic input needed to inhabit the LogZeroFreeStrip bridge. It is introduced as a structure definition whose fields directly mirror the target interface, leaving the analytic estimates as future work.
Claim. A structure consisting of real numbers $c > 0$ and $T > 1$ such that for every complex number $s$ with $|Im(s)| ≥ T$, if $Re(s) > 1 - c / log |Im(s)|$ then the Riemann zeta function satisfies $ζ(s) ≠ 0$.
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, so the module isolates the missing logarithmic strip input. It proves the elementary trigonometric kernel 3 + 4 cos θ + cos 2θ = 2(cos θ + 1)^2 ≥ 0 and defines the precise shape required to inhabit LogZeroFreeStrip from the StripZeroFreeRegion import. The structure is deliberately not an axiom; an inhabitant would require the full de la Vallee-Poussin estimates.
proof idea
The declaration is a structure definition with no proof body. It packages the parameters c and T together with the positivity hypotheses c_pos and T_gt_one and the zero-free predicate zero_free, which directly replicates the LogZeroFreeStrip interface.
why it matters
This structure supplies the input for logZeroFreeStrip_of_deLaValleePoussin and stripZeroFreeBridge_of_deLaValleePoussin, which produce the StripZeroFreeBridge object. It therefore occupies the remaining analytic slot in the ClassicalZeroFreeRegionAttackSurface bundle. The declaration touches the open question of porting the classical zero-free region into Mathlib without yet closing it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.