IsStable

formal source

 310
 311/-- A configuration is "stable" if it's a strict local minimum of J.
 312    This means there's a neighborhood where it's the unique minimizer. -/
 313def IsStable (x : ℝ) : Prop :=
 314  ∃ ε > 0, ∀ y : ℝ, y ≠ x → |y - x| < ε → defect x < defect y
 315
 316/-- In a path-connected space with continuous J, there are no isolated stable points.
 317
 318    Intuition: If x is stable with defect(x) = 0, and the space is path-connected,
 319    we can find a path from x to any nearby point. Along this path, defect varies
 320    continuously, so we can get arbitrarily close to zero defect at other points.
 321
 322    This prevents "locking in" to x — we can always drift away with negligible cost.
 323
 324    Note: The actual proof requires the intermediate value theorem and connectedness.
 325    We use ℝ as the configuration space for concreteness. -/
 326theorem continuous_no_isolated_zero_defect :
 327    ∀ x : ℝ, 0 < x → defect x = 0 →
 328    ∀ ε > 0, ∃ z : ℝ, z ≠ x ∧ |z - x| < ε ∧ defect z < ε := by
 329  intro x hx_pos hx ε hε
 330  -- Since defect = 0 implies x = 1, we work at x = 1
 331  have hx_eq_1 : x = 1 := (defect_zero_iff_one hx_pos).mp hx
 332  subst hx_eq_1
 333  -- Take z = 1 + min(ε/2, 1/2) to ensure z > 0 and close to 1
 334  let t := min (ε / 2) (1 / 2 : ℝ)
 335  have ht_pos : t > 0 := by positivity
 336  have ht_le_half : t ≤ 1 / 2 := min_le_right _ _
 337  use 1 + t
 338  constructor
 339  · linarith
 340  constructor
 341  · simp only [add_sub_cancel_left, abs_of_pos ht_pos]
 342    calc t ≤ ε / 2 := min_le_left _ _
 343      _ < ε := by linarith