rs_exists_iff_defect_zero

formal source

  70    exact ⟨hpos, hdef⟩
  71
  72/-- RSExists is equivalent to defect = 0 (for positive values). -/
  73theorem rs_exists_iff_defect_zero {x : ℝ} (hx : 0 < x) :
  74    RSExists x ↔ defect x = 0 := by
  75  constructor
  76  · intro ⟨_, hdef⟩; exact hdef
  77  · intro hdef; exact ⟨hx, hdef⟩
  78
  79/-- The only RSExistent value is 1. -/
  80theorem rs_exists_unique_one : ∀ x : ℝ, RSExists x ↔ x = 1 := by
  81  intro x
  82  constructor
  83  · intro ⟨hpos, hdef⟩
  84    exact (defect_zero_iff_one hpos).mp hdef
  85  · intro hx
  86    rw [hx]
  87    exact ⟨by norm_num, defect_at_one⟩
  88
  89/-- Unity is the unique RSExistent configuration. -/
  90theorem rs_exists_one : RSExists 1 := ⟨by norm_num, defect_at_one⟩
  91
  92/-- There exists exactly one RSExistent value. -/
  93theorem rs_exists_unique : ∃! x : ℝ, RSExists x := by
  94  use 1
  95  constructor
  96  · exact rs_exists_one
  97  · intro y hy
  98    exact (rs_exists_unique_one y).mp hy
  99
 100/-! ## Nothing Cannot RSExist -/
 101
 102/-- For any threshold, sufficiently small positive values have defect exceeding it.
 103    This means "approaching nothing" has unbounded cost. -/