language-models

Machine-checked Lean 4 proofs for "Recursive Language Models Through the Admissibility-Dynamics Framework." Covers RLM sub-call architecture, three sufficient conditions for bounded-inconsistency deployment (safe abstention, bounded-decomposable predicates, runtime depth verification), training class closure, and the deployment-boundary synthesis.

Machine-checked Lean 4 proofs for "Minimal Topologies of Forward-Local Failure in AI Systems: The Hamiltonian Microscope" — hamiltonian-path as abstract ConstraintSystem instance (inheriting Sudoku-Microscope theorems) and Layer 2 silent-commit signature formalization with provider-agnostic well-definedness.

Machine-checked Lean 4 proofs for "Commitment Failure Under Local Decision-Making in AI Systems: The Sudoku Microscope" — local-global separation, catastrophic commitment foreclosure, forced-gate safety, and bucket sufficiency in abstract constraint systems.

Machine-checked Lean 4 proofs for "Language Model Hallucinations: An Impossibility Theorem and Its Architectural Consequences." Covers Theorem 1 (impossibility of guaranteed consistency), certification-depth lower bounds, mitigation boundaries for CoT / grammar / rerank, and intrinsic/extrinsic DCF taxonomy.

Machine-checked Lean 4 proofs for "From Recursive Scaffolding to Admissibility-First Construction: Mechanism, Stability, and Failure-Mode Decomposition on OOLONG-Pairs" — filter recall preservation, oracle construction sufficiency, endpoint-factorization insufficiency, and pair-precision amplification under independence.