boundaryHit_theta_of_sensorBlowsUp
plain-language theorem explainer
If a complex sensor field has norm tending to infinity on a punctured neighborhood of z0, its Cayley transform tends to 1 there. Recognition Stability Audit cites this to turn obstruction poles into Cayley boundary hits. The argument is a filter calculation: reverse triangle inequality sends the denominator to infinity, inversion yields zero, and the identity Ξ(J)−1=−2/(2J+1) finishes the limit.
Claim. Let $\mathcal{J}:\mathbb{C}\to\mathbb{C}$ and $z_0\in\mathbb{C}$. Suppose $\|\mathcal{J}(z)\|\to+\infty$ as $z\to z_0$ along the punctured neighborhood of $z_0$. Then $\theta(\mathcal{J}(z))\to 1$ along that same punctured neighborhood, where $\theta(w)=(2w-1)/(2w+1)$ is the Cayley field map.
background
The Recognition Stability Audit front-end formalizes a four-step pipeline from the manuscript: an obstruction $G$ (holomorphic stand-in for a defect or claim), a sensor $\mathcal{J}:=1/G$, the Cayley field $\Xi:=\theta\circ\mathcal{J}$ with $\theta(w)=(2w-1)/(2w+1)$, and the implication that a sensor blow-up forces $\Xi\to 1$ on the punctured neighborhood.
"Pole" is deliberately phrased as a pure norm blow-up: $|\mathcal{J}(z)|\to+\infty$ along the filter $\mathcal{N}{z_0}^c$. That is strong enough for RSA and avoids meromorphic machinery at the interface layer; domain instantiations may later strengthen it to a genuine analytic pole.
The algebraic engine is the paper identity $\Xi(J)-1=-2/(2J+1)$, valid wherever $2J+1\neq 0$. Boundary hit means the Cayley field tends to the value $1$ in the complex topology on that punctured neighborhood.
proof idea
Write $\ell$ for the punctured neighborhood filter at $z_0$. From $|\mathcal{J}|\to+\infty$ on $\ell$, a reverse-triangle lower bound $|2\mathcal{J}+1|\ge 2|\mathcal{J}|-1$ yields $|2\mathcal{J}+1|\to+\infty$. Norm-at-top is equivalent to cobounded, so $(2\mathcal{J}+1)^{-1}\to 0$ on $\ell$.
Eventually $2\mathcal{J}+1\neq 0$ (norm eventually positive). On that set, expand $\theta$ via its quotient form and clear denominators to obtain the eventual equality $\theta(\mathcal{J})=1+(-2)(2\mathcal{J}+1)^{-1}$. The right-hand side tends to $1$ by constant multiplication and addition; transfer the limit along the eventual equality.
why it matters
This is the core front-end lemma of RSA: sensor blow-up implies Cayley boundary hit. Downstream, frontEnd_of_obstruction packages an obstruction $G$ together with candidate hypotheses ($G\to 0$ and $G\neq 0$ eventually on the punctured neighborhood) into a FrontEnd instance whose Cayley field $\Xi=\theta(1/G)$ hits the boundary state $1$. The RL layer also wires the sensor-of-obstruction definition through this step.
In the manuscript pipeline the lemma converts analytic vanishing of an obstruction into a topological boundary event without committing the interface to full meromorphic pole theory. It is the precise place where the Cayley transform turns an interior singularity of the sensor into a hit on the unit-circle boundary value $1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.