goal_theta_invTheta
plain-language theorem explainer
Left inverse for the paper-facing Cayley pair on the complex plane: applying the Cayley map after its inverse recovers every ξ away from the pole at 1. Anyone auditing the RSA Cayley dictionary or the RL gold-goal suite would cite it. The proof is a single rsa_step that applies a whitelisted milestone and closes.
Claim. For every $\xi \in \mathbb{C}$ with $\xi \neq 1$, $\theta(\theta^{-1}(\xi)) = \xi$, where $\theta(J) = \mathrm{cayley}(2J)$ is the paper-facing Cayley transform and $\theta^{-1}(\xi) = \tfrac12 \frac{1+\xi}{1-\xi}$.
background
The Recognition Stability Audit (RSA) uses a paper-facing Cayley dictionary between a cost-like coordinate $J$ and a sensor/obstruction coordinate $\Xi$. The forward map is $\theta(J) := \mathrm{cayley}(2J)$; its algebraic inverse is $\mathrm{invTheta}(\Xi) := \tfrac12 \frac{1+\Xi}{1-\Xi}$, which is undefined at the pole $\Xi = 1$ (the image of the Cayley pole under the $2J$ scaling).
This file is the RSA Reinforcement Learning module. It exposes a whitelist of simp lemmas (@[rsa_simp]) and milestone lemmas (@[rsa_milestone]), plus bounded tactics rsa_simp and rsa_step, so an external agent can propose steps and receive Lean reward on goal closure. The present declaration is one of the canonical proved gold goals that exercise that pipeline.
(The Bloch-cell phase also named theta in Gravity.Analysis is a different object; the Cayley theta/invTheta pair is the one used here.)
proof idea
One-line tactic proof: a single rsa_step. That tactic tries assumption, then applies a whitelisted @[rsa_milestone] lemma for the Cayley left-inverse identity, discharges trivial side conditions (here $\xi \neq 1$), and falls back to rsa_simp if needed. No manual algebraic expansion appears in the proof body.
why it matters
Closes the left-inverse half of the Cayley micro-goal pair (the sibling right-inverse is invTheta ∘ theta = id on $J$). Together they certify that the paper-facing Cayley dictionary is bijective away from the pole, which RSA uses when translating boundary hits, Schur-type conditions, and sensor blow-ups between $J$ and $\Xi$ coordinates.
In the RL setting this is a gold training theorem: zero sorry, short closed proof under the restricted tactic API. Downstream used-by edges are empty in the graph snapshot, so its immediate role is checklist completion and agent reward rather than a named parent theorem. It sits in the Verification domain, not on the T0–T8 forcing chain, but it underwrites stable use of the Cayley bridge wherever RSA audits recognition cost against complex sensors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.