ZeroWindingCert
plain-language theorem explainer
ZeroWindingCert packages a disk center and positive radius with a ComplexCarrierCert and a guarantee that the carrier has zero winding number on every interior circle. Researchers constructing sampled traces or contour integrals over the Euler carrier cite this certificate to obtain charge-zero winding data. The definition is a direct field-copying wrapper that invokes the carrier_zero_winding lemma on the supplied certificate.
Claim. A zero-winding certificate consists of a center $c$ in the complex plane, a radius $r > 0$, a complex carrier certificate on the disk of that radius, matching conditions on center and radius, and the property that the contour winding number of the carrier is zero for every radius strictly between zero and $r$.
background
The module upgrades the real-axis Euler carrier to a complex-analytic object on the half-plane where the real part of $s$ exceeds 1/2. The carrier function is defined as $C(s) = det_2(I - A(s))^2 = prod_p (1 - p^{-s})^2 exp(2 p^{-s})$, holomorphic and nonvanishing on that half-plane with bounded logarithmic derivative on compact subsets. ComplexCarrierCert records a disk center, radius, membership in the strip, nonvanishing on the disk, and a logarithmic derivative bound. contourWinding abstracts the winding number as an integer associated to a carrier certificate and radius; for zero-free holomorphic carriers it evaluates to zero by the argument principle.
proof idea
The definition is a one-line wrapper that copies center, radius, and radius positivity from the input ComplexCarrierCert, sets the cert field to itself, records the trivial match via rfl, and assigns the zero_winding field to the result of carrier_zero_winding applied to the certificate.
why it matters
This structure supplies the interface between the complex carrier certificate and the contour-winding layer, feeding directly into zeroWindingFromCert and carrier_trace_charge_zero. It closes the loop from the Euler carrier's analytic properties to zero charge in sampled traces, supporting the defect floor argument that forces zero winding modes. It touches the open question of lifting the full differentiableOn property from Mathlib's infinite-product API.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.