goal_invTheta_theta
plain-language theorem explainer
Left inverse for the paper-facing Cayley map on complex cost: applying the inverse transform after the forward map recovers J whenever 2J+1 is nonzero. Cited by anyone wiring RSA sensor/boundary goals to the J-cost coordinate. Proof is a single rsa_step against the milestone/simp whitelist.
Claim. For every $J \in \mathbb{C}$ with $2J+1 \neq 0$, if $\theta$ is the paper-facing Cayley transform and $\mathrm{inv}\,\theta(\Xi)=((1+\Xi)/(1-\Xi))/2$ is its inverse, then $\mathrm{inv}\,\theta(\theta(J))=J$.
background
The Recognition Stability Audit (RSA) tracks when a compiled sensor blows up and when a boundary is hit. The paper-facing Cayley pair moves between the complex cost coordinate $J$ and a bounded sensor coordinate $\Xi$. The inverse is defined by $\mathrm{inv},\theta(\Xi)=((1+\Xi)/(1-\Xi))/2$, so that $2J=(1+\Xi)/(1-\Xi)$; the matching forward map is $\theta(J)=(2J-1)/(2J+1)$, which needs the pole guard $2J+1\neq 0$.
This file is the RL front-end for RSA inside Lean: @[rsa_simp] and @[rsa_milestone] tag the only lemmas the custom tactics may use, and a small library of gold goals (no sorry) trains an agent that proposes rsa_step / rsa_simp. The present declaration is one of those micro-goals, paired with the opposite composition theta (invTheta Ξ) = Ξ under the dual non-pole hypothesis.
proof idea
One-line tactic proof: rsa_step. That tactic tries assumption, then applies a single @[rsa_milestone] lemma (discharging trivial side goals), then falls back to rsa_simp on the @[rsa_simp] whitelist. Algebraically the goal is the left-inverse identity for the Cayley pair once the denominator $2J+1$ is known nonzero; the whitelist is expected to unfold invTheta/theta and cancel.
why it matters
Closes the left-inverse half of the Cayley micro-goal pair used to connect RSA sensor coordinates back to the Recognition cost $J$. In the broader framework $J$ is the unique cost forced by the Recognition Composition Law and T5 ($J(x)=(x+x^{-1})/2-1$). Downstream RSA goals (pole implies boundary hit; obstruction implies sensor blow-up) sit on the same Cayley chart; this identity is the algebraic sanity check that the chart is invertible on its domain. No external used-by edges yet: it is a canonical training target for the RL pipeline rather than a lemma consumed by physics modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.