modal_distance_symm

formal source

  65  exact J_transition_self c.pos
  66
  67/-- Modal distance is symmetric. -/
  68lemma modal_distance_symm (c1 c2 : Config) :
  69    modal_distance c1 c2 = modal_distance c2 c1 := by
  70  unfold modal_distance
  71  exact J_transition_symm c1.pos c2.pos
  72
  73/-! ## Possibility Space Topology -/
  74
  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