FrontEnd
plain-language theorem explainer
Front-end obligations for a Recognition Stability Audit problem: if the candidate holds at a point of the audited region, the Cayley field Ξ tends to the forbidden boundary value 1 along the punctured neighborhood. Anyone packaging an RSA instance cites this Prop structure as the checklist that compiles an existence claim into a boundary-hit statement. There is no proof body; instances are filled by supplying that single implication.
Claim. For an RSA problem $P$ with audited region $\Omega\subseteq\mathbb{C}$, candidate predicate $C:\mathbb{C}\to\mathrm{Prop}$, and Cayley field $\Xi:\mathbb{C}\to\mathbb{C}$, a front-end is the obligation that for every $z_0\in\Omega$, if $C(z_0)$ holds then $\Xi(z)\to 1$ as $z\to z_0$ in the punctured neighborhood of $z_0$.
background
Recognition Stability Audit (RSA), as set out in this module and in Recognition_Stability_Audit.tex, is a three-part compiler. The front-end turns a candidate existence claim into a boundary-hit condition on a bounded Cayley field $\Xi$; the back-end supplies a finite certificate that $\Xi$ stays Schur-bounded on the audited region (hence cannot hit the forbidden boundary); the correctness theorem combines both sides to rule the candidate out.
A problem instance packages the audited region $\Omega$, the candidate predicate $C$, and the field $\Xi$ (morally the Cayley transform $\Xi=(2\mathcal{J}-1)/(2\mathcal{J}+1)$ after pullback). The compiled forbidden event is a boundary hit at $z_0$: $\Xi$ tends to $1$ along the punctured neighborhood filter $\mathcal{N}{z_0}^c$. RSA references the canonical reciprocal cost $J(x)=\tfrac12(x+x^{-1})-1$ on $\mathbb{R}_{>0}$ but does not re-prove $J$-uniqueness here.
The module is deliberately RL-friendly: each RSA step is a small structure of proof obligations, so downstream goals only consume those checklists.
proof idea
No proof body: FrontEnd is a Prop-valued structure with a single field. An instance is exactly a proof of
$$\forall z_0\in\Omega,\quad C(z_0)\implies \mathrm{BoundaryHitAt}(\Xi,z_0).$$
Concrete instances are built elsewhere by obstruction compilers (candidate implies an analytic obstruction $G\to 0$ with $G$ eventually nonzero, then $\Xi=\theta(1/G)$ hits $1$). The structure itself only records the compiled implication.
why it matters
This is the front half of the RSA soundness interface. The parent correctness theorem states: given a front-end and a back-end for the same problem, the candidate cannot occur anywhere in $\Omega$. Downstream, frontEnd_of_obstruction manufactures front-ends from two filter obligations on an obstruction $G$, and the RL goals (goal_frontEnd_from_candidate_obligations, goal_correctness_usage, goal_obstruction_to_sensor_blowup) train exactly on filling this checklist.
In the paper pipeline the front-end encodes “candidate $\Rightarrow$ sensor pole $\Rightarrow\Xi\to 1$.” That is the analytic half of the audit; the Schur/Herglotz back-end then forbids $\Xi\to 1$. The structure sits in the verification layer rather than the T0–T8 forcing chain, but it inherits the RS cost primitive $J$ (T5) via the Cayley field built from it. Closing domain-specific front-ends is how concrete “monster” candidates get ruled out on chart domains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.