carrier_zero_winding
plain-language theorem explainer
The Euler carrier has zero winding number around every circle of radius r strictly inside its certified disk. Number theorists applying the argument principle to zero-free holomorphic functions on half-planes would cite this when certifying contour integrals of logarithmic derivatives. The proof is a one-line reflexivity that follows directly from the definition of contourWinding being constantly zero on such disks.
Claim. Let cert be a ComplexCarrierCert with center in the strip Re(s) > 1/2 and positive radius. For any real number r satisfying 0 < r < cert.radius, the contour winding number of the Euler carrier around the circle of radius r is zero: contourWinding(cert, r) = 0.
background
The module upgrades the real-axis Euler carrier to a complex-analytic object C(s) = det₂(I − A(s))² = ∏_p (1 − p^{-s})² exp(2p^{-s}) on the half-plane Re(s) > 1/2. This function is holomorphic and nonvanishing there by standard results on regularized Fredholm determinants. ComplexCarrierCert packages the disk center, radius, the property that the disk lies inside the strip, and nonvanishing on the ball, lifting real-axis proofs from EulerInstantiation.lean.
proof idea
The proof is a one-line term that applies reflexivity to the definition of contourWinding, which is set directly to the constant zero for any valid cert and r inside the radius, encoding the vanishing of the Cauchy integral of C'/C.
why it matters
This result is invoked by euler_carrier_zero_winding to establish zero winding on disks D(σ₀, σ₀ − 1/2) for σ₀ > 1/2. It supplies the complex-analytic certification step required for the argument principle in the Recognition Science number-theoretic layer, supporting zero-free regions that connect to the phi-ladder and constants such as alpha inverse. It touches the open question of replacing the certificate with a full Mathlib contour-integral proof once infinite-product holomorphy API is available.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.