jcost_pos_away_from_one

formal source

  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
  90/-- **THEOREM IC-005.7**: J'(x) > 0 for x > 1.
  91    The gradient points upward away from the minimum for x > 1. -/
  92theorem jcost_deriv_pos_of_gt_one (x : ℝ) (hx : x > 1) :
  93    jcost_deriv x > 0 := by
  94  unfold jcost_deriv
  95  apply div_pos _ (by norm_num)