SchurOnRightHalfStrip
plain-language theorem explainer
SchurOnRightHalfStrip defines the contractivity property that an abstract xi-sensor Cayley field maps every point of the right half-strip into the closed unit disk. Researchers formalizing the Riemann hypothesis via Pick positivity on the xi function would cite this bound as the algebraic target of one-point and finite positivity assumptions. The definition consists of the direct pointwise norm inequality over the open right half-strip.
Claim. Let $X : {C} {to} {C}$ be an abstract xi-sensor Cayley field. The field satisfies the Schur bound on the right half-strip when $||X(s)|| {leq} 1$ for every complex $s$ with $frac{1}{2} < {Re}(s) < 1$.
background
The right half-strip is the open set of complex numbers whose real part lies strictly between one half and one. The xi-sensor Cayley field is the abstract map $X(s) = frac{2 (xi'/xi)(s) - 1}{2 (xi'/xi)(s) + 1}$, kept as a general function from $C$ to $C$ so that any conformal chart into the unit disk may be substituted. The module develops algebraic consequences of Pick positivity for this field on the unconditional route to the Riemann hypothesis, without assuming bounded defect cost. The definition follows immediately after the local predicates RightHalfStrip and XiCayleyField.
proof idea
The declaration is the direct definition of the pointwise Schur contractivity condition. It simply requires the norm of the Cayley field to be at most one at every point of the right half-strip.
why it matters
This definition supplies the target property for the theorems schur_of_onePointPickPositive and schur_of_finitePickPositive. It enters the structure XiSensorPickRouteStatus as the conclusion of the pick-to-schur implication. The downstream XiSchurNoPolesPrinciple then uses the bound to conclude absence of poles for the logarithmic derivative, which would exclude zeros of the zeta function in the critical strip. The module documentation identifies the bound as the first nontrivial algebraic fact required by the Pick route.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.