modal_distance

formal source

  48
  49    This measures how "far apart" two possibilities are in modal space.
  50    Key property: d(x,x) = 0, d(x,y) = d(y,x), triangle inequality. -/
  51noncomputable def modal_distance (c1 c2 : Config) : ℝ :=
  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.