Counterfactual

formal source

 361    1. y ∈ P(c) (y was possible)
 362    2. y ≠ Actualize(c) (y wasn't chosen)
 363    3. J(y) > J(Actualize c) (y costs more, which is why it wasn't chosen) -/
 364def Counterfactual (c : Config) : Set Config :=
 365  {y : Config | y ∈ Possibility c ∧ y ≠ Actualize c ∧ J y.value > J (Actualize c).value}
 366
 367/-! ## Possibility Space -/
 368
 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