Problem_XiFromSensor_def
plain-language theorem explainer
Unfolds the sensor-to-Cayley field map: the audited field built from a complex sensor 𝓙 is pointwise the RSA Cayley transform of 𝓙(z). Cited by anyone simplifying RSA problem instances under the rsa_simp whitelist. Proof is pure definitional equality (rfl).
Claim. For any sensor $\mathcal{J}:\mathbb{C}\to\mathbb{C}$, the Cayley field obtained from that sensor equals $z\mapsto \theta(\mathcal{J}(z))$, where $\theta$ is the paper-facing Cayley map $\theta(J)=\mathrm{cayley}(2J)$.
background
Recognition Stability Audit (RSA) packages an audit as a Problem: a region $\Omega\subseteq\mathbb{C}$, a candidate predicate to rule out on $\Omega$, and an audited Cayley field $\Xi$. In the paper, $\Xi$ is the pullback of $(2\mathcal{J}-1)/(2\mathcal{J}+1)$.
The convenience constructor builds that field from a sensor $\mathcal{J}$ by composing with RSA's Cayley transform $\theta(J)=\mathrm{cayley}(2J)$. (A same-named theta in Bloch-cell gravity is unrelated cell phase; the dependency here is the Cayley theta.)
This module is the RL front-end for RSA: @[rsa_simp] tags whitelisted unfold/rewrite lemmas for the restricted rsa_simp tactic used in training goals.
proof idea
One-line definitional proof: rfl. The statement is exactly the body of the sensor-to-field constructor, so both sides are definitionally equal and need no lemmas beyond the definition.
why it matters
Gives the RL/simp layer a named, tagged unfold for the sensor-built Cayley field so rsa_simp can expose $\theta(\mathcal{J},z)$ without opening the full Problem API. No downstream theorems currently depend on it; it is infrastructure for canonical training goals and milestone steps in the RSA reinforcement-learning pipeline, not a physics forcing step (T0–T8). It keeps paper notation $\Xi$ aligned with the Lean Cayley field during automated audits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.