IndisputableMonolith.Verification.RecognitionStabilityAudit.Cayley
Defines the Cayley map from the closed right half-plane into the closed unit disk, together with a scaled variant theta used by the Recognition Stability Audit and its two-sided inverse. Analysts working on Herglotz positivity, phase caps, or RSA front-end pole-to-boundary arguments cite these maps. The module is definitional plus elementary complex-norm identities; no deep analysis is proved here.
claimThe module introduces the Cayley transform $c(z)=(z-1)/(z+1)$ (and a scaled form $\theta(J)=(2J-1)/(2J+1)$) sending $\{z:\operatorname{Re} z\ge 0\}$ into the closed unit disk, with inverse $\theta^{-1}$, plus the elementary identities $|c(z)|\le 1$ and $|\theta(J)|\le 1$ whenever the real part is nonnegative.
background
In complex analysis the classical Cayley transform conjugates the right half-plane to the unit disk. Recognition Science uses the same conjugation to turn Herglotz-type positivity (nonnegative real part) into a Schur-class bound (modulus at most one). That conversion is the geometric engine behind phase caps and the RSA "Cayley field".
This module sits under Verification / Recognition Stability Audit and only imports Mathlib. It packages the raw maps cayley and theta, the inverse invTheta, and the norm-square identities needed to prove $|c(z)|\le 1$ and $|\theta(J)|\le 1$ on $\operatorname{Re}\ge 0$. Downstream RSA text writes the Cayley field as $\Xi:=\theta\mathcal{J}=(2\mathcal{J}-1)/(2\mathcal{J}+1)$ for a sensor $\mathcal{J}=1/G$.
Foundation paper F4 (Schur pinch) likewise needs the half-plane $\leftrightarrow$ disk dictionary: phase bounds $|\arg z|<\pi/2$ become $\operatorname{Re} z>0$, which the Cayley map turns into a disk condition usable by Schur-type pinching.
proof idea
Definition module with short algebraic lemmas, not a single theorem chain. The Cayley and theta maps are introduced as rational functions; theta_eq_div records the explicit quotient form. Norm control proceeds from a norm-square identity comparing $|z+1|^2$ and $|z-1|^2$ (or the scaled $2J\pm 1$ analogues): nonnegativity of the real part makes the difference nonnegative, hence the image lies in the closed unit disk. Invertibility is by direct composition: invTheta_theta and theta_invTheta cancel the rational maps on the appropriate domains.
why it matters in Recognition Science
RSA FrontEnd imports this module to build the Cayley field $\Xi:=\theta\mathcal{J}$ and to convert a pole of the sensor $\mathcal{J}$ into a boundary hit $\Xi\to 1$. Core RSA and the SchurPinch foundation layer also import it, so every phase-cap / Herglotz / Cayley–Schur pinch argument in the monolith shares one definition of the half-plane-to-disk map.
Without a single, Mathlib-backed Cayley package, the F4 exclusion template and the RSA compiler front-end would each re-prove elementary disk bounds. The module therefore closes a small but shared scaffolding gap between foundation positivity and verification sensors. It does not itself state a Recognition forcing step (T0–T8); it supplies the complex-analytic dictionary those later arguments assume.
scope and limits
- Does not prove Herglotz representation or full Schur-class theory.
- Does not establish phase caps or the F4 pinch exclusion itself.
- Does not analyze poles of RSA sensors; only supplies the Cayley map.
- Does not address multipoint or operator-valued Cayley transforms.
- Does not claim uniqueness of the scaling in theta versus classical cayley.