PossibilityBall

formal source

  75/-- **POSSIBILITY BALL**: The set of configs within modal distance r of c.
  76
  77    B_r(c) = {y : modal_distance(c, y) ≤ r} -/
  78def PossibilityBall (c : Config) (r : ℝ) : Set Config :=
  79  {y : Config | modal_distance c y ≤ r}
  80
  81/-- Identity is in every sufficiently large possibility ball.
  82
  83    **Note**: The radius r must be large enough to contain the path from c to identity.
  84    For r > modal_distance(c, identity), the identity is guaranteed to be in the ball. -/
  85lemma identity_in_ball (c : Config) (hr : r > modal_distance c (identity_config c.time)) :
  86    ∃ t : ℕ, identity_config t ∈ PossibilityBall c r := by
  87  use c.time
  88  simp only [PossibilityBall, Set.mem_setOf_eq]
  89  exact le_of_lt hr
  90
  91/-- **CONNECTIVITY**: Every configuration connects to identity.
  92
  93    This gives possibility space a "star" topology with identity at the center. -/
  94theorem possibility_space_connected (c : Config) :
  95    ∃ path : ℕ → Config, path 0 = c ∧
  96    ∀ n, ∃ m > n, (path m).value = 1 := by
  97  use fun n => if n = 0 then c else identity_config (c.time + 8 * n)
  98  constructor
  99  · simp
 100  · intro n
 101    use n + 1
 102    constructor
 103    · omega
 104    · simp [identity_config]
 105
 106/-! ## Possibility Curvature -/
 107
 108/-- **POSSIBILITY CURVATURE**: The curvature of possibility space at a config.