XiFromSensor
plain-language theorem explainer
Convenience map sending a complex sensor 𝓙 to the paper-facing Cayley field Ξ by pointwise RSA Cayley transform. Anyone packaging an RSA problem instance uses it to turn 𝓙 into Ξ. The body is the one-line lambda Ξ(z) = θ(𝓙(z)).
Claim. Given a sensor $\mathcal{J}:\mathbb{C}\to\mathbb{C}$, define the associated Cayley field by $\Xi(z)=\theta(\mathcal{J}(z))$, where $\theta$ is the RSA Cayley transform $\theta(J)=\mathrm{cayley}(2J)$ (equivalently $\Xi=(2\mathcal{J}-1)/(2\mathcal{J}+1)$ after pullback).
background
The Recognition Stability Audit (RSA) is a compiler: front-end turns a candidate existence claim into a boundary-hit condition for a bounded Cayley field $\Xi$; back-end certifies that $\Xi$ stays Schur-class on the audited region; correctness then rules the candidate out. This module is the RL-friendly core interface for that pipeline (structures as checklists of obligations).
RSA rests on the canonical reciprocal cost $J(x)=\tfrac12(x+x^{-1})-1$ on $\mathbb{R}_{>0}$ (formalized as Jcost); uniqueness is not re-proved here. The paper-facing Cayley transform is $\theta(J)=\mathrm{cayley}(2J)$. An RSA problem instance packages an audited region $\Omega$, a candidate predicate, and the Cayley field $\Xi$ to certify.
This definition is the standard bridge from a sensor $\mathcal{J}$ to that $\Xi$ field: pointwise $\theta\circ\mathcal{J}$.
proof idea
Pure definition, not a proof. The body is the lambda $z\mapsto\theta(\mathcal{J}(z))$, applying the upstream RSA Cayley transform theta pointwise to the sensor. No tactics, no lemmas beyond that composition.
why it matters
Gives the canonical packaging of a sensor into the paper-facing field $\Xi$ that every RSA problem instance audits. Downstream, Problem_XiFromSensor_def is the @[rsa_simp] unfold equating this map to $z\mapsto\theta(\mathcal{J}(z))$, so front-end encodings and RL-facing checklists can rewrite through it cleanly.
In the RSA compiler picture, front-end obligations compile candidate $\Rightarrow$ sensor pole $\Rightarrow\Xi\to 1$ (boundary hit). Without a fixed $\Xi$-from-sensor constructor, those obligations would each re-inline the Cayley composition. The definition sits at the cost layer interface: it references $J$/Cayley without reopening T5 J-uniqueness or the RCL, keeping the audit pipeline focused on Schur certificates and boundary hits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.