modal_completeness

formal source

 234
 235    The modal manifold is "geodesically complete" in the sense that
 236    every configuration has a finite-cost path to the attractor. -/
 237theorem modal_completeness (c : Config) :
 238    ∃ path : List Config, path.head? = some c ∧
 239    path.getLast? = some (identity_config (c.time + 8)) := by
 240  use [c, identity_config (c.time + 8)]
 241  simp only [List.head?_cons, List.getLast?_cons_cons, List.getLast?_singleton, and_self]
 242
 243/-! ## Boundaries of Possibility -/
 244
 245/-- **IMPOSSIBLE REGION**: Where J → ∞.
 246
 247    As x → 0⁺, J(x) → ∞, making these configurations unreachable at finite cost.
 248    This is the "boundary of possibility." -/
 249def ImpossibleRegion : Set ℝ := {x : ℝ | x ≤ 0}
 250
 251/-- The impossible region has infinite cost. -/
 252theorem impossible_infinite_cost (x : ℝ) (hx : x ≤ 0) :
 253    ¬∃ c : Config, c.value = x := by
 254  intro ⟨c, hc⟩
 255  have : 0 < c.value := c.pos
 256  linarith
 257
 258/-- **BOUNDARY OF POSSIBILITY**: The limit of the possible.
 259
 260    ∂P = {x : x → 0⁺} where J(x) → ∞
 261
 262    This is NOT a configuration, but a limit of configurations. -/
 263def PossibilityBoundary : Set ℝ := {x : ℝ | x = 0}
 264
 265/-- The boundary is unreachable at finite cost. -/
 266theorem boundary_unreachable :
 267    ∀ c : Config, c.value ≠ 0 := by