stripHalfPlane
plain-language theorem explainer
stripHalfPlane defines the open half-plane of complex numbers whose real part exceeds 1/2. Analysts lifting the Euler carrier C(s) = det₂(I − A(s))² from real-axis proofs to holomorphic domains would cite this set to delimit the region where local uniform convergence holds. The definition is a direct set comprehension with no lemmas or tactics required.
Claim. The open half-plane $S = { s ∈ ℂ | ½ < Re(s) }$.
background
The module upgrades the real-axis Euler carrier from EulerInstantiation.lean to a complex-analytic object on the half-plane Re(s) > 1/2. The carrier C(s) = det₂(I − A(s))² = ∏_p (1 − p^{-s})² exp(2p^{-s}) is holomorphic there because the log-factor series converges locally uniformly, nonvanishing as an exponential, and has bounded logarithmic derivative on compact subsets, following standard results on regularized Fredholm determinants.
proof idea
Direct set comprehension {s : ℂ | 1/2 < s.re} with no lemmas applied.
why it matters
The set is consumed by ComplexCarrierCert to record that a disk lies inside the half-plane and by mkComplexCarrierCert to build certificates for any σ₀ > 1/2. It supplies the domain for the complex lift of the Euler carrier, enabling contour-winding arguments in the Recognition framework while the real-axis convergence and nonvanishing remain in EulerInstantiation.lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.