65theorem jcost_pos_away_from_one (x : ℝ) (hx : x > 0) (hne : x ≠ 1) : 66 Jcost x > 0 := by
proof body
Term-mode proof.
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. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.