goal_theta_eq_div
plain-language theorem explainer
For any complex cost $J$, the paper-facing Cayley map sends $J$ to $(2J-1)/(2J+1)$. Anyone auditing the RSA Cayley interface or training an RL agent on the whitelist tactics would cite this. The proof is a single `rsa_step` that closes by unfolding the definition against whitelisted simp lemmas.
Claim. For every $J\in\mathbb{C}$, the paper-facing Cayley transform satisfies $\theta(J)=\dfrac{2J-1}{2J+1}$.
background
The Recognition Stability Audit (RSA) package exposes a paper-facing Cayley transform on complex costs: $\theta(J):=\mathrm{cayley}(2J)$. With the standard Cayley map $\mathrm{cayley}(z)=(z-1)/(z+1)$, this expands at once to $(2J-1)/(2J+1)$. The inverse map is $\mathrm{inv}\Theta(\Xi)=((1+\Xi)/(1-\Xi))/2$, recovering $J$ from the transformed coordinate $\Xi$.
This file is the RL harness for RSA inside Lean. Lemmas tagged @[rsa_simp] form a whitelist for a restricted simp; lemmas tagged @[rsa_milestone] may be applied by the bounded tactic rsa_step. A small library of proved gold goals (no sorry) trains and scores agents that propose those tactics.
The present goal is one of those gold checks: it only asks that the definition of $\theta$ match the explicit rational formula used in the paper.
proof idea
One-line wrapper: rsa_step. That tactic tries assumption, then milestone apply, then falls back to rsa_simp on the @[rsa_simp] whitelist. Unfolding $\theta(J)=\mathrm{cayley}(2J)$ and simplifying the Cayley formula yields $(2J-1)/(2J+1)$ with no further lemmas.
why it matters
This is a canonical training goal in the RSA RL module, not a deep physics theorem. It pins the paper-facing Cayley interface so that later gold goals (goal_theta_invTheta, goal_invTheta_theta, pole/boundary and obstruction-to-sensor goals) can treat $\theta$ as the explicit Möbius map $(2J-1)/(2J+1)$ without re-proving the expansion. Downstream stability and sensor-blowup audits rely on that identification when they move between the cost coordinate $J$ and the Cayley coordinate $\Xi$. In the broader Recognition framework the Cayley chart is the bridge between the $J$-cost language of the forcing chain and complex analysis used in the stability audit; this lemma is the first checklist item that the RL pipeline can close automatically.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.