BoundaryHitAt_def
plain-language theorem explainer
Unfolds the boundary-hit predicate to the filter statement that a complex field tends to 1 along the punctured neighborhood of a point. Audit and RL tactics cite it as a whitelisted rewrite so automated steps can expand the compiled forbidden-event form without leaving the RSA simp set. The proof is pure definitional reflexivity.
Claim. For a field $\Xi:\mathbb{C}\to\mathbb{C}$ and a point $z_0\in\mathbb{C}$, the assertion that a boundary hit occurs at $z_0$ is definitionally equal to $\Xi(z)\to 1$ as $z\to z_0$ through the punctured plane $\mathbb{C}\setminus\{z_0\}$.
background
Recognition Stability Audit (RSA) packages analytic obstruction checks as Lean predicates on complex fields. The core predicate "boundary hit at a point" means: along the punctured neighborhood filter of $z_0$, the field $\Xi$ tends to the value $1$. Upstream, that is exactly the definition of the compiled forbidden-event form used in candidate-implies-boundary-hit arguments (typically via a sensor pole forcing $\Xi\to 1$).
This module sits in the RSA reinforcement-learning layer. It tags selected equalities with @[rsa_simp] so the restricted tactic rsa_simp may unfold them, and it keeps high-level wrappers intact until a milestone apply is chosen. The local setting is therefore not new analysis: it is a controlled interface so an external agent can propose bounded audit steps and receive a deterministic Lean reward on goal progress.
proof idea
One-line definitional proof: rfl. The left-hand side is the named predicate; the right-hand side is its defining Tendsto statement on the punctured neighborhood filter, so the equality holds by construction and needs no lemmas beyond the definition.
why it matters
In the RSA pipeline the boundary-hit predicate is the compiled forbidden event: a candidate configuration is rejected when the field is forced to $1$ at a puncture. Registering the unfold as an @[rsa_simp] lemma lets automated and RL-driven audit steps expand that event inside the whitelist without ad-hoc simp sets or leaking non-audit rewrites.
No downstream theorems are recorded as direct users yet; the declaration exists so gold training goals and rsa_step/rsa_simp runs can normalize boundary-hit goals to filter language. It does not itself prove any physical stability claim; it only exposes the Core definition to the RL-friendly tactic surface of the Verification stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.