Machine-checked Lean 4 proofs for:
"The Non-Locality of Extendability: An Impossibility Theorem for Bounded Information Systems, with Applications to Generative Sequential Systems"
Paper DOI (concept, always resolves to latest): 10.5281/zenodo.19688367
Shawn Kevin Jason — Independent Researcher, Las Vegas, NV
ORCID: 
Eight standalone Lean 4 proof files covering the principal formal results of the paper. The proofs split into three groups: a forward-indistinguishable divergence group containing the load-bearing kernel lemma, its horizon non-convergence corollary, and the policy-adaptive adversary construction showing any deterministic forward-local policy can be driven into non-extendable commitment; a structural lemmas group covering the arithmetic core of the forced-inconsistency construction, admissible-set monotonicity, and the participation invariance underlying the depletion-boundary argument; and a defensive distinctions group establishing through concrete witnesses that NEO is not reducible to POMDP-style partial observability or to viability-based formulations.
Each file is independent and verifies against the current Mathlib release.
031_extendability_indistinguishability.lean — Lemma 2 (Forward-Indistinguishable Divergence)
The load-bearing kernel of the impossibility argument. Two prefixes share an identical bounded horizon projection but differ in extendability under a terminal constraint: with target sum 7 and remaining budget, prefix sum 7 admits a zero-completion (extendable) while prefix sum 8 does not. This divergence witness is the structural fact on which the rest of the impossibility argument is built.
036_horizon_nonconvergence.lean — Corollary 7 (Non-Convergence of Horizon)
For every horizon h, a separating pair exists at depth h+1: two states with identical bounded horizon projections that differ in extendability can be constructed at any horizon depth. No finite evaluation horizon eliminates the failure class.
034_policy_adaptive_adversary.lean — Lemma 5 (Policy-Adaptive Adversary)
For any deterministic forward-local policy, there exists an admissible environment in which the policy is driven into non-extendable commitment. The adversary exploits observational equivalence (from the divergence witness, 031) and determinism: the policy produces the same action for two observationally equivalent states, but in one state that action forecloses all completions. Formalizes the one-step construction; block concatenation for arbitrarily many commitments follows by iteration.
039_participation_invariance.lean — Participation Invariance
Structural precondition for the Constraint Requirement at the depletion boundary. A non-empty admissible set contains at least one element, and a singleton admissible set is non-empty (participation_invariance_singleton). These are minimal but load-bearing facts on which the depletion-boundary argument depends.
046_forced_inconsistency.lean — Forced Inconsistency Arithmetic Core
Once a prefix sum exceeds a target, no nonnegative completion can reduce it back to the target (forced_inconsistency). The companion (admissible_action_preserved) formalizes the dual: a prefix sum equal to the target is trivially completable with a zero-length completion. The two clauses together capture the arithmetic substrate of the witness family.
047_admissible_set_monotone_discrete.lean — Admissible-Set Monotone Refinement
Along any admissible trajectory, the admissible set is monotonically non-increasing: A_{t+1} ⊆ A_t at every step. The companion theorem (admissible_set_strict_decrease) characterizes when the inclusion is strict — strict shrinkage corresponds to commitment, equality means the step preserved all options.
033_neo_distinct_from_partial_observability.lean — Remark 4 (NEO Is Not Partial Observability)
Concrete witness showing that even with complete observation of the current state, two trajectories with identical current observable states can differ in extendability — extendability depends on history outside the current observation. The file constructs two trajectories τ1, τ2 with identical current observation and proves one extendable and the other non-extendable, ruling out any reduction of NEO to POMDP-style partial observability.
049_viability_extendability_orthogonal.lean — Remark 12 (Viability and Extendability Are Orthogonal)
Concrete witness: there exist partial trajectories where the current state is in the viability kernel — at least one action keeps the state within the ongoing state constraint indefinitely — yet the prefix is non-extendable to a terminal target. The file constructs the witness at running sum 9 and proves the full set of orthogonality facts (state viable, viable under all actions, non-extendable from current, viability and extendability orthogonal in general).
| Paper Result | File | Lean Theorem |
|---|---|---|
| Lemma 2 (Forward-Indistinguishable Divergence) | 031_extendability_indistinguishability.lean |
extendability_indistinguishability |
| Corollary 7 (Non-Convergence of Horizon) | 036_horizon_nonconvergence.lean |
horizon_nonconvergence |
| Lemma 5 (Policy-Adaptive Adversary) | 034_policy_adaptive_adversary.lean |
deterministic_same_action, policy_adaptive_adversary |
| Participation Invariance | 039_participation_invariance.lean |
participation_invariance, participation_invariance_singleton |
| Forced Inconsistency Arithmetic Core | 046_forced_inconsistency.lean |
forced_inconsistency, admissible_action_preserved |
| Admissible-Set Monotone Refinement | 047_admissible_set_monotone_discrete.lean |
admissible_set_monotone, admissible_set_strict_decrease |
| Remark 4 (NEO Distinct from Partial Observability) | 033_neo_distinct_from_partial_observability.lean |
neo_distinct_from_partial_observability |
| Remark 12 (Viability and Extendability Orthogonal) | 049_viability_extendability_orthogonal.lean |
viability_and_extendability_orthogonal |
- Open live.lean-lang.org
- Confirm the dropdown in the upper right is set to Latest Mathlib
- Paste the contents of any
.leanfile into the editor - Wait for checking to complete — "No goals" on each theorem and no errors in the Problems pane confirms verification
Each file is independent; no cross-file imports are required.
These proofs verify the formal logical structure of the stated results — the divergence kernel underlying NEO Lemma 2, the horizon non-convergence corollary, the structural admissibility-set lemmas, and the defensive distinctions establishing that NEO is not reducible to POMDP-style partial observability or to viability-based formulations. They do not establish:
- The full policy-level impossibility argument (NEO Theorem 3, developed in Sections 3–4 of the paper)
- The empirical constructive instantiation over 30,000 episodes across 16 configurations (Section 6)
- The cross-domain unification across planning, reinforcement learning, and language generation (Section 5)
The foundational projection-theoretic result of which NEO is a forward-case specialization is developed in:
Projection Insufficiency and Trajectory Realization: A Unified Constraint-Based Framework for Bounded Systems — DOI: 10.5281/zenodo.19633241 (Lean proofs: 10.5281/zenodo.19687629)
The stochastic extension of the NEO result, with a quantitative inconsistency-accumulation lower bound and a matching positive representational theorem, is developed in:
Inconsistency Accumulation in Forward-Local Sequential Policies: A Lower Bound under Delayed Constraints — DOI: 10.5281/zenodo.19688628 (Lean proofs: 10.5281/zenodo.19687094)
MIT