SensorBlowsUpAt_def
plain-language theorem explainer
Definitional unfold of the sensor blow-up predicate: for a complex sensor map J and point z0, blow-up at z0 means the norm of J tends to +infinity in every punctured neighborhood of z0. Audit and RL pipeline authors cite it so rsa_simp can expand the named predicate. The proof is pure rfl against the FrontEnd definition.
Claim. For $\mathcal{J}:\mathbb{C}\to\mathbb{C}$ and $z_0\in\mathbb{C}$, the statement that the sensor blows up at $z_0$ is definitionally equal to $\lVert\mathcal{J}(z)\rVert\to+\infty$ as $z\to z_0$ along the punctured neighborhood $\mathbb{C}\setminus\{z_0\}$.
background
The Recognition Stability Audit (RSA) FrontEnd defines a sensor blow-up predicate: a complex-valued sensor $\mathcal{J}$ "blows up" at $z_0$ when its norm tends to $+\infty$ on the punctured filter $\mathcal{N}{z_0}^c$. Upstream doc: "Pole/blow-up condition for a sensor $\mathcal{J}$ at $z_0$: the norm tends to $+\infty$ on a punctured neighborhood."
This module is the RL-facing layer of RSA. It whitelists rewrite lemmas under @[rsa_simp] so the custom tactic rsa_simp may unfold only approved equalities, and marks milestone lemmas for the bounded step tactic rsa_step. Canonical gold goals exercise the pipeline without sorry.
The named predicate is the left-hand side of the core paper identity linking sensor poles to the Cayley field hitting 1 ($\Xi(J)-1=-2/(2J+1)$ when $\lVert 2J+1\rVert\to\infty$).
proof idea
One-line definitional proof: rfl. The theorem states equality of the FrontEnd def with its body (Tendsto of the norm to atTop on the punctured neighborhood filter), so no lemmas or tactics beyond reflexivity are required. The @[rsa_simp] attribute registers it for the restricted simp set.
why it matters
Gives the RL and audit tactics a safe unfold for the sensor pole predicate without opening the whole simp set. Downstream gold goals in this module (e.g. obstruction-to-sensor-blowup and pole-implies-boundary-hit style milestones) need this expansion when the goal still mentions the named predicate rather than the raw Tendsto statement. It sits in the verification layer that checks Recognition Stability Audit claims about sensors, Cayley transforms, and boundary hits; it does not itself advance the T0–T8 forcing chain, but keeps the audit pipeline machine-checkable and RL-trainable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.