eulerZeroWindingCert
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove holomorphy or differentiability of the carrier on the complex plane (requires unavailable Mathlib infinite-product API).
- Does not extend the certificate to the critical line Re(s) = 1/2.
- Does not supply explicit numerical bounds on the logarithmic derivative beyond the certificate fields.
- Does not address convergence or nonvanishing for Re(s) ≤ 1/2.
Lean usage
SampledTrace.sampledBudgetedCarrier (eulerZeroWindingCert σ₀ hσ) (carrierDerivBound σ₀) (carrierDerivBound_pos hσ)formal statement (Lean)
143noncomputable def eulerZeroWindingCert (σ₀ : ℝ) (hσ : 1/2 < σ₀) :
144 ZeroWindingCert :=
proof body
Definition body.
145 (mkComplexCarrierCert σ₀ hσ).toZeroWindingCert
146
147end
148
149end EulerCarrierComplex
150end NumberTheory
151end IndisputableMonolith