RSExists_stable

formal source

 465    2. x is isolated in configuration space (it's locked in)
 466
 467    In a continuous space, condition 2 fails for all x. -/
 468def RSExists_stable (x : ℝ) (config_space : Set ℝ) : Prop :=
 469  defect x = 0 ∧ ∃ ε > 0, ∀ y ∈ config_space, y ≠ x → |y - x| > ε
 470
 471/-- **Theorem**: RSExists_stable is impossible in connected configuration spaces containing 1.
 472
 473    If config_space is connected and contains 1, then 1 is not isolated,
 474    so RSExists_stable 1 config_space is false. -/
 475theorem rs_exists_impossible_continuous
 476    (config_space : Set ℝ)
 477    (h1 : (1 : ℝ) ∈ config_space)
 478    (_hconn : IsConnected config_space)
 479    (hdense : ∀ x ∈ config_space, ∀ ε > 0, ∃ y ∈ config_space, y ≠ x ∧ |y - x| < ε) :
 480    ¬RSExists_stable 1 config_space := by
 481  intro ⟨_, ε, hε, hisolated⟩
 482  obtain ⟨y, hy_in, hy_ne, hy_close⟩ := hdense 1 h1 ε hε
 483  have := hisolated y hy_in hy_ne
 484  linarith
 485
 486/-- **Corollary**: Stable existence requires discrete configuration space.
 487
 488    This is the formalization of the key insight:
 489    The cost landscape J forces discreteness because only discrete
 490    configurations can be "trapped" at the unique J-minimum (x = 1).
 491
 492    Note: RSExists_stable x config_space means x has defect 0 and is isolated
 493    from config_space. This doesn't require x ∈ config_space, but in practice
 494    we're interested in cases where x = 1 (the unique defect minimum). -/
 495theorem stable_existence_requires_discrete :
 496    (∃ x config_space, RSExists_stable x config_space) →
 497    ∃ config_space : Set ℝ, ∃ x, RSExists_stable x config_space := by
 498  intro ⟨x, config_space, hstable⟩