goal_boundaryHit_value
plain-language theorem explainer
Continuity at a point plus a boundary hit (limit value 1 on the punctured neighborhood) forces the complex field to equal 1 at that point. RSA pipeline authors and RL trainers cite it as a gold micro-goal linking the compiled forbidden-event predicate to a concrete value. The proof is one rsa_step against the milestone whitelist.
Claim. Let $\Xi:\mathbb{C}\to\mathbb{C}$ and $z_0\in\mathbb{C}$. If $\Xi$ is continuous at $z_0$ and $\Xi(z)\to 1$ as $z\to z_0$ through $z\neq z_0$, then $\Xi(z_0)=1$.
background
In the Recognition Stability Audit (RSA), a boundary hit is the compiled forbidden-event predicate: along the punctured neighborhood of a point $z_0$, the complex field $\Xi$ tends to $1$. Formally, BoundaryHitAt is the filter statement $\mathrm{Tendsto},\Xi,(\mathcal{N}[{z_0}^c],z_0),(\mathcal{N},1)$. Upstream, candidate events (sensor poles, obstruction blow-ups) are reduced to this predicate.
Continuity at $z_0$ is the missing glue: a limit on the punctured neighborhood does not by itself fix the value at the point. Once continuity is assumed, the limit and the point value must agree, so $\Xi(z_0)=1$.
This file is the RSA reinforcement-learning layer. It exposes gold theorems (no sorry) that exercise the whitelisted tactics rsa_step and rsa_simp, so an external agent can propose steps and receive Lean reward on goal closure.
proof idea
One-line wrapper: rsa_step. That tactic tries assumption, then applies a lemma tagged @[rsa_milestone], discharges trivial subgoals, and falls back to the @[rsa_simp] whitelist. Here the milestone is the standard filter fact that continuous-at plus tendsto on the punctured neighborhood forces the point value to equal the limit (namely 1). No manual case split or complex analysis beyond that continuity/limit agreement is required.
why it matters
This is a back-end micro-goal in the RSA gold library: boundary hit plus continuity yields the concrete value $\Xi(z_0)=1$. Downstream RSA reasoning chains sensor poles and obstruction blow-ups into boundary hits; this lemma closes the last arithmetic step from the hit predicate to a fixed complex value.
In the broader Recognition Stability Audit, forbidden events are compiled to $\Xi\to 1$ on punctured neighborhoods. Pinning the continuous value at the puncture is what turns that asymptotic statement into an equality usable by later constancy or Schur-class arguments (siblings such as pole-implies-boundary-hit and obstruction-to-sensor-blowup sit in the same training set).
No parent theorem currently lists this declaration as a dependency (used_by is empty); its role is training and checklist completion inside the RL-friendly RSA pipeline rather than a named paper proposition in the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.