goal_pole_implies_boundaryHit
plain-language theorem explainer
Sensor blow-up at a complex point forces the Cayley-transformed field to tend to 1 on the punctured neighborhood. Recognition Stability Audit users cite this when wiring a front-end pole into the compiled forbidden-event predicate. The proof is a single rsa_step that fires the whitelisted milestone linking sensor poles to boundary hits.
Claim. Let $\mathcal{J}:\mathbb{C}\to\mathbb{C}$ and $z_0\in\mathbb{C}$. If $\|\mathcal{J}(z)\|\to +\infty$ as $z\to z_0$ through the punctured neighborhood of $z_0$, then the Cayley field $z\mapsto\theta(\mathcal{J}(z))$ tends to $1$ at $z_0$ (again through the punctured neighborhood).
background
The Recognition Stability Audit (RSA) treats a complex sensor $\mathcal{J}$ as the front-end observable. Sensor blow-up at $z_0$ means $|\mathcal{J}(z)|$ tends to $+\infty$ along the punctured filter $\mathcal{N}[{z_0}^c]z_0$. The compiled forbidden event is a boundary hit: a field $\Xi$ tends to $1$ on that same punctured neighborhood.
RSA's paper-facing Cayley map is $\theta(J)=\mathrm{cayley}(2J)$. The core identity behind the implication is $\Xi(J)-1=-2/(2J+1)$, so $|2J+1|\to\infty$ whenever $|J|\to\infty$, forcing $\Xi\to 1$.
This file is the RL-facing layer of RSA: @[rsa_milestone] lemmas are the only nontrivial steps rsa_step may apply, and a small library of gold theorems (no sorry) trains the pipeline.
proof idea
One-line wrapper: rsa_step. That tactic tries assumption, then applies a whitelisted @[rsa_milestone] lemma (here the core front-end fact that sensor blow-up implies the Cayley field hits 1), discharges trivial subgoals, and falls back to the @[rsa_simp] whitelist if needed. No manual algebra appears in the proof body.
why it matters
This is a canonical training goal in the RSA RL module: it exercises the front-end half of the audit chain candidate $\Rightarrow$ sensor pole $\Rightarrow$ boundary hit. The Core definition of boundary hit is the compiled forbidden-event predicate ("candidate $\Rightarrow$ boundary hit, usually via sensor pole $\Rightarrow\Xi\to 1$"). Closing the pole-to-boundary step lets later milestones focus on obstruction-to-sensor and region-level audits. No downstream consumers are recorded yet; the declaration exists as a gold theorem for checklist completion and reward signal inside Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.