  52  J_transition c1.value c2.value c1.pos c2.pos
  53
  54/-- Modal distance is non-negative. -/
  55lemma modal_distance_nonneg (c1 c2 : Config) : 0 ≤ modal_distance c1 c2 := by
  56  unfold modal_distance J_transition
  57  apply mul_nonneg (abs_nonneg _)
  58  apply div_nonneg
  59  · apply add_nonneg (J_nonneg c1.pos) (J_nonneg c2.pos)
  60  · norm_num
  61
  62/-- Modal distance to self is zero. -/
  63lemma modal_distance_self (c : Config) : modal_distance c c = 0 := by
  64  unfold modal_distance
  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)) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.