ClassicalZeroFreeRegionAttackSurface
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not prove the de la Vallée-Poussin zero-free region.
- Does not derive the Riemann Hypothesis.
- Does not supply logarithmic derivative estimates for ζ.
- Does not close the unconditional RH plan.
formal statement (Lean)
88structure ClassicalZeroFreeRegionAttackSurface where
89 trig_kernel_nonneg :
90 ∀ θ : ℝ, 0 ≤ 3 + 4 * Real.cos θ + Real.cos (2 * θ)
91 open_deLaValleePoussin :
92 DeLaValleePoussinZeroFreeRegion → StripZeroFreeBridge
93