HalfStripDiskChart
plain-language theorem explainer
A structure abstracting any map from the open right half-strip (1/2 < Re(s) < 1) into the open unit disk. Analysts pursuing the Pick/Schur route to zero-free regions for the xi function cite this interface to state chart assumptions on the Cayley field. The declaration is a bare structure definition with a single map field and the disk-mapping axiom.
Claim. A map $φ:ℂ→ℂ$ such that $∀s∈ℂ$, if $1/2<Re(s)<1$ then $‖φ(s)‖<1$. This supplies an abstract conformal chart sending the open right half of the critical strip into the unit disk.
background
The right half-strip is defined by the predicate 1/2 < Re(s) < 1. The module develops algebraic positivity statements for an abstract xi-sensor Cayley field X(s) obtained by sending the logarithmic derivative of xi through the Cayley transform. The local goal is to derive the pointwise Schur bound on the right half-strip from finite Pick positivity without assuming bounded defect cost.
proof idea
Structure definition. The maps_to_disk field directly encodes the required strict contraction into the unit disk; no tactics or lemmas are applied.
why it matters
Supplies the chart interface required by schur_of_finitePickPositive, schur_of_onePointPickPositive, and criticalStripBridge_of_pickPositive. These close the algebraic half of the Pick/Schur positivity argument that would exclude poles of xi'/xi from the right half-strip. The missing analytic step remains the passage from the Schur bound to the zero-free region.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.