cayley
plain-language theorem explainer
The Cayley transform maps the right half-plane to the closed unit disk by the formula (H-1)/(H+1). Researchers pursuing the Riemann Hypothesis via the bounded-real-function and Schur-class route cite this algebraic definition as the unconditional bridge from Herglotz to Schur functions. It is implemented as a direct one-line definition with no lemmas or tactics.
Claim. The map sending $H$ to $(H-1)/(H+1)$ carries the closed right half-plane to the closed unit disk.
background
In Recognition Science the shifted cost is $H(x)=J(x)+1=½(x+x^{-1})$, where $J$ satisfies the Recognition Composition Law. The present module isolates the purely algebraic Cayley-Schur step of the BRF route to the Riemann Hypothesis. A function is Herglotz when $0≤Re H$ and its Cayley image is Schur when the norm is at most 1. Upstream CostAlgebra.H supplies the explicit form $H(x)=J(x)+1$ while FunctionalEquation.H reparametrizes the d'Alembert identity.
proof idea
One-line definition that directly encodes the standard Cayley transform formula.
why it matters
This supplies the algebraic link from Re $H≥0$ to ‖Θ‖≤1 that is invoked by norm_cayley_le_one_of_re_nonneg, by theta (the BRF-specific variant), and by schur_pinch to close the Pick-gap argument. The step is fully unconditional and algebraic, consistent with T5 J-uniqueness and the eight-tick octave. It touches the open question whether the resulting Schur pinch forces the critical strip to be zero-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.