XiSchurNoPolesPrinciple
plain-language theorem explainer
The definition packages the analytic claim that Schur contractivity of the xi-sensor Cayley field on the right half-strip implies the critical-strip zero-free bridge. Analysts pursuing the Pick positivity route to the Riemann hypothesis would cite it as the removable-singularity step converting an algebraic bound into zero exclusion. It is introduced directly as the implication between the Schur proposition and the bridge proposition, with no further reduction.
Claim. Let $X:ℂ→ℂ$ be an abstract xi-sensor Cayley field. The principle asserts that if $‖X(s)‖≤1$ for all $s$ in the right half-strip, then the critical-strip zero-free bridge holds.
background
The XiSensorPickPositivity module targets Pick/Schur positivity for the xi-sensor Cayley field as the route that avoids assuming bounded defect cost (already RH-equivalent). The field is the abstract map $X(s)=(2(ξ'/ξ)(s)-1)/(2(ξ'/ξ)(s)+1)$, kept as any conformal chart into the unit disk. SchurOnRightHalfStrip requires the pointwise bound $‖X(s)‖≤1$ on the right half-strip. CriticalStripZeroFreeBridge is the named target Nonempty CriticalStripZeroFree, which the Riemann hypothesis implies by making the open right half-strip zero-free. The module doc states that the algebraic facts are now in place and the remaining analytic step is precisely this exclusion of poles of ξ'/ξ.
proof idea
This is a one-line definition that directly sets the principle equal to the implication SchurOnRightHalfStrip X → CriticalStripZeroFreeBridge. No lemmas are applied and no tactics are used; the body simply names the analytic claim for downstream use.
why it matters
The definition supplies the analytic link that closes the xi-sensor Pick route. It is applied in the theorem criticalStripBridge_of_pickPositive to obtain CriticalStripZeroFreeBridge from finite Pick positivity together with this principle. It also appears in the XiSensorPickRouteStatus structure as the schur_to_zero_free_open component. Within the Recognition framework this step converts the algebraic Schur bound into exclusion of zeta zeros off the critical line, supporting the number-theoretic formalization of the Riemann hypothesis. The open question it leaves is whether the Schur bound itself follows from the xi-sensor construction without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.