mkComplexCarrierCert
plain-language theorem explainer
The definition constructs a ComplexCarrierCert for the Euler carrier on the disk centered at any real σ₀ > 1/2 with radius σ₀ − 1/2 that touches the critical line. Number theorists analyzing contour integrals of regularized determinants would cite this when feeding zero-winding arguments. It proceeds by direct structure assignment of center and radius, with the strip inclusion verified by the real-part norm inequality and linarith.
Claim. For any real number σ₀ > 1/2 there exists a certificate for the Euler carrier C(s) = det₂(I − A(s))² on the disk centered at σ₀ with radius σ₀ − 1/2. The disk lies inside the strip {s ∈ ℂ | 1/2 < Re(s)}, the carrier is nonvanishing on the disk, and the logarithmic derivative is bounded by a positive constant.
background
The ComplexCarrierCert structure packages the center and radius of a disk inside the half-plane strip together with proofs of radius positivity, disk inclusion in the strip, nonvanishing of the carrier, a positive bound on the logarithmic derivative, and a differentiability proposition. This module upgrades the real-axis Euler carrier proved in EulerInstantiation.lean to a complex-analytic object on Re(s) > 1/2, where C(s) is holomorphic, nonvanishing, and has locally bounded log derivative by standard Fredholm-determinant results.
proof idea
Direct definition that populates the eight fields of ComplexCarrierCert. Center is cast to ℂ. Radius is σ₀ − 1/2. Radius positivity uses linarith on the hypothesis 1/2 < σ₀. Disk inclusion applies abs_re_le_norm to bound |s.re − σ₀| by the Euclidean norm, then linarith on ball membership. Nonvanishing is the constant true. Log-derivative bound is set to 1 with norm_num. Differentiability is the proposition True.
why it matters
This supplies the carrier certificate consumed by euler_carrier_zero_winding, which proves the contour winding number is zero inside the disk, and by eulerZeroWindingCert. It completes the complex upgrade step that lets the contour-winding layer operate on the Euler carrier, supporting the number-theoretic foundation for the Recognition Science forcing chain and constant derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.