theorem
proved
term proof
rs_exists_impossible_continuous
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Term-mode proof.
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). -/