euler_carrier_zero_winding
plain-language theorem explainer
Any σ₀ > 1/2 admits a complex Euler carrier holomorphic and nonvanishing on Re(s) > 1/2. The theorem asserts that this carrier has winding number zero around every circle of radius r centered at σ₀ whenever r < σ₀ - 1/2. Analytic number theorists working with regularized determinants and contour integrals cite the result to confirm absence of encirclements inside such disks. The argument is a direct instantiation of the general carrier zero-winding lemma on the Euler-specific certificate.
Claim. For any real number $σ_0 > 1/2$ and $r > 0$ with $r < σ_0 - 1/2$, the winding number of the complex Euler carrier $C(s) = ∏_p (1 - p^{-s})^2 exp(2 p^{-s})$ around the circle of radius $r$ centered at $σ_0$ is zero.
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 the square of the regularized determinant det₂(I - A(s)), equivalently the product over primes ∏_p (1 - p^{-s})^2 exp(2 p^{-s}). It is holomorphic and nonvanishing there, with bounded logarithmic derivative on compact subsets, by standard results on Fredholm determinants (Simon, Trace Ideals, Ch. 9). The real-axis versions appear in EulerInstantiation.lean; this module packages the complex lift as a certificate structure for the contour-winding layer.
proof idea
The proof is a one-line wrapper that applies the carrier zero winding lemma to the Euler carrier certificate constructed from mkComplexCarrierCert.
why it matters
This supplies the zero-winding certificate consumed by the sampled-trace layer. It completes the complex upgrade step from the real-axis Euler instantiation, enabling contour arguments in the number-theory pipeline. In the Recognition Science framework it supports holomorphic properties that underwrite the phi-ladder mass formulas, though it makes no direct reference to the forcing chain T0-T8 or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.