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. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.