DiscreteConfigSpace

formal source

 406
 407    In a discrete space, adjacent configurations are separated by a minimum
 408    "gap" in J-cost. This allows configurations to be "trapped" at minima. -/
 409structure DiscreteConfigSpace where
 410  /-- The discrete configuration values -/
 411  configs : Finset ℝ
 412  /-- All configs are positive -/
 413  configs_pos : ∀ x ∈ configs, 0 < x
 414  /-- There's a minimum gap between adjacent configurations' J-costs -/
 415  min_gap : ℝ
 416  min_gap_pos : 0 < min_gap
 417  /-- The gap property: any config x ≠ 1 has defect at least min_gap.
 418      This ensures that 1 is strictly isolated as the unique minimum. -/
 419  gap_property : ∀ x : ℝ, x ∈ configs → x ≠ 1 → defect x ≥ min_gap
 420
 421/-- **Key Theorem**: In a discrete configuration space, the unique minimum is stable.
 422
 423    If 1 ∈ configs (the point with defect = 0), then it's strictly isolated:
 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)