theorem
proved
term proof
possibility_space_connected
show as:
view Lean formalization →
formal statement (Lean)
94theorem possibility_space_connected (c : Config) :
95 ∃ path : ℕ → Config, path 0 = c ∧
96 ∀ n, ∃ m > n, (path m).value = 1 := by
proof body
Term-mode proof.
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. -/