discrete_minimum_stable

formal source

 424    all other configurations have defect ≥ min_gap.
 425
 426    This is why discrete spaces support stable existence. -/
 427theorem discrete_minimum_stable (D : DiscreteConfigSpace) (_h1 : (1 : ℝ) ∈ D.configs) :
 428    ∀ x ∈ D.configs, x ≠ 1 → defect x ≥ D.min_gap := by
 429  intro x hx hx_ne
 430  exact D.gap_property x hx hx_ne
 431
 432/-! ## The Discreteness Forcing Theorem -/
 433
 434/-- **The Discreteness Forcing Theorem**
 435
 436    For stable existence (RSExists), the configuration space must be discrete.
 437
 438    Proof sketch:
 439    1. RSExists requires defect → 0 (Law of Existence)
 440    2. Defect = 0 only at x = 1 (unique minimum)
 441    3. In a continuous space, x = 1 is not isolated (continuous_space_no_lockIn)
 442    4. Therefore, no configuration can be "locked in" to existence
 443    5. For stable existence, we need discrete configurations
 444
 445    Conclusion: The cost landscape J forces discreteness.
 446    Continuous configuration spaces cannot support stable existence.
 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)