possibility_space_connected

formal source

  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
 116
 117/-- Curvature at identity. -/
 118lemma curvature_at_identity : possibility_curvature (identity_config 0) = 2 := by
 119  simp only [possibility_curvature, identity_config, inv_one, one_pow]
 120  ring
 121
 122/-- Curvature is positive everywhere. -/
 123lemma curvature_pos (c : Config) : 0 < possibility_curvature c := by
 124  unfold possibility_curvature