Machine-checked Lean 4 proofs for "Path-Game GAF Pilot v0.1: Cross-Provider Program Handoff v1.7" — 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 "Sudoku as a Microscope for Non-Extendable Commitment: Empirical Validation of Global Admissibility Filtering" — 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 "Inconsistency Accumulation in Forward-Local Sequential Policies." Quantitative lower bound E[I_N] >= N/|U| with measure-theoretic verification via two independent proof paths, plus Proposition 1 summary sufficiency and Section 7 arithmetic witnesses.

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 "The Non-Locality of Extendability." Forward-case impossibility result for bounded information systems: the divergence kernel, horizon non-convergence, structural admissibility lemmas, and witnesses distinguishing extendability from POMDP observability and viability.

Machine-checked Lean 4 proofs for "Projection Insufficiency and Trajectory Realization." Establishes that no function on a non-injective projection can recover a trajectory-dependent property, with specializations to language-model hallucination, planning, RL, POMDPs, and constraint propagation.

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.