theta_invTheta
plain-language theorem explainer
The paper-facing Cayley map is a left inverse of its explicit algebraic inverse on ℂ away from the pole at 1. Anyone wiring Recognition Stability Audit sensors through the unit-disk chart cites this identity. The argument is direct field arithmetic: unfold both closed forms, clear denominators, and cancel.
Claim. For every $\Xi \in \mathbb{C}$ with $\Xi \neq 1$, if $\theta(J) = (2J-1)/(2J+1)$ and $\mathrm{inv}\,\theta(\Xi) = ((1+\Xi)/(1-\Xi))/2$, then $\theta(\mathrm{inv}\,\theta(\Xi)) = \Xi$.
background
The Recognition Stability Audit (RSA) repeatedly maps the closed right half-plane $\mathrm{Re}(z)\ge 0$ into the closed unit disk via a Cayley transform. This module is the purely algebraic core of that plumbing, matching the setup in Recognition_Stability_Audit.tex.
Two paper-facing maps are fixed here. The forward chart is $\theta(J)=\mathrm{cayley}(2J)=(2J-1)/(2J+1)$. Its explicit inverse is $\mathrm{inv},\theta(\Xi)=((1+\Xi)/(1-\Xi))/2$, obtained by solving $2J=(1+\Xi)/(1-\Xi)$ for $J$. The pole of the inverse sits at $\Xi=1$, which is exactly the hypothesis of this lemma.
A simp lemma records the closed quotient form of $\theta$, so downstream algebra can avoid expanding through the intermediate $\mathrm{cayley}$ definition.
proof idea
Term-mode style tactic proof by direct algebra. First rewrite the hypothesis $\Xi\neq 1$ into $1-\Xi\neq 0$ so the inverse denominator is admissible. Unfold $\theta$ via its quotient form and unfold the inverse definition. Clear the remaining field denominators with that non-vanishing fact, then finish by ring cancellation. No external analytic lemmas are required.
why it matters
RSA treats these Cayley identities as small, self-contained training targets in the verification pipeline: each gives immediate, checkable progress before heavier analytic estimates. The sibling composition the other way (inverse after forward map) sits beside this one; together they certify that the paper-facing chart is algebraically invertible off the pole.
Downstream, the RL audit layer marks Cayley plumbing as an explicit milestone and consumes the chart when building obstruction sensors. Without left-invertibility of the inverse map, sensor values pulled back from the disk chart would not recover the original complex obstruction coordinate. This is pure verification scaffolding for RSA, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.