427theorem discrete_minimum_stable (D : DiscreteConfigSpace) (_h1 : (1 : ℝ) ∈ D.configs) : 428 ∀ x ∈ D.configs, x ≠ 1 → defect x ≥ D.min_gap := by
proof body
Term-mode proof.
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). -/
depends on (20)
Lean names referenced from this declaration's body.