continuous_space_no_lockIn

formal source

 388    there's always a low-cost escape route.
 389
 390    This is why continuous spaces don't support stable existence. -/
 391theorem continuous_space_no_lockIn (x : ℝ) (hx_pos : 0 < x) (hx_exists : defect x = 0) :
 392    ∀ ε > 0, ∃ y : ℝ, y ≠ x ∧ |y - x| < ε := by
 393  intro ε hε
 394  have hx_eq_one : x = 1 := (defect_zero_iff_one hx_pos).mp hx_exists
 395  subst hx_eq_one
 396  -- Any nearby point exists
 397  use 1 + ε / 2
 398  constructor
 399  · linarith
 400  · simp only [add_sub_cancel_left, abs_of_pos (by linarith : ε / 2 > 0)]
 401    linarith
 402
 403/-! ## Stability in Discrete Spaces -/
 404
 405/-- A discrete configuration space with finite step cost.
 406
 407    In a discrete space, adjacent configurations are separated by a minimum
 408    "gap" in J-cost. This allows configurations to be "trapped" at minima. -/
 409structure DiscreteConfigSpace where
 410  /-- The discrete configuration values -/
 411  configs : Finset ℝ
 412  /-- All configs are positive -/
 413  configs_pos : ∀ x ∈ configs, 0 < x
 414  /-- There's a minimum gap between adjacent configurations' J-costs -/
 415  min_gap : ℝ
 416  min_gap_pos : 0 < min_gap
 417  /-- The gap property: any config x ≠ 1 has defect at least min_gap.
 418      This ensures that 1 is strictly isolated as the unique minimum. -/
 419  gap_property : ∀ x : ℝ, x ∈ configs → x ≠ 1 → defect x ≥ min_gap
 420
 421/-- **Key Theorem**: In a discrete configuration space, the unique minimum is stable.