boundaryHit_implies_value_eq_one
plain-language theorem explainer
If a complex map Ξ is continuous at z0 and hits the unit-circle boundary value 1 in the punctured-neighborhood sense, then Ξ(z0) equals 1. Recognition Stability Audit cites this as the first link in the Schur/Herglotz pinch chain. The proof equates the continuity limit with the boundary-hit limit along the same punctured filter via uniqueness of limits in ℂ.
Claim. Let $\Xi:\mathbb{C}\to\mathbb{C}$ and $z_0\in\mathbb{C}$. If $\Xi$ is continuous at $z_0$ and $\Xi$ tends to $1$ along the punctured neighborhood filter at $z_0$ (a boundary hit at $z_0$), then $\Xi(z_0)=1$.
background
The Recognition Stability Audit (RSA) back-end abstracts a manuscript argument: on an audited open region Ω one assumes a Schur bound ‖Ξ z‖ ≤ 1, holomorphy of Ξ on Ω, and nontriviality (Ξ not identically constant), and concludes there are no boundary hits inside Ω.
A boundary hit at z0 means Ξ tends to the complex value 1 along the punctured neighborhood filter 𝓝[{z0}ᶜ] z0. Continuity at z0 means Ξ tends to Ξ(z0) in the ordinary neighborhood filter. The module builds the pinch from four reusable steps; this declaration is step 1: continuity plus a boundary hit forces the point value Ξ(z0) = 1.
Later steps feed maximum modulus: once the value is 1 under a Schur bound, ‖Ξ‖ attains its maximum, holomorphy on a preconnected open set forces constancy, and nontriviality yields the contradiction.
proof idea
Work on the shared punctured filter l := 𝓝[{z0}ᶜ] z0. Continuity at z0 upgrades (via tendsto_nhdsWithin_of_tendsto_nhds) to Tendsto Ξ l (𝓝(Ξ z0)). The boundary-hit hypothesis is already Tendsto Ξ l (𝓝 1). The punctured neighborhood filter on ℂ is nontrivial (no isolated points), so NeBot l holds by instance. Uniqueness of limits (tendsto_nhds_unique) therefore identifies Ξ(z0) with 1. Pure filter comparison; no complex analysis beyond continuity.
why it matters
This is the first reusable lemma in the RSA back-end pinch chain documented in the module: boundary hit + continuity ⇒ value 1; Schur + value 1 ⇒ maximum of ‖Ξ‖; maximum modulus ⇒ constant; nontriviality contradicts constancy.
It is consumed directly by eq_const_one_of_boundaryHit, the full pinch lemma: if Ξ is holomorphic and Schur-bounded on a preconnected open Ω and hits the boundary at any z0 ∈ Ω, then Ξ ≡ 1 on Ω. That lemma in turn supports no_boundaryHit_of_schur_holomorphic_nontrivial and backEnd_of_schur_holomorphic_nontrivial, closing the audited “no boundary hits” claim under Schur + holomorphy + nontriviality.
In the broader Recognition framework this is verification infrastructure rather than a forcing-chain (T0–T8) step: it certifies stability of recognition observables under Schur-class analytic constraints, and is also referenced from the RL sensor-of-obstruction plumbing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.