ComplexCarrierCert
plain-language theorem explainer
The carrier certificate structure packages the center, radius, and analytic properties of the Euler carrier function on a disk inside the critical strip. Number theorists working on analytic properties of Euler products would cite this when lifting real-axis convergence results to the complex half-plane. The definition records the disk geometry and states the required holomorphic and nonvanishing properties as fields without deriving complex differentiability from scratch.
Claim. A structure consisting of a center $c$ in the complex numbers, a positive radius $r$, the assertion that the open disk of radius $r$ around $c$ lies inside the half-plane where the real part exceeds one half, the nonvanishing of the Euler carrier on that disk, a positive real bound on the absolute value of its logarithmic derivative, and a proposition asserting differentiability on the disk.
background
The module upgrades the real-axis Euler carrier from EulerInstantiation.lean to a complex-analytic object on the half-plane where the real part exceeds one half. The carrier is defined as the square of a regularized determinant and equals the product over primes of (1 minus p to the minus s) squared times the exponential of twice p to the minus s. It is holomorphic on that half-plane by local uniform convergence of the log-factor series, nonvanishing there, and equipped with bounded logarithmic derivative on compact subsets, following standard results on regularized Fredholm determinants.
proof idea
This is a structure definition with no proof body. The constructor supplies the fields for any real number greater than one half by setting the center to that number and the radius to the distance to the critical line, with the disk-containment and positivity fields discharged by linear arithmetic.
why it matters
This declaration supplies the interface consumed by the zero-winding theorem for the carrier and the zero-winding certificate structure. It completes the complex upgrade of the Euler carrier, enabling the argument principle application that yields zero winding number inside the disk. The declaration touches the scaffolding gap in complex-analysis infrastructure for infinite products.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.