eq_const_one_of_boundaryHit
plain-language theorem explainer
If a holomorphic map Ξ on a preconnected open set Ω is Schur-bounded (‖Ξ‖ ≤ 1) and hits the unit-circle boundary at an interior point, then Ξ is identically 1 on Ω. RSA back-end and stability-audit arguments cite this pinch. The proof evaluates Ξ at the hit via continuity, obtains an interior maximum of ‖Ξ‖, and applies the maximum-modulus principle.
Claim. Let $\Omega \subset \mathbb{C}$ be open and preconnected, and let $\Xi : \mathbb{C} \to \mathbb{C}$ be holomorphic on $\Omega$ with $\|\Xi(z)\| \le 1$ for all $z \in \Omega$. If there exists $z_0 \in \Omega$ at which $\Xi$ has a boundary hit (in the RSA sense), then $\Xi(z) = 1$ for every $z \in \Omega$.
background
The Recognition Stability Audit (RSA) back-end abstracts a manuscript argument: on an audited region Ω one assumes a Schur bound ‖Ξ z‖ ≤ 1, complex differentiability on Ω, and (in the main lemma) nontriviality, then concludes that BoundaryHitAt Ξ z0 is impossible for every interior point z0.
A boundary hit is an RSA obstruction sensor event at an interior point; the sibling lemma records that continuity at that point forces the value Ξ z0 = 1. SchurOn Ω Ξ is the pointwise disk bound ‖Ξ z‖ ≤ 1 on Ω. The module builds the pinch from four reusable steps: value-one at a hit, interior maximum of the modulus, maximum-modulus constancy, and (downstream) contradiction with nontriviality.
The local analytic engine is the standard maximum-modulus principle on a preconnected open set in ℂ: if a holomorphic map attains a maximum of its modulus at an interior point, it is constant on the component.
proof idea
Four short tactic steps.
-
Holomorphy on an open set gives continuity at z0; the sibling lemma
boundaryHit_implies_value_eq_onethen yields Ξ z0 = 1. -
SchurOn supplies ‖Ξ z‖ ≤ 1 everywhere on Ω. Rewriting the right-hand side via Ξ z0 = 1 shows that norm ∘ Ξ attains a maximum at z0 on Ω.
-
Apply Mathlib's
Complex.eqOn_of_isPreconnected_of_isMaxOn_normwith openness, preconnectedness, holomorphy, and the maximum just obtained: Ξ equals the constant function with value Ξ z0 on Ω. -
Transitivity of Set.EqOn plus substitution of Ξ z0 = 1 finishes: Ξ is identically 1 on Ω.
why it matters
This is the RSA back-end “pinch” lemma named in the module doc: boundary hit plus Schur holomorphy forces the constant-1 map. Its immediate parent is no_boundaryHit_of_schur_holomorphic_nontrivial, which adds a nontriviality hypothesis (some point of Ω where Ξ ≠ 1) and concludes that BoundaryHitAt is impossible anywhere in Ω. That is the manuscript pinch: Schur bound + analyticity + nontriviality ⇒ no interior boundary hits.
A second use site is in the RL layer (sensorOfObstruction_def), where obstruction sensors are wired to the same boundary-hit language. Within Recognition Science verification, the lemma is pure complex analysis scaffolding for stability audits of recognition maps; it does not itself invoke the forcing chain (T5–T8), RCL, or the φ-ladder, but it underwrites the analytic half of those audits whenever a Schur-class transfer function is checked for interior boundary contact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.