goal_backEnd_const_zero
plain-language theorem explainer
Constant zero as the complex sensor on the whole plane yields a back-end certificate for the Recognition Stability Audit problem. RSA training and verification cite this as a gold micro-goal with empty candidate set. The proof feeds the generic Schur-holomorphic-nontrivial constructor and closes openness, connectedness, holomorphy, the Schur bound, and nontriviality by elementary simp and norm_num.
Claim. Let $P$ be the RSA problem with domain $\Omega=\mathbb{C}$, candidate predicate identically false, and sensor $\Xi\equiv 0$. Then $P$ admits a back-end certificate: a global Schur bound for $\Xi$ on $\Omega$ together with the pinch conclusion that $\Xi$ never hits a forbidden boundary value at any interior point.
background
The Recognition Stability Audit (RSA) packages analytic control of a complex sensor $\Xi$ on a domain $\Omega\subseteq\mathbb{C}$. A Problem records $\Omega$, a candidate predicate, and $\Xi$. The back-end structure is the finite certificate that prevents boundary hits: it demands a global Schur bound on $\Xi$ and the derived statement that no interior point is a boundary hit.
Upstream, the constructor builds that certificate from three analytic inputs once $\Omega$ is open and preconnected: holomorphy of $\Xi$ on $\Omega$, the Schur bound, and nontriviality ($\Xi(z)\neq 1$ somewhere in $\Omega$). In the paper language this is Schur/Herglotz control plus the pinch argument; the Lean interface keeps those obligations explicit.
This file is the RL-facing layer of RSA: whitelisted simp and milestone lemmas, plus a library of proved gold goals that train or audit step tactics. The present goal is the simplest constant case on the full plane.
proof idea
One refine of the generic constructor backEnd_of_schur_holomorphic_nontrivial on the constant-zero problem. Openness and preconnectedness of $\mathbb{C}$ are isOpen_univ and isPreconnected_univ. Holomorphy of the constant map and the Schur bound on the universe are discharged by simp. Nontriviality is the witness $z=0$ with $0\neq 1$, closed by norm_num.
why it matters
Among the canonical RSA training goals, this is the end-to-end micro-goal that rules out the empty candidate immediately when $\Omega$ is the whole plane and $\Xi\equiv 0$. It exercises the back-end constructor path (Schur bound, holomorphy, nontriviality) without any sensor blow-up or pole analysis, so an RL agent or auditor can score a clean certificate closure.
No downstream theorem currently depends on it; its role is pedagogical and pipeline-facing inside the verification domain. It sits beside sibling gold goals (theta identities, pole-implies-boundary-hit, obstruction-to-sensor-blowup) that stress harder RSA milestones. Framework-wise it does not touch the forcing chain T0–T8 or the mass ladder; it only certifies the analytic back-end interface used when RSA is applied to recognition-stable sensors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.