sensorOfObstruction
plain-language theorem explainer
Defines the RSA sensor associated to a complex obstruction map G by pointwise inversion: J(z) = 1/G(z). Domain instantiations and the front-end compiler cite it to turn zeros of G into norm blow-ups of the sensor. The body is a one-line function definition.
Claim. Given a complex-valued map $G:\mathbb{C}\to\mathbb{C}$, the associated sensor is the pointwise reciprocal $J(z):=(G(z))^{-1}$.
background
The Recognition Stability Audit (RSA) front-end formalizes a manuscript pipeline: an obstruction $G$ (a holomorphic representative of a defect or claim), a sensor $J:=1/G$, a Cayley field $\Xi:=\theta(J)=(2J-1)/(2J+1)$, and the implication that a norm blow-up of $J$ at $z_0$ forces $\Xi\to 1$ along the punctured neighborhood of $z_0$.
Poles are phrased only as norm blow-up conditions at this interface layer, deliberately avoiding meromorphic machinery so that domain instantiations can later strengthen the analytic content. The sensor is the bridge from "$G$ tends to zero and stays nonzero" to "$|J|\to\infty$", which is the filter-level input needed by the Cayley boundary-hit step.
proof idea
Pure definition: the sensor of $G$ is the anonymous function $z\mapsto (G z)^{-1}$. No lemmas or tactics; noncomputable only because complex inversion is involved. Downstream theorems such as sensorBlowsUpAt_of_tendsto_zero immediately specialize filter lemmas to this reciprocal.
why it matters
This is the canonical naming of step 2 in the RSA front-end chain (obstruction $\to$ sensor $\to$ Cayley field $\to$ boundary hit). It is consumed by frontEnd_of_obstruction, which builds a full FrontEnd instance once a candidate forces $G\to 0$ and $G\neq 0$ eventually on the punctured neighborhood, yielding $\Xi\to 1$. It is also the target of the micro-goal goal_obstruction_to_sensor_blowup and the simp lemma sensorOfObstruction_def in the RL layer.
In the broader Recognition framework this packages the generic analytic move that domain proofs must discharge when they show "candidate implies the obstruction has a (simple) zero": invert to obtain the sensor blow-up that drives the Cayley map to the boundary state $1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.