identity_in_ball

formal source

  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.
 109
 110    κ(c) = J''(c.value) = 1/c.value² + 1/c.value⁴
 111
 112    At identity (c = 1): κ(1) = 2
 113    This curvature determines how "spread out" possibilities are. -/
 114noncomputable def possibility_curvature (c : Config) : ℝ :=
 115  c.value⁻¹^2 + c.value⁻¹^4