backEnd_of_schur_holomorphic_nontrivial
plain-language theorem explainer
Packages a Schur disk bound, holomorphy, openness/preconnectedness of the audit region, and nontriviality into a full RSA back-end certificate: the field never boundary-hits at any interior point. Analysts certifying Recognition Stability Audit instances cite this constructor. The body is a one-line refine that reuses the main pinch lemma.
Claim. Given an RSA problem $P$ with audit region $\Omega$ open and preconnected, Cayley field $\Xi$ holomorphic on $\Omega$, Schur-bounded ($\|\Xi z\|\le 1$ on $\Omega$), and nontrivial ($\exists z\in\Omega$ with $\Xi z\ne 1$), there is a back-end certificate for $P$: the Schur bound holds and $\Xi$ has no boundary hit at any $z_0\in\Omega$.
background
Recognition Stability Audit (RSA) certifies that a candidate obstruction cannot occur on an audited complex region $\Omega$. A problem instance supplies $\Omega$, a candidate predicate, and a Cayley field $\Xi$ (in the paper, typically $\Xi=(2\mathcal{J}-1)/(2\mathcal{J}+1)$ after pullback). The Schur bound on $\Omega$ means $|\Xi z|\le 1$ for all $z\in\Omega$.
A boundary hit at $z_0$ is the compiled forbidden event: along the punctured neighborhood of $z_0$, the field tends to $1$. The back-end structure is the finite certificate demanded by the manuscript: it must supply both the global Schur bound and the derived conclusion that no interior point is a boundary hit.
The module implements the Schur/Herglotz pinch route: Schur bound plus analyticity plus nontriviality force the no-hit conclusion via maximum modulus. The upstream lemma already states that under those hypotheses, $\mathrm{BoundaryHitAt},\Xi,z_0$ is impossible for every $z_0\in\Omega$.
proof idea
One-line constructor. Refine the back-end structure with the given Schur hypothesis as the first field. For the second field (no boundary hit at arbitrary $z_0\in\Omega$), apply the main back-end lemma no_boundaryHit_of_schur_holomorphic_nontrivial with the openness, preconnectedness, holomorphy, Schur, and nontriviality hypotheses. No further case analysis.
why it matters
This is the reusable RSA back-end builder from the manuscript's Schur/Herglotz pinch argument: Schur bound + holomorphy + nontriviality yield the certificate that interior boundary hits are impossible. Downstream, the RL layer uses it for the canonical goal that constant $\Xi\equiv 0$ on $\Omega=\mathrm{univ}$ admits a back-end (holomorphic, Schur-bounded, and $\ne 1$), and it appears in the sensor-of-obstruction plumbing. It closes the interface between Core's BackEnd obligations and the analytic lemmas, so domain instantiations need only discharge openness, connectedness, holomorphy, Schur, and a single nontrivial point rather than replaying maximum modulus each time.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.