discreteness_forced

formal source

 447
 448    Note: The hypothesis includes x > 0 because defect is only meaningful for positive x
 449    (J(x) = (x + 1/x)/2 - 1 requires x ≠ 0, and for x < 0, J(x) < 0 ≠ defect minimum). -/
 450theorem discreteness_forced :
 451    (∀ x : ℝ, 0 < x → defect x = 0 → x = 1) ∧  -- Unique minimum
 452    (∀ ε > 0, ∃ y : ℝ, y ≠ 1 ∧ defect y < ε) →  -- No isolation in ℝ
 453    ¬∃ (x : ℝ), 0 < x ∧ x ≠ 1 ∧ defect x = 0 := by      -- No other stable points
 454  intro ⟨hunique, _hno_isolation⟩
 455  push_neg
 456  intro x hx_pos hx_ne hdef
 457  exact hx_ne (hunique x hx_pos hdef)
 458
 459/-! ## RSExists Requires Discreteness -/
 460
 461/-- A predicate for "stable existence" in the RS sense.
 462
 463    x RSExists if:
 464    1. defect(x) = 0 (it exists)
 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