classicalZeroFreeRegionAttackSurface
plain-language theorem explainer
Classical zero-free region attack surface bundles the proved nonnegativity of the de la Vallee-Poussin kernel 3 + 4 cos θ + cos 2θ with the conversion from a hypothetical de la Vallee-Poussin zero-free region to a strip zero-free bridge. Researchers formalizing the Riemann Hypothesis unconditional closure would reference this as the current Track B1 status marker. The definition constructs the record by direct assignment of the kernel theorem and the bridge lemma.
Claim. The classical zero-free region attack surface is the record whose first field asserts that $3 + 4 cos θ + cos 2θ ≥ 0$ for every real $θ$, and whose second field asserts that any de la Vallee-Poussin zero-free region yields a strip zero-free bridge.
background
Module ClassicalZeroFreeRegion tracks Track B1 of the RH unconditional-closure plan. Mathlib supplies riemannZeta_ne_zero_of_one_le_re but lacks the Hadamard-de la Vallee-Poussin logarithmic zero-free strip. The structure ClassicalZeroFreeRegionAttackSurface packages the elementary positivity kernel proved via reduction to a square together with the exact analytic input DeLaValleePoussinZeroFreeRegion that would produce StripZeroFreeBridge. Upstream results are the nonnegativity theorem and the bridge construction that applies the log zero-free strip lemma.
proof idea
The definition is a record constructor that directly assigns the proved theorem deLaValleePoussin_trig_kernel_nonneg to the trig_kernel_nonneg field and the theorem stripZeroFreeBridge_of_deLaValleePoussin to the open_deLaValleePoussin field.
why it matters
This declaration supplies the B1 status bundle in the Recognition Science framework. It feeds the unconditional RH closure plan by marking the elementary kernel as proved while leaving the classical analytic zero-free region as an open hypothesis. The module doc-comment identifies it as the starting point for porting the Hadamard-de la Vallee-Poussin theorem without assuming the hard analytic result is already formalized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.