 152/-! ## Structured Set -/
 153
 154/-- The structured set S = {x ∈ ℝ₊ : defect(x) = 0} = {1}. -/
 155def StructuredSet : Set ℝ := {x : ℝ | 0 < x ∧ defect x = 0}
 156
 157theorem structured_set_singleton : StructuredSet = {1} := by
 158  ext x
 159  simp only [StructuredSet, Set.mem_setOf_eq, Set.mem_singleton_iff]
 160  constructor
 161  · intro ⟨hpos, hdef⟩; exact (defect_zero_iff_one hpos).mp hdef
 162  · intro h; subst h; exact ⟨one_pos, defect_at_one⟩
 163
 164/-- Membership in structured set ⟺ existence. -/
 165theorem mem_structured_iff_exists {x : ℝ} : x ∈ StructuredSet ↔ Exists x :=
 166  ⟨fun ⟨hpos, hdef⟩ => ⟨hpos, hdef⟩, fun ⟨hpos, hdef⟩ => ⟨hpos, hdef⟩⟩
 167
 168/-! ## Economic Inevitability -/
 169
 170/-- **Existence is Economically Inevitable**: 1 is the unique minimizer of defect. -/
 171theorem existence_economically_inevitable :
 172    ∃! x : ℝ, 0 < x ∧ ∀ y, 0 < y → defect x ≤ defect y := by
 173  refine ⟨1, ⟨one_pos, ?_⟩, ?_⟩
 174  · intro y hy
 175    rw [defect_at_one]
 176    exact defect_nonneg hy
 177  · intro z ⟨hzpos, hzmin⟩
 178    have h1 : defect z ≤ defect 1 := hzmin 1 one_pos
 179    rw [defect_at_one] at h1
 180    have h2 : defect z = 0 := le_antisymm h1 (defect_nonneg hzpos)
 181    exact (defect_zero_iff_one hzpos).mp h2
 182
 183/-! ## Complete Law of Existence -/
 184
 185/-- **Complete Law of Existence**: The following are equivalent for x > 0:

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.