J

formal source

  26/-! ## The Cost/Defect Functional -/
  27
  28/-- The canonical cost functional J(x) = ½(x + x⁻¹) - 1. -/
  29noncomputable def J (x : ℝ) : ℝ := (x + x⁻¹) / 2 - 1
  30
  31/-- The defect functional. Equals J for positive x. -/
  32noncomputable def defect (x : ℝ) : ℝ := J x
  33
  34/-- Defect at unity is zero. -/
  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]