v2.0 — Machine-Checked Principal Results

v2.0 release of the Lean 4 proofs for "Recursive Language Models Through the Admissibility-Dynamics Framework: A Principled Theory of When Recursive Scaffolding Succeeds."

This release contains six standalone Lean 4 proof files covering the principal formal results of the paper, organized into four groups:

Architectural Primitives

• 133_subcall_bounded_scope.lean — Sub-Calls Construct Bounded-Scope Summaries (subcall_output_bounded, subcall_codomain_card_bounded, subcall_composition_inherits_bound): definitional consequence of how RLM sub-calls are typed — an RLM sub-call is a function whose output is bounded in size by a parameter b, so every sub-call output sits in a space of cardinality at most b. Recorded explicitly because subsequent results about RLM compositional reach (sufficiency on bounded-decomposable predicates, insufficiency on global invariants) cite it as a structural premise. The file proves the output bound, the codomain cardinality bound, and that composition of sub-calls inherits the bound.

Sufficient Conditions for Bounded Inconsistency

• 139_sound_decoder_safe_abstention.lean — Sound Decoder Safe Abstention (sound_decoder_yields_safe_abstention, always_abstain_is_safe): soundness-without-completeness consequence of the summary-state framework — a summary-state decoder need not be both sound and complete to support safe behavior. A sound-but-incomplete decoder (positive certifications correct, negatives may be conservative) still supports an abstention policy that achieves zero non-admissible commitments. The policy commits only to actions the decoder positively certifies and otherwise abstains. Safety is preserved at the cost of productivity. First of three conditions the deployment synthesis disjunction packages.
• 143_rlm_rag_architectural_contrast.lean — RLM / RAG Architectural Contrast, escape and inheritance directions (rlm_escapes_rag_on_bounded_decomposable, rlm_inherits_rag_insufficiency_on_non_decomposable, rlm_rag_fault_line): two-sided characterization of where RLM extends RAG and where it doesn't, in a single file. The escape direction: on admissibility predicates that factor into bounded-scope sub-checks, RLM's recursive sub-call structure can certify admissibility through composition of sub-check certificates, where standard RAG's single-shot retrieval cannot. The inheritance direction: on global invariants that do not factor into bounded-scope sub-checks, RLM's recursive structure does not escape the obstruction — no sub-call's bounded-budget output captures the non-decomposable global condition. The fault line between the two regimes is the BoundedDecomposable predicate. Second of three sufficient conditions for bounded-inconsistency deployment.
• 145_runtime_recursion_must_be_measured.lean — Runtime Recursion Must Be Measured, Not Merely Enabled (configured_does_not_force_runtime, runtime_depth_underdetermined_by_config, reach_must_condition_on_runtime_depth): structural distinction between configured and runtime recursion depth — an RLM architecture's configured maximum recursion depth d_max is an upper bound on permitted sub-call nesting, not a guarantee that any specific execution reaches that depth. The actual runtime depth on a given query is a property of the execution trace and must be measured per-execution. Three theorems formalize the consequence: configured depth does not force runtime depth, runtime depth is underdetermined by configuration, and reach claims must condition on the actual runtime depth used. Third of three sufficient conditions for bounded-inconsistency deployment.

Class Closure Under Training

• 148_training_preserves_reach.lean — Training Cannot Extend RLM Reach Beyond Information Bound (training_preserves_unreachability, no_training_extends_reach): class-closure consequence — an RLM architecture with fixed depth d and per-call budget b has a structural information bound determined by (d, b). Training is a transformation that updates policy parameters within the (d, b)-class but does not change the architectural information bound. Therefore training cannot produce a (d, b)-RLM that solves a query the class as a whole cannot solve. The file establishes that training preserves unreachability and that no training scheme extends the reach of the architectural class. Covers the contrapositive of the RLM Insufficiency Theorem developed in the associated paper.

Deployment Synthesis

• 149_constraint_requirement_boundary.lean — Constraint-Requirement Boundary for RLM Deployments (constraint_requirement_satisfiable, any_branch_satisfies_constraint_requirement): synthesis of the architectural results into a deployment-level claim. An RLM deployment that claims uniformly bounded inconsistency across queries must satisfy at least one of three structural conditions: (a) the admissibility predicates lie in the bounded-decomposable class (sub-call composition certifies admissibility, per file 143); (b) the deployment incorporates a sound decoder supporting safe abstention (non-admissible commitments excluded by conservative refusal, per file 139); or (c) the runtime recursion depth on every query is measured and verified to meet the architectural reach requirement (per file 145). A deployment satisfying none of these inherits RAG-like insufficiency on non-decomposable predicates and provides no uniform inconsistency guarantee.

The architectural primitive (file 133) gives the type-bounded sub-call output structure on which the rest of the framework rests. The sufficient-conditions group (139, 143, 145) gives three independent structural paths to bounded inconsistency — safe abstention via sound decoders, sub-check composition over bounded-decomposable predicates, and per-execution runtime-depth verification. The class-closure result (148) restricts what training within a fixed architectural class can achieve. The deployment-synthesis file (149) packages the three sufficient conditions into a single disjunctive deployment-level constraint: any uniformly-bounded-inconsistency RLM deployment must satisfy at least one branch.

All files compile against current Mathlib.

Companion paper: https://doi.org/10.5281/zenodo.19753549