frontEnd_of_obstruction
plain-language theorem explainer
Builds an RSA front-end from an obstruction map G on a complex domain. Whenever a candidate forces G→0 on the punctured neighborhood and G stays eventually nonzero, the Cayley field Ξ=θ(1/G) hits the boundary value 1. Verification authors cite it to compile analytic candidate obligations into a boundary-hit witness. Proof: lift the two tendsto hypotheses to sensor blow-up, then apply the pole⇒boundary-hit lemma.
Claim. Let $\Omega\subseteq\mathbb{C}$, let $\mathrm{Candidate}$ be a predicate on $\mathbb{C}$, and let $G:\mathbb{C}\to\mathbb{C}$. Suppose that for every $z_0\in\Omega$ with $\mathrm{Candidate}(z_0)$, one has $G\to 0$ along the punctured neighborhood of $z_0$ and $G\neq 0$ eventually there. Then $(\Omega,\mathrm{Candidate},\Xi)$ with $\Xi(z)=\theta((G(z))^{-1})$ is a front-end: every such candidate forces $\Xi$ to hit the boundary state $1$.
background
Recognition Stability Audit (RSA) front-end is the manuscript step that turns an analytic obstruction into a boundary hit. An obstruction $G$ is a holomorphic representative of a defect or claim. The sensor is $\mathcal{J}:=1/G$, and the Cayley field is $\Xi:=\theta\circ\mathcal{J}$, where RSA's paper-facing Cayley map is $\theta(J)=\mathrm{cayley}(2J)$, equivalently $\Xi=(2\mathcal{J}-1)/(2\mathcal{J}+1)$.
The module deliberately phrases "pole" as a norm blow-up of the sensor on the punctured neighborhood. That is strong enough for RSA and avoids meromorphic machinery at the interface; domain instantiations may later strengthen it to a true analytic pole.
A FrontEnd packages a domain $\Omega$, a candidate predicate, and a field $\Xi$, with the obligation that every candidate forces a boundary hit of $\Xi$ at $1$. The two input hypotheses here are exactly the analytic obligations that make $1/G$ blow up at candidates.
proof idea
One-structure constructor. refine ⟨?_⟩ opens the single FrontEnd field. For arbitrary candidate $z_0$, apply sensorBlowsUpAt_of_tendsto_zero to the pair $(G\to 0$, eventual $G\neq 0)$ to obtain SensorBlowsUpAt (sensorOfObstruction G) z0. Then boundaryHit_theta_of_sensorBlowsUp converts that sensor blow-up into a boundary hit of $\theta\circ\mathcal{J}$ at $1$. A final simpa [sensorOfObstruction] aligns the sensor definition $\mathcal{J}=1/G$ with the Cayley field written in the structure.
why it matters
This is the reusable compiler from obstruction-plus-obligations to a concrete FrontEnd instance. Downstream, goal_frontEnd_from_candidate_obligations packages the canonical goal in which the candidate is the pair of analytic obligations and this definition discharges the front-end compilation; sensorOfObstruction_def records the simp fact $\mathrm{sensorOfObstruction},G=1/G$ used at the interface.
In the RSA pipeline it closes the manuscript step "obstruction → sensor → Cayley field → pole ⇒ boundary hit" without committing to meromorphic language. It sits in the Verification layer rather than the T0–T8 forcing chain, but it is how candidate defects are turned into certified boundary witnesses for later stability audits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.