SensorBlowsUpAt
plain-language theorem explainer
Defines the RSA “sensor blow-up” predicate at a point z0: the complex sensor field has norm tending to infinity on the punctured neighborhood of z0. Domain authors and front-end compilers cite it as the interface notion of a pole without meromorphic machinery. It is a one-line filter definition (Tendsto of the norm to atTop).
Claim. A complex sensor field $\mathcal{J}$ blows up at $z_0\in\mathbb{C}$ when $\|\mathcal{J}(z)\|\to +\infty$ as $z\to z_0$ through the punctured neighborhood $\mathbb{C}\setminus\{z_0\}$.
background
The Recognition Stability Audit (RSA) front-end converts an obstruction into a boundary hit on the unit circle via a Cayley transform. An obstruction $G$ is a holomorphic representative of a defect or claim; the sensor is $\mathcal{J}:=1/G$; the Cayley field is $\Xi=\theta(\mathcal{J})=(2\mathcal{J}-1)/(2\mathcal{J}+1)$. The manuscript step is: if the sensor blows up at $z_0$, then $\Xi\to 1$ along the punctured neighborhood.
This definition deliberately phrases “pole” as a pure norm blow-up on the punctured filter $\mathcal{N}{z_0}^c$. That is strong enough for RSA and keeps meromorphic language out of the interface layer; domain instantiations may later strengthen it to an analytic pole.
Downstream, blow-up is obtained from $G\to 0$ with $G$ eventually nonzero (via the sensor-of-obstruction map), and is fed into the core identity $\Xi(J)-1=-2/(2J+1)$ together with $|2J+1|\to\infty$ when $|J|\to\infty$.
proof idea
Pure definitional abbreviation: the proposition is exactly the Mathlib filter statement that the real-valued map $z\mapsto|\mathcal{J}(z)|$ tends to $+\infty$ along the punctured neighborhood filter of $z_0$. No lemmas are applied; the body is the Tendsto ... atTop term itself. A companion simp lemma in the RL layer unfolds it by rfl.
why it matters
This is the interface atom of the RSA front-end chain in the manuscript: obstruction $\to$ sensor $\to$ Cayley field $\to$ boundary hit at $1$. It is the hypothesis of the core lemma that sensor blow-up implies the Cayley field hits the boundary state $1$, and of the RL micro-goal that packages the same implication for tactic automation.
It is also the conclusion of the generic filter lemma that turns “candidate $\Rightarrow$ obstruction tends to zero and stays nonzero” into sensor blow-up, and of the front-end compiler that builds a full FrontEnd instance from an obstruction $G$. The RL layer re-exports the definitional equality so rsa_step can discharge micro-goals without reopening filters.
Within Recognition Science verification, this keeps the stability audit at the level of norms and filters rather than full meromorphic calculus, matching the module’s design choice for the interface layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.