sensorOfObstruction_def
plain-language theorem explainer
Unfolds the obstruction sensor: for a complex map G, the sensor is the pointwise reciprocal z ↦ (G z)⁻¹. RSA pipeline authors and RL agents cite it as a whitelisted simp fact when reducing sensor-blowup goals to reciprocal poles. The proof is pure definitional equality (rfl).
Claim. For any map $G:\mathbb{C}\to\mathbb{C}$, the obstruction sensor of $G$ equals the pointwise reciprocal: $\mathrm{sensor}(G)(z)=(G(z))^{-1}$ for all $z$.
background
This lives in the Recognition Stability Audit (RSA) reinforcement-learning module. That module tags rewrite lemmas with @[rsa_simp] and milestone lemmas with @[rsa_milestone], then exposes bounded tactics (rsa_simp, rsa_step) so an external agent can propose steps while Lean scores goal closure.
The obstruction sensor is the audit's probe for zeros of a complex map $G$: where $G$ vanishes, the reciprocal develops a pole. Sibling definitions in the same file package related audit atoms (boundary-hit predicates, Schur-class hypotheses, sensor-blowup statements). Downstream training goals connect poles of the sensor to boundary hits and to constancy conclusions for Schur maps.
Upstream name collisions on G (Newton constant, log-reparametrized cost, etc.) are unrelated; here $G$ is simply an arbitrary complex function serving as the obstruction map under audit.
proof idea
One-line definitional proof: rfl. The theorem exists only to expose the equation sensorOfObstruction G = fun z => (G z)⁻¹ to the @[rsa_simp] whitelist, so rsa_simp can unfold the sensor without opening arbitrary definitions.
why it matters
Inside RSA, sensor blow-up is the bridge from analytic obstruction (a zero of $G$) to geometric boundary contact on the disk. This unfold lemma is the first rewrite in that chain: once the sensor is the reciprocal, tendsto-zero lemmas on $G$ become pole lemmas on the sensor, which feed boundary-hit milestones (boundaryHit_theta_of_sensorBlowsUp, sensorBlowsUpAt_of_tendsto_zero) and the gold training goals under RLGoals.
It does not itself touch the forcing chain (T5–T8), RCL, or the mass ladder; it is verification scaffolding for the stability audit. used_by is currently empty, so its place is as a tagged primitive for the RL tactic loop rather than as a cited lemma in finished physics theorems. Closing the surrounding scaffold means discharging the canonical goals (goal_obstruction_to_sensor_blowup, pole-implies-boundaryHit, etc.) entirely by rsa_step/rsa_simp without free-form simp.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.