jcost_squared_form

formal source

  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²). -/
  83noncomputable def jcost_deriv (x : ℝ) : ℝ := (1 - (x⁻¹)^2) / 2
  84
  85/-- **THEOREM IC-005.6**: J'(1) = 0 — the gradient vanishes at the ground state.
  86    This confirms x = 1 is the unique critical point (and global minimum). -/
  87theorem jcost_deriv_zero_at_one : jcost_deriv 1 = 0 := by
  88  unfold jcost_deriv; simp
  89