schur_of_finitePickPositive
plain-language theorem explainer
Finite Pick positivity for the xi-sensor Cayley field on a right half-strip chart implies the pointwise Schur contractivity bound. Number theorists formalizing zero-free regions via Pick matrices would cite this algebraic reduction. The proof is a one-line wrapper that extracts the embedded one-point positivity hypothesis and applies the corresponding Schur theorem.
Claim. Let $C$ be a conformal chart from the right half-strip to the open unit disk and let $X$ be the xi-sensor Cayley field. If the one-point Pick positivity condition holds for $X$ under $C$, then $|X(s)|$ is at most 1 for every $s$ in the right half-strip.
background
The module develops an algebraic route to the Riemann hypothesis by establishing Pick positivity for the xi-sensor Cayley field $X(s) = (2 (xi'/xi)(s) - 1) / (2 (xi'/xi)(s) + 1)$. A HalfStripDiskChart is an abstract conformal map sending the right half-strip into the open unit disk. FinitePickPositive packages the one-point positivity hypothesis together with a placeholder for finite-matrix conditions. SchurOnRightHalfStrip asserts that $X$ maps the right half-strip into the closed unit disk. The module documentation states that the unconditional route should not assume bounded defect cost and that the right target is Pick/Schur positivity for the xi-sensor Cayley field.
proof idea
The proof is a one-line wrapper that applies schur_of_onePointPickPositive to the one_point component of the FinitePickPositive hypothesis.
why it matters
This theorem is invoked inside criticalStripBridge_of_pickPositive, which combines the resulting Schur bound with the XiSchurNoPolesPrinciple to obtain a CriticalStripZeroFreeBridge. It supplies the algebraic link between finite positivity and the Schur bound, advancing the Pick/Schur route that excludes poles of xi'/xi in the right half-strip. The module notes that the analytic removable-singularity step remains missing. In the Recognition framework it contributes to the number-theoretic component of the forcing chain that derives three spatial dimensions and the golden-ratio constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.