v2.0 — Machine-Checked Principal Results

v2.0 release of the Lean 4 proofs for "Projection Insufficiency and Trajectory Realization: A Unified Constraint-Based Framework for Bounded Systems."

Expands the v1.0 set (three foundational files) to nine standalone Lean 4 proof files covering the principal formal results of the paper, organized into four groups:

Foundational Results

• 004_projection_insufficiency.lean — Projection Insufficiency Theorem (projection_insufficiency) and Non-recoverability is Structural (Corollary 3): when a projection map P : T → R is non-injective and a property Φ : T → Y differs across some indistinguishability class of P, no function f : R → Y can recover Φ from P. The headline impossibility result; Corollary 3 follows immediately as a structural restatement.
• 012_admissibility_nonlocal.lean — Admissibility is Trajectory-Dependent (admissibility_nonlocal) and Non-Locality of Admissibility (Corollary 12): specializes the projection-insufficiency obstruction to predicates — when admissibility is trajectory-dependent relative to a bounded projection, no function on the projection alone recovers the admissibility predicate. Self-contained: includes a re-statement of the underlying theorem so it can be verified in isolation.
• 015_contractive_fixed_point_unique.lean — Constructive Resolution under Contractivity (contractive_fixed_point_unique): under a contractive self-map K : X → X with constant q < 1, K has at most one fixed point. The constructive partial converse to the impossibility results above.

Trajectory-Level Enforcement Template

• 021_trajectory_admissibility_enforcement.lean — Trajectory Admissibility Enforcement (Proposition 10): the architectural template instantiated by every specialization below. Defines the SameFiberConflict predicate (same-projection / different-admissibility pattern); proves deterministic (no_deterministic_local_policy_guarantees_admissibility) and stochastic (no_stochastic_local_policy_guarantees_admissibility) policy forms. Each file in the AI-domain and adjacent-formalisms groups below is a domain-specific instance of this template.

AI-Domain Specializations (Section 9)

• 018_lm_hallucination_ceiling.lean — Language-Model Hallucination Ceiling: a language model with bounded context window of depth h is a forward-local system whose next-token selection is a function of the bounded context projection. The SameContextHallucinationRisk predicate is the LM specialization of the same-fiber conflict; deterministic (lm_hallucination_ceiling_deterministic) and stochastic (lm_hallucination_ceiling_stochastic) decoder forms.
• 019_planning_dead_end_boundary.lean — Planning Dead-End Detection Boundary: a planner with bounded local state representation (lookahead horizon plus current state, abstraction, or factored variables) is a forward-local system whose action selection is a function of that bounded representation. The SameRepDeadEndConflict predicate yields deterministic (planning_dead_end_boundary_deterministic) and stochastic (planning_dead_end_boundary_stochastic) planner forms.
• 020_rl_terminal_constraint_boundary.lean — RL Terminal-Constraint Boundary: an RL policy operating under a finite value horizon h evaluates states using a bounded value-projection of the trajectory. The SameProjTerminalConflict predicate yields deterministic (rl_terminal_constraint_boundary_deterministic) and stochastic (rl_terminal_constraint_boundary_stochastic) policy forms.

Adjacent Formalisms (Section 10)

• 022_pomdp_belief_state_insufficiency.lean — POMDP Belief-State Insufficiency: a POMDP agent that derives its belief state from its observation history acts on a function of that history. When two trajectories produce identical observation histories, the composition belief∘obs is a lossy projection; the SameBeliefAdmissibilityConflict predicate yields deterministic (pomdp_belief_state_insufficient_deterministic) and stochastic (pomdp_belief_state_insufficient_stochastic) forms.
• 023_constraint_propagation_boundary.lean — Constraint-Propagation Infeasibility Boundary: arc-consistency and generalized arc-consistency algorithms operate on a bounded local view of a partial assignment. The SameViewFeasibilityConflict predicate yields deterministic (constraint_propagation_boundary_deterministic) and nondeterministic (constraint_propagation_boundary_nondeterministic) propagation forms.

The foundational impossibility (file 004) and its constructive partial converse (file 015) establish the framework's two pillars. File 021 codifies the canonical same-fiber conflict pattern as a reusable template, and the five domain specializations (018, 019, 020, 022, 023) each instantiate that template for a specific AI or formal-systems setting.

All files compile against current Mathlib.

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