invTheta_theta
plain-language theorem explainer
Left inverse for the paper-facing Cayley map on complex J-costs: composing the inverse transform after theta recovers J whenever 2J+1 is nonzero. RSA and RL audit proofs cite it when unwinding unit-disk sensors back to half-plane coordinates. The proof is a direct complex field calculation: clear denominators with field_simp, then finish by ring.
Claim. Let $\theta(J)=(2J-1)/(2J+1)$ and $\mathrm{inv}\theta(\xi)=\frac12\cdot(1+\xi)/(1-\xi)$. For every $J\in\mathbb{C}$ with $2J+1\neq 0$, one has $\mathrm{inv}\theta(\theta(J))=J$.
background
The Recognition Stability Audit repeatedly sends the closed right half-plane $\mathrm{Re}(z)\ge 0$ into the closed unit disk via Cayley-type maps. This module is the purely algebraic core of that plumbing from the RSA paper: the classical Cayley transform, a paper-facing rescaling of the cost variable, and its explicit inverse.
Here $\theta(J)=(2J-1)/(2J+1)$ is Cayley applied to $2J$, and $\mathrm{inv}\theta(\xi)=((1+\xi)/(1-\xi))/2$ is the algebraic inverse. The hypothesis $2J+1\neq 0$ is exactly the pole of $\theta$. Sibling lemmas record the division form of $\theta$, the norm bound $|\theta(J)|\le 1$ when $\mathrm{Re}(J)\ge 0$, and the matching right inverse.
proof idea
Unfold $\mathrm{inv}\theta$ and the division form of $\theta$. The only side condition is that the post-substitution denominator $1-\theta(J)$ is nonzero. That expression simplifies by field arithmetic to $2/(2J+1)$, which is nonzero because $2\neq 0$ and $2J+1\neq 0$ by hypothesis. With both denominators cleared, field_simp reduces the goal to a polynomial identity discharged by ring.
why it matters
RSA needs certified round-trips so disk-valued obstruction sensors can be rewritten in half-plane J-coordinates without information loss. Downstream, the RL audit module treats Cayley plumbing as an rsa_milestone and builds sensorOfObstruction on this layer. Together with the companion right-inverse identity, this lemma shows $\theta$ is bijective onto its image away from the pole. It is local algebra supporting the stability audit, not a step in the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.