`IndisputableMonolith.Verification.RecognitionStabilityAudit`

IndisputableMonolith/Verification/RecognitionStabilityAudit.lean · 23 lines · 0 declarations

Explainer status: ready · generated 2026-08-13 18:34:30.582174+00:00

   1import IndisputableMonolith.Verification.RecognitionStabilityAudit.Core
   2import IndisputableMonolith.Verification.RecognitionStabilityAudit.FrontEnd
   3import IndisputableMonolith.Verification.RecognitionStabilityAudit.BackEnd
   4import IndisputableMonolith.Verification.RecognitionStabilityAudit.RStoRL
   5
   6/-!
   7# Recognition Stability Audit (RSA) (umbrella module)
   8
   9Paper reference: `papers/tex/Recognition_Stability_Audit.tex`.
  10
  11This module re-exports the RSA core interface so downstream code can simply:
  12
  13`import IndisputableMonolith.Verification.RecognitionStabilityAudit`
  14
  15and then work with:
  16
  17- `RecognitionStabilityAudit.Problem`
  18- `RecognitionStabilityAudit.FrontEnd`
  19- `RecognitionStabilityAudit.BackEnd`
  20- `RecognitionStabilityAudit.correctness`
  21- `RecognitionStabilityAudit.RStoRL` — RS→RL bridge (virtue actions, lexicographic selection, Gibbs)
  22-/
  23

source mirrored from github.com/jonwashburn/shape-of-logic