eulerZeroWindingCert
plain-language theorem explainer
The declaration supplies the zero-winding certificate for the Euler carrier on any disk centered at real σ₀ > 1/2 with radius reaching the critical line. Researchers packaging the carrier for sampled-trace analysis or the conditional Riemann hypothesis would cite it. The proof is a one-line wrapper that converts the complex carrier certificate into the zero-winding structure.
Claim. For any real number σ₀ > 1/2, the Euler carrier admits a zero-winding certificate on the disk centered at σ₀ with radius σ₀ − 1/2, asserting that the carrier function has zero winding number around every interior circle.
background
The module upgrades the real-axis Euler carrier to a complex-analytic object on the half-plane Re(s) > 1/2. The carrier is defined as C(s) = det₂(I − A(s))² = ∏_p (1 − p^{-s})² exp(2p^{-s}), which is holomorphic and nonvanishing on that half-plane by standard results on regularized Fredholm determinants. ZeroWindingCert is the structure consumed by the sampled-trace layer; it records a center, positive radius, the underlying ComplexCarrierCert, and the assertion that contourWinding equals zero on every smaller circle. mkComplexCarrierCert constructs the ComplexCarrierCert for any σ₀ > 1/2 by placing the disk center at σ₀ and radius at σ₀ − 1/2.
proof idea
One-line wrapper that applies toZeroWindingCert to the ComplexCarrierCert produced by mkComplexCarrierCert σ₀ hσ.
why it matters
This definition supplies the zero-winding property required by eulerSampledBudgetedCarrier to package the carrier as a BudgetedCarrier and by riemann_hypothesis_euler_conditional to obtain the full RH statement under cost-covering and topological-floor hypotheses. It completes the complex upgrade step that lets contour integration replace synthetic zero-charge traces in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.