cayley
plain-language theorem explainer
The Cayley transform sends z to (z-1)/(z+1), mapping the closed right half-plane into the closed unit disk. RSA and Schur-pinch arguments cite it as the algebraic bridge from Herglotz (nonnegative real part) data to Schur (contractive) data. The declaration is a one-line definitional equation with no proof obligations.
Claim. For $z \in \mathbb{C}$, define the Cayley transform by $\mathrm{Cayley}(z) = \frac{z-1}{z+1}$. This Möbius map sends the closed right half-plane $\operatorname{Re} z \ge 0$ into the closed unit disk $\|w\| \le 1$ (away from the pole $z = -1$).
background
The Recognition Stability Audit (RSA) repeatedly converts half-plane positivity into disk contractivity. This module is the purely algebraic core of that pipeline: it isolates the Cayley map, a paper-facing rescaling theta, and the explicit inverse, as small self-contained lemmas.
Classically, $\mathrm{Cayley}(z)=(z-1)/(z+1)$ is the Möbius transformation carrying the right half-plane to the unit disk. In RSA it is the primitive used to prove $|\mathrm{Cayley}(z)|\le 1$ whenever $\operatorname{Re} z\ge 0$. A sibling form in the Schur-pinch layer, $(2H-1)/(2H+1)$, is exactly this map applied to $2H$, so the audit definition is the common algebraic engine.
Downstream lemmas also introduce the paper-facing variant $\theta(J)=(2J-1)/(2J+1)$ and its inverse, both built from the same Möbius skeleton.
proof idea
Pure definition: the body is the single term $(z-1)/(z+1)$. No tactics, no lemmas, no obligations. Downstream proofs unfold this equation and work with complex norm-squared identities.
why it matters
This definition is the shared algebraic primitive for the RSA Cayley plumbing and for the Schur-pinch layer. Local consumers include the identity $|z+1|^2-|z-1|^2=4\operatorname{Re} z$ and the half-plane bound $|\mathrm{Cayley}(z)|\le 1$ when $\operatorname{Re} z\ge 0$. The Schur-pinch module reuses it (via the $2H$ rescaling) to prove F4.1.3: Cayley of a point with nonnegative real part has modulus at most one, and therefore Cayley composed with a Herglotz function is Schur wherever the denominator is nonzero.
That half-plane-to-disk step feeds the master pinch hypotheses (F4.3.4): Herglotz data, non-cancellation at candidate poles, and a strict interior Cayley normalization together force the pole set in the domain to be empty. In short, the definition is the Möbius hinge between positivity and contractivity throughout the stability audit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.