pith. machine review for the scientific record. sign in
theorem proved term proof

discreteness_forced

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Term-mode proof.

 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)
 458
 459/-! ## RSExists Requires Discreteness -/
 460
 461/-- A predicate for "stable existence" in the RS sense.
 462
 463    x RSExists if:
 464    1. defect(x) = 0 (it exists)
 465    2. x is isolated in configuration space (it's locked in)
 466
 467    In a continuous space, condition 2 fails for all x. -/

depends on (15)

Lean names referenced from this declaration's body.