pith. machine review for the scientific record. sign in
theorem

defect_zero_iff_one

proved
show as:
view math explainer →
module
IndisputableMonolith.Foundation.LawOfExistence
domain
Foundation
line
58 · github
papers citing
37 papers (below)

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.LawOfExistence on GitHub at line 58.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  55/-! ## Core Equivalence Theorems -/
  56
  57/-- **Defect Zero Characterization**: defect(x) = 0 ⟺ x = 1 (for x > 0). -/
  58theorem defect_zero_iff_one {x : ℝ} (hx : 0 < x) : defect x = 0 ↔ x = 1 := by
  59  simp only [defect, J]
  60  constructor
  61  · intro h
  62    have hx0 : x ≠ 0 := hx.ne'
  63    -- (x + 1/x)/2 - 1 = 0 implies (x + 1/x) = 2
  64    have h1 : x + x⁻¹ = 2 := by linarith
  65    -- Multiply by x: x² + 1 = 2x, so (x-1)² = 0
  66    have h2 : x * (x + x⁻¹) = x * 2 := by rw [h1]
  67    have h3 : x^2 + 1 = 2 * x := by field_simp at h2; linarith
  68    nlinarith [sq_nonneg (x - 1)]
  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. -/