Problem
plain-language theorem explainer
An RSA problem instance packages three data: an audited complex region Ω, a candidate existence predicate on ℂ, and a Cayley field Ξ. Anyone setting up a Recognition Stability Audit cites this as the input bundle. It is a pure structure definition with no proof obligations of its own; downstream FrontEnd, BackEnd, and correctness fill the checklist.
Claim. An RSA problem instance is a triple $(\Omega, C, \Xi)$ where $\Omega \subseteq \mathbb{C}$ is the audited region (typically a chart domain normalized to the unit disk), $C : \mathbb{C} \to \mathrm{Prop}$ is the candidate existence predicate to be ruled out on $\Omega$, and $\Xi : \mathbb{C} \to \mathbb{C}$ is the audited Cayley field (paper form $\Xi = (2\mathcal{J}-1)/(2\mathcal{J}+1)$ after pullback).
background
Recognition Stability Audit (RSA) is the Lean interface for the pipeline in Recognition_Stability_Audit.tex. Morally it is a compiler: the front-end turns a candidate existence claim into a boundary-hit condition for a bounded Cayley field Ξ (candidate ⇒ sensor pole ⇒ Ξ → 1); the back-end issues a finite certificate that Ξ stays in the Schur class on the audited region; correctness says both sides together make the candidate impossible there.
The cost primitive behind the sensor is the canonical reciprocal cost $J(x) = \tfrac12(x+x^{-1})-1$ on $\mathbb{R}_{>0}$ (formalized as Jcost). This module does not re-prove J-uniqueness (T5); it only references the cost layer. The Cayley field Ξ is the paper-facing transform of a sensor 𝓙, written $\Xi=(2\mathcal{J}-1)/(2\mathcal{J}+1)$ after pullback to the complex chart.
Problem is the RL-friendly checklist entry that holds the three inputs every audit needs: region, candidate predicate, and Ξ. Sibling structures (FrontEnd, BackEnd, SchurOn, BoundaryHitAt) attach the proof obligations around this bundle.
proof idea
No proof. This is a structure definition with three fields (Ω, Candidate, Xi) and field doc-comments only. Instantiation is by supplying a set in ℂ, a Prop-valued predicate, and a complex map; no tactics or lemmas fire at this declaration.
why it matters
Problem is the root input type for the RSA compiler. Downstream cosmology and gravity modules that need a stability-audit framing (dark-energy scale and equation of state, Ω_Λ bounds, flatness and horizon bookkeeping, J-cost equilibrium profiles) sit on the same verification spine that consumes Problem instances via FrontEnd/BackEnd/correctness.
In framework terms it sits after the cost layer (T5 J-uniqueness, RCL) and before any Schur certificate: without a packaged (Ω, candidate, Ξ) there is nothing for the finite Schur bound to kill. The module doc frames the design as intentionally structure-shaped so each RSA step is a small obligation list rather than a monolithic theorem. It does not itself close any open bridge from the ledger floor (T−1–T8); it only standardizes the audit payload those bridges would feed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.