IndisputableMonolith.Verification.RecognitionStabilityAudit.Cayley
Defines the Cayley transform and a scaled variant that send the closed right half-plane into the closed unit disk, with an inverse. Recognition Stability Audit and the F4 Schur-pinch stack import this as the holomorphic map from a positive-real sensor to a contractive field. The module is mostly elementary complex arithmetic: norm identities, Re-nonneg contractivity, and inverse laws.
claimThe Cayley map $c(z)=(z-1)/(z+1)$ and the scaled field $\theta(J)=(2J-1)/(2J+1)$ send $\{\operatorname{Re} z\ge 0\}$ into the closed unit disk. Norm-square identities and $\|c(z)\|\le 1$, $\|\theta(J)\|\le 1$ under nonnegative real part are recorded, together with a two-sided inverse $\theta^{-1}$.
background
Classical complex analysis maps the open right half-plane biholomorphically onto the open unit disk by the Cayley transform $z\mapsto(z-1)/(z+1)$. The closed half-plane lands in the closed disk, with the imaginary axis sent to the unit circle (away from the pole at $-1$).
In the Recognition Stability Audit, a holomorphic sensor $J$ (often $1/G$ for an obstruction $G$) is converted to a Cayley field $\Xi:=\theta(J)=(2J-1)/(2J+1)$. Contractivity of $\theta$ on $\operatorname{Re} J\ge 0$ turns positivity or Herglotz-type hypotheses into disk-valued bounds used by phase caps and boundary-hit arguments.
The module sits under Verification and is imported by the RSA core/front-end and by Foundation.SchurPinch (F4: phase bounds, Herglotz positivity, Cayley–Schur pinch exclusion).
proof idea
Definition module with short supporting lemmas, not a single deep theorem. It introduces cayley and the scaled theta, records the algebraic identity relating $|z+1|^2-|z-1|^2$ to the real part, and deduces $|\mathrm{cayley}(z)|\le 1$ and $|\theta(J)|\le 1$ whenever $\operatorname{Re}\ge 0$. Inverse maps invTheta with the two composition identities close the dictionary between half-plane and disk coordinates. Arguments are direct expansions in $\mathbb{C}$, not heavy analysis.
why it matters in Recognition Science
RSA FrontEnd builds the Cayley field $\Xi:=\theta J$ and uses pole-to-boundary behavior ($J$ blows up $\Rightarrow$ $\Xi\to 1$) as the sensor-to-boundary step of the audit compiler. RSA Core imports the same primitives as the Lean home for the Recognition Stability Audit manuscript. Foundation.SchurPinch (paper F4) uses the half-plane/disk dictionary for phase caps ($|\arg z|<\pi/2\Rightarrow\operatorname{Re} z>0$) and the Cayley–Schur pinch exclusion template. Without a verified contractive Cayley map, those positivity-to-disk reductions stay informal.
scope and limits
- Does not prove Herglotz representation or full Schur-product theorems.
- Does not establish RSA obstruction or sensor axioms; only the Cayley map.
- Does not treat the pole at $-1$ beyond the usual domain restriction.
- Does not derive physical constants, mass ladders, or forcing-chain steps T0–T8.
- Does not claim uniqueness of the Cayley normalization among all disk maps.