IndisputableMonolith.Verification.RecognitionStabilityAudit
Barrel module for the Recognition Stability Audit (RSA). It re-exports the core interface, front-end (obstruction/sensor to boundary hit), back-end (Schur/Herglotz pinch forbidding boundary hits), and the RS-to-RL bridge. Verification and RL authors import this single entry point rather than the four submodules. No local theorems; structure is pure aggregation.
claimRecognition Stability Audit package: front-end sends a holomorphic obstruction $G$ through sensor $\mathcal{J}=1/G$ and Cayley field $\Xi=(2\mathcal{J}-1)/(2\mathcal{J}+1)$ to a unit-circle boundary hit; back-end assumes a Schur bound $\|\Xi z\|\le 1$ on an audited region $\Omega$, plus analyticity and nontriviality, and concludes no boundary hits; core and RS$\to$RL layers expose the pipeline for reinforcement-learning control.
background
RSA is the Lean home for the audit described in Recognition_Stability_Audit.tex. The manuscript treats RSA as a compiler from a claimed defect to a rigidity contradiction. The front-end builds a holomorphic obstruction $G$, forms the sensor $\mathcal{J}:=1/G$, and the Cayley field $\Xi:=\theta\mathcal{J}=(2\mathcal{J}-1)/(2\mathcal{J}+1)$. A pole of $\mathcal{J}$ forces $\Xi\to 1$ on the punctured neighborhood (boundary hit).
The back-end assumes a Schur bound $|\Xi z|\le 1$ on an audited region $\Omega$, holomorphic dependence on $\Omega$, and nontriviality ($\Xi$ not identically constant). Under those hypotheses the Schur/Herglotz pinch rules out boundary hits, closing the contradiction.
Core is the RL-friendly interface layer. RStoRL translates Recognition Science control data (MoralState ledger/bonds/skew/energy; fourteen virtues as minimal generators) into practical RL machinery. This barrel only wires those four pieces together.
proof idea
This is a definition/import module, not a proof-bearing declaration. It imports Core, FrontEnd, BackEnd, and RStoRL and exposes them as a single Verification entry point. All mathematical content and tactic machinery live in the submodules; the barrel itself has no theorems, no tactics, and no sorry.
why it matters in Recognition Science
Gives Verification and RL consumers one stable import for the full RSA pipeline. Downstream, RecognitionStabilityAudit.RL makes the pipeline RL-friendly inside Lean: @[rsa_simp] whitelists rewrite lemmas for rsa_simp, and @[rsa_milestone] marks lemmas that rsa_step may apply. Without this barrel, RL automation would have to reach into FrontEnd/BackEnd/Core/RStoRL separately. In the broader RS picture the audit is the analytic rigidity check that a claimed defect cannot sit inside a Schur-bounded holomorphic regime, complementary to the forcing chain (T5 J-uniqueness through T8 dimension) rather than a substitute for it.
scope and limits
- Does not prove any RSA theorem; only re-exports submodule APIs.
- Does not state the Schur bound, analyticity, or nontriviality hypotheses itself.
- Does not implement rsa_simp or rsa_step; those live in the RL submodule.
- Does not encode mass-ladder, alpha-band, or T0–T8 forcing results.
- Does not define MoralState or the fourteen virtues; RStoRL owns those.