goal_frontEnd_from_candidate_obligations
plain-language theorem explainer
Canonical FrontEnd gold goal for the RSA RL pipeline: if the candidate set is defined exactly by the two analytic obligations (G tends to 0 on the punctured neighborhood, and G is eventually nonzero there), then FrontEnd holds for Ξ = θ ∘ (1/G). Anyone wiring RSA micro-goals into an RL reward loop would cite it. Proof is a short refine through frontEnd_of_obstruction, projecting the candidate conjunction.
Claim. For any $\Omega \subseteq \mathbb{C}$ and $G:\mathbb{C}\to\mathbb{C}$, let the candidate predicate at $z_0$ be "$G\to 0$ along the punctured neighborhood of $z_0$, and $G$ is eventually nonzero there". Then the FrontEnd package with domain $\Omega$, that candidate, and sensor $\Xi(z)=\theta((G z)^{-1})$ holds.
background
The enclosing module turns the Recognition Stability Audit (RSA) into an RL-friendly Lean environment: @[rsa_simp] / @[rsa_milestone] tags, bounded tactics rsa_simp and rsa_step, and a library of proved gold goals that supply reward signal when an agent closes them.
FrontEnd is the audit's front-end package: a domain $\Omega$, a candidate predicate on points, and a complex sensor $\Xi$. The intended reading is that candidates are obstruction loci for an analytic map $G$, and $\Xi$ is built from $G$ so that a boundary hit of $\Xi$ records the obstruction. Here $\Xi(z)=\theta((G z)^{-1})$, with $\theta$ the sensor transform used throughout the sibling micro-goals (goal_theta_eq_div, goal_pole_implies_boundaryHit, etc.).
The two analytic obligations baked into the candidate are: (i) $G$ tends to $0$ in the punctured filter at $z_0$, and (ii) $G$ is eventually nonzero on that punctured neighborhood (so the reciprocal is eventually defined). Upstream constructor frontEnd_of_obstruction turns exactly those two facts into a FrontEnd witness.
proof idea
One short tactic proof. After introducing the local Candidate binder, refine frontEnd_of_obstruction builds the FrontEnd structure from the obstruction constructor, leaving two subgoals: the limit obligation and the eventual-nonzero obligation. Each is discharged by projecting the corresponding conjunct out of the candidate hypothesis (hC.1 and hC.2). No analytic work is redone; the candidate definition is definitionally the pair of obligations the constructor demands.
why it matters
This is a canonical training goal in the RSA RL suite, not a physics derivation step. It locks the FrontEnd API shape: candidates that already carry the two punctured-neighborhood obligations compile, via frontEnd_of_obstruction, into a boundary-hit-ready FrontEnd with sensor $\Xi=\theta\circ(1/G)$. Downstream sibling goals (pole implies boundary hit; obstruction to sensor blow-up; back-end forcing $\Xi z_0=1$ from boundary hit plus continuity) sit on the same checklist and assume this packaging is available.
In the broader Recognition Stability Audit, FrontEnd is the entry point that turns analytic obstruction data into the sensor language used by Schur-type and boundary-hit milestones. The declaration has no further used_by edges yet; its role is to be a closed, sorry-free gold theorem the RL loop can target. It does not itself invoke the forcing chain (T5–T8), RCL, or the mass ladder; it only stabilizes the verification front-end those later audits consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.