BackEnd
plain-language theorem explainer
Back-end certificate for a Recognition Stability Audit problem: the Cayley field Ξ is Schur-bounded on the audited region Ω, and therefore never hits the forbidden boundary value 1 at any interior point. Auditors and the RSA correctness theorem cite it as the finite certificate half of the front-end/back-end compiler. It is a Prop-valued structure bundling those two obligations; domain work discharges the pinch clause from Schur plus holomorphy and nontriviality.
Claim. For an RSA problem $P$ (audited region $\Omega$, candidate predicate, Cayley field $\Xi$), a back-end certificate is the pair of propositions: (i) $\Xi$ is Schur-bounded on $\Omega$, i.e. $\|\Xi(z)\| \le 1$ for all $z \in \Omega$; (ii) $\Xi$ has no boundary hit at any $z_0 \in \Omega$, meaning $\Xi$ does not tend to $1$ along the punctured neighborhood of $z_0$.
background
Recognition Stability Audit (RSA) is the Lean interface for the paper pipeline that treats existence claims as a compiler. The front-end turns a candidate into a boundary-hit condition for a bounded Cayley field $\Xi$; the back-end supplies a finite certificate that $\Xi$ stays in the Schur class on the audited chart domain, so the forbidden boundary state is unreachable; correctness then rules the candidate out on that region.
A problem instance packages $\Omega \subseteq \mathbb{C}$, a candidate predicate, and the field $\Xi$ (morally the Cayley transform of the pulled-back cost). Schur-on-$\Omega$ means $|f(z)| \le 1$ everywhere on $\Omega$. A boundary hit at $z_0$ is the filter statement that $\Xi$ tends to $1$ along the punctured neighborhood of $z_0$—the compiled forbidden event (sensor pole $\Rightarrow \Xi \to 1$).
The module sits on the canonical reciprocal cost $J(x)=\frac12(x+x^{-1})-1$ already formalized as Jcost; it does not re-prove $J$-uniqueness, only the audit checklist.
proof idea
No proof body: BackEnd is a Prop-valued structure, i.e. an explicit checklist of two fields. The first field is the global disk bound SchurOn P.Ω P.Xi. The second is the universal pinch conclusion: every interior point of $\Omega$ fails BoundaryHitAt for $P.Xi$.
Concrete certificates are built downstream. The main constructor applies the lemma that Schur bound plus holomorphy on an open preconnected $\Omega$ plus nontriviality ($\exists z\in\Omega$, $\Xi(z)\ne 1$) implies no boundary hits, then packages both obligations into a BackEnd value. RL micro-goals exercise the constant-$\Xi\equiv 0$ case and related pinch facts.
why it matters
This structure is the back half of the RSA compiler. The soundness theorem correctness consumes a FrontEnd and a BackEnd and concludes that the candidate cannot hold anywhere in $\Omega$: front-end yields a boundary hit from the candidate; back-end forbids every such hit.
Downstream, backEnd_of_schur_holomorphic_nontrivial and no_boundaryHit_of_schur_holomorphic_nontrivial realize the paper’s Schur/Herglotz-plus-pinch route inside Lean, while the RL goals (goal_backEnd_const_zero, boundary-hit forces constancy, end-to-end trivial correctness) train agents to fill the checklist. In framework terms the audit rides on the canonical $J$-cost (T5 uniqueness) after Cayley normalization; the structure itself is domain-agnostic scaffolding for those certificates, not a new forcing step (T6–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.