ClassicalZeroFreeRegionAttackSurface
plain-language theorem explainer
ClassicalZeroFreeRegionAttackSurface packages the proved non-negativity of the kernel 3 + 4 cos θ + cos 2θ with the conversion from a classical de la Vallée-Poussin zero-free region instance to StripZeroFreeBridge. Analytic number theorists formalizing the Riemann Hypothesis would cite the structure as the precise interface separating the elementary positivity result from the remaining analytic input. The declaration is introduced as a bare structure whose fields directly record Track B1 status.
Claim. A structure whose fields are a proof that $3 + 4 cos θ + cos(2θ) ≥ 0$ for all real $θ$, together with a map sending any instance of the de la Vallée-Poussin zero-free region (parameters $c > 0$, $T > 1$, and the condition that $ζ(s) ≠ 0$ whenever $Re(s) > 1 - c / log |Im(s)|$ for $|Im(s)| ≥ T$) to an instance of StripZeroFreeBridge.
background
The ClassicalZeroFreeRegion module opens Track B1 of the unconditional RH closure plan. It proves the elementary trigonometric identity 3 + 4 cos θ + cos 2θ = 2(cos θ + 1)^2 ≥ 0 and isolates the exact analytic input still missing from Mathlib. DeLaValleePoussinZeroFreeRegion is defined as the structure carrying c, T, and the zero-free statement on ζ; its doc-comment notes that supplying an inhabitant requires the full logarithmic derivative estimates and pole control. StripZeroFreeBridge is the Prop Nonempty LogZeroFreeStrip that serves as the next named bridge.
proof idea
The declaration is a structure definition with an empty proof body. The trig_kernel_nonneg field is supplied by the sibling lemma deLaValleePoussin_trig_kernel_nonneg. The open_deLaValleePoussin field is the conversion function stripZeroFreeBridge_of_deLaValleePoussin that turns the classical input into the bridge.
why it matters
The structure marks the exact status of Track B1 and is instantiated by the downstream definition classicalZeroFreeRegionAttackSurface. It separates the already-proved positivity kernel from the classical zero-free region input required for the logarithmic strip. The declaration touches the open Mathlib task of formalizing the full Hadamard-de la Vallée-Poussin theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.