v1.0 — Machine-Checked Principal Results

Initial release of the Lean 4 proofs for "Recursive Language Models Through the Admissibility-Dynamics Framework: A Principled Theory of When Recursive Scaffolding Succeeds."
Covers the principal results: the architectural primitive that RLM sub-call outputs are type-bounded by the per-call budget, the three sufficient conditions for bounded-inconsistency RLM deployment (sound-decoder safe abstention, bounded-decomposable predicates that admit sub-check certification, runtime recursion depth verified per execution), the class-closure consequence that training within a fixed (d, b)-architectural class cannot extend reach beyond the class's information bound, the two-sided RLM-vs-RAG architectural contrast (escape direction on bounded-decomposable predicates, inheritance direction on non-decomposable global invariants), and the deployment-boundary synthesis packaging the three sufficient conditions into a constraint-requirement disjunction. All files compile against current Mathlib.
Companion paper: [https://zenodo.org/records/19753550]