sensorBlowsUpAt_of_tendsto_zero
plain-language theorem explainer
If a complex obstruction G tends to 0 on a punctured neighborhood of z0 and is eventually nonzero there, then the sensor 1/G has norm tending to +∞ at z0. Domain RSA instantiations cite this when they reduce “candidate implies simple zero of G” to the sensor blow-up interface. The proof upgrades the limit into the punctured codomain and composes with Mathlib’s norm-of-inverse-at-top lemma.
Claim. Let $G:\mathbb{C}\to\mathbb{C}$ and $z_0\in\mathbb{C}$. If $G(z)\to 0$ as $z\to z_0$ in the punctured neighborhood of $z_0$, and $G(z)\neq 0$ eventually on that punctured neighborhood, then the sensor $\mathcal{J}:=1/G$ blows up at $z_0$: $\|\mathcal{J}(z)\|\to +\infty$ along the same punctured filter.
background
Recognition Stability Audit (RSA) front-end formalizes the manuscript chain obstruction → sensor → Cayley field → boundary hit. An obstruction $G$ is a holomorphic (or at least continuous) 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)$. RSA phrases “pole” as a pure norm blow-up so the interface stays free of meromorphic machinery.
SensorBlowsUpAt is exactly that interface predicate: $|\mathcal{J}(z)|\to+\infty$ on the punctured neighborhood filter $\mathcal{N}{z_0}^c$. The companion constructor packages candidate hypotheses that force $G\to 0$ and $G\neq 0$ eventually, then concludes the Cayley field hits the boundary state $1$.
This lemma is the generic filter bridge those domain proofs need: zero of $G$ (with nonvanishing) becomes sensor blow-up.
proof idea
Term-mode composition of two filter facts. First, upgrade $G\to 0$ in the ordinary neighborhood of $0$ to a limit into the punctured codomain $\mathcal{N}{0}^c$, using eventual nonvanishing via tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within.
Second, invoke Mathlib’s tendsto_norm_inv_nhdsNE_zero_atTop: $|w^{-1}|\to+\infty$ as $w\to 0$ off ${0}$. Compose that map with the upgraded limit of $G$, then simpa unfolds SensorBlowsUpAt, sensorOfObstruction ($\mathcal{J}=1/G$), and function composition.
why it matters
This is the reusable analytic step that turns “candidate forces a (simple) zero of the obstruction” into the RSA sensor blow-up predicate. Downstream, frontEnd_of_obstruction builds a full FrontEnd instance from exactly the two obligations this theorem consumes ($G\to 0$ and eventual $G\neq 0$), concluding that the Cayley field $\Xi=\theta(1/G)$ hits boundary state $1$. The RL simp lemma sensorOfObstruction_def keeps the sensor definition aligned for rewriting.
In the manuscript front-end, pole ⇒ boundary hit is the gate before stability/audit conclusions. By staying at the norm-blow-up level, the lemma lets domain instantiations later strengthen to genuine poles without changing the interface. It does not itself touch T5–T8 forcing, RCL, or the mass ladder; it is verification plumbing that makes obstruction zeros speak the RSA boundary language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.