goal_correctness_usage
plain-language theorem explainer
End-to-end RSA compiler correctness: if a FrontEnd maps candidates to boundary hits and a BackEnd certifies that boundary hits are impossible, then no candidate can sit in the audited region Ω. Cited as a gold training goal for the RSA reinforcement-learning pipeline. Proof is a one-line application of the underlying correctness lemma after introducing the point.
Claim. Let $P$ be a recognition-stability problem with audited region $\Omega_P$ and candidate predicate $\mathrm{Candidate}_P$. Given a front-end that compiles any candidate into a boundary hit and a back-end certificate that forbids boundary hits on $P$, every $z_0\in\Omega_P$ satisfies $\neg\mathrm{Candidate}_P(z_0)$.
background
The module packages the Recognition Stability Audit (RSA) as an RL-friendly Lean environment: whitelisted simp lemmas (rsa_simp), milestone lemmas (rsa_step), and a library of proved gold goals that an agent can close for reward.
A Problem carries an audited complex region $\Omega$ and a Candidate predicate. A FrontEnd is a compilation that turns any candidate into a boundary-hit witness; a BackEnd is a certificate that no boundary hit can occur. The composition is the standard RSA compiler-correctness pattern: front-end obstruction plus back-end exclusion implies the candidate is empty on $\Omega$.
Upstream scaffolding includes the RS tick $\tau_0=1$ (eight-tick octave period), bridge structures that equate native and display observables, and foundation forcing material; those appear as ambient dependencies rather than direct proof ingredients here.
proof idea
Term-mode one-liner. Introduce $z_0\in\Omega$ and discharge by exact correctness FE BE hz0, i.e. apply the already-proved end-to-end correctness lemma specialized to the given problem, front-end, and back-end. No additional rewriting or case analysis.
why it matters
This is a canonical gold theorem in the RSA RL goals namespace: it exercises the full FrontEnd/BackEnd compiler story in a form an agent can target with rsa_step/rsa_simp. The doc-comment frames it as end-to-end compiler correctness for the audit pipeline.
It sits downstream of the core correctness result and sibling goals (pole-implies-boundary-hit, obstruction-to-sensor-blowup, theta identities). In the broader Recognition framework it is verification scaffolding, not a forcing-chain step (T5–T8); it checks that candidate exclusion is mechanically usable once boundary-hit compilation and certificates are in hand. No further used-by edges are recorded; its role is training and audit closure rather than feeding a named parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.