jcost_unique_minimum

formal source

  49/-- **THEOREM IC-005.2**: J-cost has a unique minimum at x = 1.
  50    This proves that the "ground state" of RS is uniquely determined
  51    and can be verified in constant time. -/
  52theorem jcost_unique_minimum : ∀ x : ℝ, x > 0 → Jcost 1 ≤ Jcost x := by
  53  intro x hx
  54  rw [Cost.Jcost_unit0]
  55  exact Cost.Jcost_nonneg hx
  56
  57/-- **THEOREM IC-005.3**: J-cost equals the squared-deviation formula.
  58    J(x) = (x-1)²/(2x) — this form makes the convexity explicit. -/
  59theorem jcost_squared_form (x : ℝ) (hx : x > 0) :
  60    Jcost x = (x - 1)^2 / (2 * x) :=
  61  Cost.Jcost_eq_sq hx.ne'
  62
  63/-- **THEOREM IC-005.4**: J-cost is strictly positive away from x = 1.
  64    The "violation" from the ground state is proportional to (x-1)²/(2x) > 0. -/
  65theorem jcost_pos_away_from_one (x : ℝ) (hx : x > 0) (hne : x ≠ 1) :
  66    Jcost x > 0 := by
  67  rw [jcost_squared_form x hx]
  68  apply div_pos
  69  · have : x - 1 ≠ 0 := sub_ne_zero.mpr hne
  70    positivity
  71  · positivity
  72
  73/-- **THEOREM IC-005.5**: J-cost is symmetric: J(x) = J(1/x).
  74    This means the RS cost landscape has a reflection symmetry,
  75    ensuring the optimization problem is well-conditioned. -/
  76theorem jcost_symmetric (x : ℝ) (hx : x > 0) :
  77    Jcost x = Jcost x⁻¹ :=
  78  Cost.Jcost_symm hx
  79
  80/-! ## II. Gradient of J-Cost (Computability of First-Order Optimization) -/
  81
  82/-- The derivative of J-cost: J'(x) = (1 - 1/x²)/2 = (x² - 1)/(2x²). -/