exists_implies_defect_zero

formal source

  69  · intro h; simp [h]
  70
  71/-- **Law of Existence (Forward)**: Existence implies defect is zero. -/
  72theorem exists_implies_defect_zero {x : ℝ} (h : Exists x) : defect x = 0 :=
  73  h.defect_zero
  74
  75/-- **Law of Existence (Backward)**: Zero defect (with x > 0) implies existence. -/
  76theorem defect_zero_implies_exists {x : ℝ} (hpos : 0 < x) (hdef : defect x = 0) :
  77    Exists x := ⟨hpos, hdef⟩
  78
  79/-- **Law of Existence (Biconditional)**: x exists ⟺ defect collapses. -/
  80theorem law_of_existence (x : ℝ) : Exists x ↔ DefectCollapse x :=
  81  ⟨fun ⟨hpos, hdef⟩ => ⟨hpos, hdef⟩, fun ⟨hpos, hdef⟩ => ⟨hpos, hdef⟩⟩
  82
  83/-- **Existence Characterization**: x exists ⟺ x = 1. -/
  84theorem exists_iff_unity {x : ℝ} (hx : 0 < x) : Exists x ↔ x = 1 :=
  85  ⟨fun ⟨_, hdef⟩ => (defect_zero_iff_one hx).mp hdef,
  86   fun h => ⟨hx, (defect_zero_iff_one hx).mpr h⟩⟩
  87
  88/-- **Unity is Unique Existent**: ∀ x, Exists x ⟺ x = 1. -/
  89theorem unity_unique_existent : ∀ x : ℝ, Exists x ↔ x = 1 := by
  90  intro x
  91  constructor
  92  · intro ⟨hpos, hdef⟩; exact (defect_zero_iff_one hpos).mp hdef
  93  · intro h; subst h; exact ⟨one_pos, defect_at_one⟩
  94
  95/-- Alias for `defect_at_one`. -/
  96theorem defect_one : defect 1 = 0 := defect_at_one
  97
  98/-- Defect is strictly positive for x ≠ 1. -/
  99theorem defect_pos_of_ne_one {x : ℝ} (hx : 0 < x) (hne : x ≠ 1) : 0 < defect x := by
 100  have h_nn := defect_nonneg hx
 101  have h_ne_zero : defect x ≠ 0 := fun h => hne ((defect_zero_iff_one hx).mp h)
 102  exact lt_of_le_of_ne h_nn (Ne.symm h_ne_zero)