self_ref_not_rs_true

formal source

 165    - c encodes "I don't stabilize"
 166
 167    Then c cannot be RSTrue. -/
 168theorem self_ref_not_rs_true
 169    (c : ℝ)
 170    (h_encodes : ∀ P : Prop, (P ↔ RSStab c) → (P ↔ ¬RSStab c) → False)
 171    (h_correct : RSStab c ↔ ¬RSStab c) :
 172    False := by
 173  -- h_correct is P ↔ ¬P which is directly contradictory
 174  by_cases hs : RSStab c
 175  · exact (h_correct.mp hs) hs
 176  · exact hs (h_correct.mpr hs)
 177
 178/-- The stabilization status of any configuration is definite.
 179    Either defect = 0 or defect ≠ 0. There's no third option. -/
 180theorem stab_decidable (c : ℝ) : RSStab c ∨ ¬RSStab c := by
 181  exact em (RSStab c)
 182
 183/-- For real configurations, RSDiverge is actually impossible
 184    (defect is a real number, can't be greater than all reals). -/
 185theorem diverge_impossible (c : ℝ) : ¬RSDiverge c := by
 186  intro h
 187  -- RSDiverge c says ∀ C, defect c > C
 188  -- Take C = defect c
 189  have : defect c > defect c := h (defect c)
 190  linarith
 191
 192/-- Every real configuration is either RSStab or RSOutside (never RSDiverge). -/
 193theorem config_classification (c : ℝ) : RSStab c ∨ RSOutside c := by
 194  by_cases hs : RSStab c
 195  · left; exact hs
 196  · right
 197    exact ⟨hs, diverge_impossible c⟩
 198