schur_pinch
plain-language theorem explainer
The schur_pinch theorem shows that if J is differentiable with nonnegative real part on an open connected set U minus an isolated set Z, the Cayley transform theta o J satisfies |theta(J(s))| < 1 at one point, and |J(s)| tends to infinity at points of Z, then Z must be empty inside U. Complex analysts formalizing the Riemann hypothesis via Pick functions and Schur bounded analytic functions would cite this closure result. The proof proceeds by contradiction: it establishes a bounded holomorphic extension of theta o J across the punctures and de
Claim. Let $U$ be an open connected subset of the complex plane and let $Z$ be a set of isolated points in $U$. Let $J$ be differentiable on $U$ minus $Z$ with real part nonnegative on that domain. Assume that the norm of $J(s)$ tends to infinity as $s$ approaches any point of $Z$, and that there exists a point $s_0$ in $U$ minus $Z$ such that the norm of the Cayley transform applied to $J(s_0)$ is strictly less than one. Then $Z$ is empty inside $U$.
background
In Recognition Science the function J maps to the right half-plane under the nonnegativity assumption and is given explicitly by $J(x) = (x + x^{-1})/2 - 1$. The module recasts the Riemann Hypothesis as persistence of the Pick spectral gap for this J on the Euler region. The Cayley transform theta, defined by theta(z) = (2z - 1)/(2z + 1), sends the right half-plane to the unit disk and converts the real-part condition into a bounded holomorphic function. The local setting is the formalization of RH via gap persistence, where positivity of the gap in the Euler region implies absence of zeros off the critical line. Upstream lemmas include norm_theta_le_one_of_re_nonneg from BRFPlumbing (which converts Re J >= 0 into |theta o J| <= 1) and theta_comp_differentiableOn together with max_modulus_constant from the same module.
proof idea
The proof is by contradiction. Assume Z cap U is nonempty and extract a point rho. The hypothesis Re J >= 0 plus norm_theta_le_one_of_re_nonneg immediately gives |theta o J| <= 1 on U minus Z. Differentiability of theta o J on the punctured domain follows from theta_comp_differentiableOn, using that 2J + 1 never vanishes. The nontrivial point where the norm is strictly less than one is taken from the given existential. An algebraic identity theta(z) = 1 - 2/(2z + 1) shows that the norm tends to 1 as |z| tends to infinity. Combined with the pole condition that |J(s)| tends to infinity, any continuous extension must attain norm 1 at rho. Removable-singularity infrastructure extends the bounded holomorphic function to all of U. The maximum-modulus lemma then forces the norm to be strictly less than one everywhere, contradicting the value 1 at rho.
why it matters
This supplies the analytic closure for the Schur pinch inside the Pick-gap persistence route to the Riemann Hypothesis. It is invoked directly by BWD3Model and feasible_implies_boolean in the Complexity.SAT.BWD3SchurPinch module to guarantee that admissible linear witnesses are Boolean. Within the present module it feeds pick_gap_persistence_implies_RH, which is listed as fully proved. In the Recognition Science chain it supports the step from J-uniqueness (T5) and the eight-tick octave (T7) to the implication that gap persistence forces the critical-line location of zeros, consistent with the phi-ladder mass formula and the alpha band in RS-native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.