invTheta
plain-language theorem explainer
Defines the algebraic inverse of the paper-facing Cayley map: from a complex disk coordinate Ξ back to the half-plane variable J via J = ((1+Ξ)/(1-Ξ))/2. RSA and Cayley-plumbing proofs cite it whenever they round-trip between J and Ξ. The body is a one-line field formula, not a proved identity.
Claim. For $\Xi \in \mathbb{C}$, set the inverse paper-facing Cayley transform to $\frac{1}{2}\cdot\frac{1+\Xi}{1-\Xi}$. Equivalently, if $2J=(1+\Xi)/(1-\Xi)$, then $J$ is recovered by this formula.
background
The Recognition Stability Audit (RSA) repeatedly maps the closed right half-plane $\mathrm{Re}(z)\ge 0$ into the closed unit disk $|\cdot|\le 1$ by a Cayley transform. This module is the purely algebraic core of that plumbing (see the RSA paper).
Two paper-facing maps sit on top of the classical Cayley form $z\mapsto(z-1)/(z+1)$: the forward map $\theta(J)=(2J-1)/(2J+1)$, and this inverse, which solves $2J=(1+\Xi)/(1-\Xi)$ for $J$. The half-plane variable is the cost-like coordinate used in stability statements; the disk coordinate is the bounded sensor variable.
No upstream lemmas are required: the definition is self-contained complex arithmetic.
proof idea
Not a proof: a noncomputable definition whose body is the explicit field expression $((1+\Xi)/(1-\Xi))/2$. Downstream round-trip theorems discharge the denominators $1-\Xi\ne 0$ and $2J+1\ne 0$ by direct field_simp algebra.
why it matters
Gives the explicit inverse needed to close Cayley round-trips in RSA. Immediate parents are the local identities invTheta_theta and theta_invTheta (left and right inverses under the obvious non-vanishing hypotheses). Those identities are re-exported as RL micro-goals (goal_invTheta_theta, goal_theta_invTheta), so the definition is a training target in the RSA pipeline: small, checkable algebraic progress toward stability audit lemmas.
It does not itself touch the forcing chain (T0–T8), RCL, or the $\varphi$-ladder; it is infrastructure for the half-plane/disk dictionary used when RSA bounds recognition cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.