BoundaryHitAt
plain-language theorem explainer
A complex map Ξ has a boundary hit at z0 when it tends to the value 1 along every approach in a punctured neighborhood of z0. This is the compiled forbidden-event predicate of the Recognition Stability Audit: candidates are reduced to such hits (typically via a sensor pole forcing Ξ → 1). Front-end and back-end RSA structures, and the audit soundness theorem, all quote this predicate. The body is a one-line filter-limit definition.
Claim. For a map $\Xi:\mathbb{C}\to\mathbb{C}$ and a point $z_0\in\mathbb{C}$, a boundary hit at $z_0$ means $\Xi(z)\to 1$ as $z\to z_0$ with $z\neq z_0$ (equivalently: $\Xi$ tends to $1$ along the punctured-neighborhood filter at $z_0$).
background
Recognition Stability Audit (RSA) is the Lean interface for the audit pipeline in Recognition_Stability_Audit.tex. It is structured as a compiler: a front-end turns a candidate existence claim into a boundary-hit condition on a Cayley field $\Xi$; a back-end supplies a finite certificate that $\Xi$ stays Schur-bounded on an audited open region $\Omega$ and therefore cannot hit the forbidden boundary state; correctness says that if both sides succeed, the candidate is impossible in $\Omega$.
The foundational cost is the canonical reciprocal $J(x)=\frac12(x+x^{-1})-1$ on $\mathbb{R}_{>0}$ (already formalized as Jcost). RSA does not re-prove $J$-uniqueness; it only references that cost layer. The Cayley field $\Xi$ is the complex object the audit certifies as Schur-bounded. A boundary hit is the compiled event the front-end aims to force and the back-end aims to rule out.
Sibling interface pieces include SchurOn (Schur bound on a region), Problem (region, candidate predicate, and $\Xi$), FrontEnd, BackEnd, and the top-level correctness theorem.
proof idea
Pure definition: no proof obligations. The predicate is the Mathlib filter statement that $\Xi$ tends to the constant $1$ along the punctured neighborhood filter $\mathcal{N}{z_0}^c$. That is exactly the analytic meaning of “approaches the forbidden boundary value $1$ at an interior point without needing the value at $z_0$ itself.” Downstream lemmas compare this limit to continuity or holomorphy at $z_0$ when they need $\Xi(z_0)=1$.
why it matters
This predicate is the hinge of the RSA compiler. The front-end structure requires candidate_implies_boundaryHit: every candidate point in $\Omega$ produces a boundary hit for $\Xi$. The back-end structure requires no_boundary_hit: under a Schur certificate, no interior point admits a boundary hit. Audit soundness (correctness) is the one-line clash of those two obligations.
Concrete parents: boundaryHit_implies_value_eq_one (continuous at $z_0$ plus a hit forces $\Xi(z_0)=1$); eq_const_one_of_boundaryHit (holomorphic Schur on a preconnected open set plus any hit forces $\Xi\equiv 1$); no_boundaryHit_of_schur_holomorphic_nontrivial (same hypotheses plus nontriviality rule out hits entirely). Front-end encodings such as boundaryHit_theta_of_sensorBlowsUp discharge the candidate-to-hit arrow via sensor poles.
In framework terms, RSA sits in the verification layer that polices stability of recognition observables built on the $J$-cost (T5 uniqueness) without reopening the forcing chain. The definition itself is closed; open work is filling domain-specific FrontEnd/BackEnd instances.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.