defect_nonneg

formal source

  35@[simp] theorem defect_at_one : defect 1 = 0 := by simp [defect, J]
  36
  37/-- Defect is non-negative for positive arguments. -/
  38theorem defect_nonneg {x : ℝ} (hx : 0 < x) : 0 ≤ defect x := by
  39  simp only [defect, J]
  40  have hx0 : x ≠ 0 := hx.ne'
  41  have h : 0 ≤ (x - 1)^2 / x := by positivity
  42  calc (x + x⁻¹) / 2 - 1 = ((x - 1)^2 / x) / 2 := by field_simp; ring
  43    _ ≥ 0 := by positivity
  44
  45/-! ## The Existence Predicate -/
  46
  47/-- **Existence Predicate**: x exists in the RS framework iff x > 0 and defect(x) = 0. -/
  48structure Exists (x : ℝ) : Prop where
  49  pos : 0 < x
  50  defect_zero : defect x = 0
  51
  52/-- **Defect Collapse Predicate**: Equivalent formulation. -/
  53def DefectCollapse (x : ℝ) : Prop := 0 < x ∧ defect x = 0
  54
  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)]