correctness
plain-language theorem explainer
RSA audit soundness: for any problem instance (audited region, candidate predicate, Cayley field), a front-end that compiles candidates into boundary hits plus a back-end certificate that forbids boundary hits jointly imply the candidate never occurs in the region. Cited by anyone using the Recognition Stability Audit pipeline or its RL training goals. Proof is a two-line contradiction: front-end produces a hit; back-end rules it out.
Claim. Let $P$ be an RSA problem with audited region $\Omega \subseteq \mathbb{C}$, candidate predicate $C$, and Cayley field $\Xi$. Suppose a front-end shows that $C(z_0)$ implies a boundary hit of $\Xi$ at every $z_0 \in \Omega$, and a back-end certificate shows $\Xi$ has no boundary hits on $\Omega$. Then $\neg C(z_0)$ for all $z_0 \in \Omega$.
background
Recognition Stability Audit (RSA) is the Lean interface for the audit pipeline in Recognition_Stability_Audit.tex. It is structured as a compiler: a front-end turns a candidate existence claim into a boundary-hit condition on a bounded Cayley field $\Xi$; a back-end supplies a finite certificate that $\Xi$ stays Schur-bounded on the audited region and therefore cannot hit the forbidden boundary; correctness then concludes the candidate is impossible there.
A problem instance packages the audited region $\Omega$ (typically a chart domain normalized to the disk), the candidate predicate $C$ ("the monster"), and the Cayley field $\Xi$ (in the paper, $\Xi = (2\mathcal{J}-1)/(2\mathcal{J}+1)$ after pullback). A boundary hit at $z_0$ means $\Xi$ tends to $1$ along the punctured neighborhood of $z_0$. The front-end obligation is exactly candidate $\Rightarrow$ boundary hit; the back-end supplies a global Schur bound plus the derived pinch conclusion that no interior point of $\Omega$ is a boundary hit.
RSA references the canonical reciprocal cost $J(x) = \tfrac12(x+x^{-1})-1$ on $\mathbb{R}_{>0}$ (formalized as Jcost) but does not re-prove cost uniqueness; the focus is the audit interface.
proof idea
Term-mode contradiction in three steps. Fix $z_0 \in \Omega$ and assume the candidate holds at $z_0$. Apply the front-end field candidate_implies_boundaryHit to obtain a boundary hit of $\Xi$ at $z_0$. Apply the back-end field no_boundary_hit at the same point to obtain the negation of that hit. Discharge. No analytic estimates or Schur theory are invoked here; those live inside concrete back-end instances. The theorem only composes the two structure obligations.
why it matters
This is the top-level soundness theorem of the RSA compiler and the explicit training target for the RL-friendly checklist design: fill front-end encodings and back-end certificates, then invoke correctness. Downstream, goal_correctness_usage is a one-line wrapper that applies it end-to-end, and goal_correctness_trivial_univ is the trivial micro-goal with $\Omega = \mathrm{univ}$ and candidate False. The same interface is referenced from foundation material on biconditional self-negation (GeneralSelfNegatingPredicate, no_general_self_negating_predicate), where audit-style correctness fields encode stabilization status.
In the broader Recognition framework the Cayley field is built from the canonical $J$-cost (T5 uniqueness: $J(x)=\cosh(\log x)-1$), so a successful audit rules out candidate pathologies on regions where the Schur/Herglotz certificate holds. The theorem itself is pure interface glue; domain instantiations still must discharge Schur bounds and the pinch argument from analyticity and nontriviality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.