contourWinding
The declaration defines the contour winding number of the Euler carrier function around an interior circle as the integer zero. Researchers in analytic number theory or complex analysis within Recognition Science cite it when establishing zero-winding certificates for holomorphic nonvanishing carriers on disks in the half-plane Re(s) > 1/2. The definition directly assigns the constant 0, encoding the argument principle result that the integral of C'/C vanishes by Cauchy's theorem.
claimFor a certificate $C$ of the complex Euler carrier (holomorphic and nonvanishing on a disk of positive radius inside the strip Re$(s) > 1/2$) and radius $r > 0$ inside that disk, the winding number of the contour around the circle of radius $r$ is defined to be the integer $0$.
background
The module upgrades the real-axis Euler carrier $C(s) = det_2(I - A(s))^2$ to a complex-analytic object holomorphic and nonvanishing on Re$(s) > 1/2$, with bounded logarithmic derivative on compact subsets. The referenced ComplexCarrierCert structure packages the disk center, radius (with radius_pos), disk_in_strip membership, nonvanishing on the ball, logDerivBound_val, and differentiableOn property; real-axis convergence and nonvanishing are lifted from EulerInstantiation.lean. Upstream results supply the real-axis proofs of convergence, nonvanishing, and log-derivative bounds that this certificate lifts to the complex setting.
proof idea
This is a direct definition that sets contourWinding to the constant 0. It encodes the standard complex-analysis fact that the winding number vanishes for zero-free holomorphic functions, via the argument principle and Cauchy's theorem applied to the logarithmic derivative.
why it matters in Recognition Science
The definition supplies the zero value consumed by the downstream theorems carrier_zero_winding and euler_carrier_zero_winding, which assert zero winding for any circle inside the certified disk D(σ₀, σ₀ - 1/2) when σ₀ > 1/2. It completes the complex upgrade step in the NumberTheory.EulerCarrierComplex module, linking to Recognition Science's use of holomorphic carriers for zeta-like objects and the zero-winding interface required by the sampled-trace layer. It touches the open question of full Mathlib contour-integral support for a future explicit proof.
scope and limits
- Does not evaluate an explicit contour integral.
- Does not apply when the carrier has zeros inside the disk.
- Does not extend the radius beyond the certificate's certified disk.
- Does not depend on specific numerical values of the carrier beyond the certificate fields.
Lean usage
theorem use_site (cert : ComplexCarrierCert) (r : ℝ) (hr : 0 < r) (hrR : r < cert.radius) : contourWinding cert r = 0 := rflformal statement (Lean)
95noncomputable def contourWinding (_cert : ComplexCarrierCert) (_r : ℝ) : ℤ := 0
proof body
Definition body.
96
97/-- The carrier has zero winding around every circle inside the disk.
98
99This is the content of the argument principle for zero-free holomorphic
100functions: `C` is holomorphic and nonvanishing on the disk, so `C'/C` is
101holomorphic there, and by Cauchy's theorem `∮ C'/C dz = 0`. Therefore the
102winding number is zero.
103
104The definition `contourWinding` is set to `0` directly, encoding this
105standard result. In a future version with full Mathlib contour-integral
106support, this would be proved by applying
107`circleIntegral_eq_zero_of_differentiable_on_off_countable` to `C'/C`. -/