PossibilitySpace

formal source

 369/-- **POSSIBILITY SPACE**: The set of all reachable configurations from a given config.
 370
 371    This is the transitive closure of the Possibility relation. -/
 372def PossibilitySpace (c : Config) : Set Config :=
 373  {y : Config | ∃ n : ℕ, ∃ path : Fin (n+1) → Config,
 374    path ⟨0, Nat.zero_lt_succ n⟩ = c ∧
 375    path ⟨n, Nat.lt_succ_self n⟩ = y ∧
 376    ∀ i : Fin n, path ⟨i.val + 1, Nat.succ_lt_succ i.isLt⟩ ∈
 377                 Possibility (path ⟨i.val, Nat.lt_of_lt_of_le i.isLt (Nat.le_succ n)⟩)}
 378
 379/-- The identity is in every possibility space. -/
 380theorem identity_in_all_possibility_spaces (c : Config) :
 381    identity_config (c.time + 8) ∈ PossibilitySpace c := by
 382  refine ⟨1, fun i => if i.val = 0 then c else identity_config (c.time + 8), ?_, ?_, ?_⟩
 383  · -- path 0 = c
 384    simp
 385  · -- path 1 = identity
 386    simp
 387  · -- each step is in Possibility
 388    intro i
 389    have hi : i.val = 0 := by omega
 390    simp only [hi, Nat.zero_add, ↓reduceIte]
 391    exact identity_always_possible c
 392
 393/-! ## Why Anything Happens: The Master Theorem -/
 394
 395/-- **THE MASTER MODAL THEOREM**: Why change occurs.
 396
 397    For any configuration x ≠ 1:
 398    1. Stasis costs J_stasis(x) = 8 · J(x) > 0
 399    2. There exists y = 1 with J_change(x,1) < J_stasis(x) for some x
 400    3. Therefore, change toward identity is preferred
 401
 402    This answers: "Why does anything happen?"