jcost_squared_form
plain-language theorem explainer
J-cost on positive reals equals the squared deviation (x-1)^2/(2x). Recognition Science researchers cite this to exhibit the explicit quadratic convexity of the cost landscape near equilibrium. The proof is a one-line term application of the core Jcost_eq_sq lemma after weakening x > 0 to x ≠ 0.
Claim. For every positive real $x$, the J-cost satisfies $J(x) = (x-1)^2 / (2x)$.
background
The module IC-005 derives the computational complexity of physics from the structure of J-cost minimization in Recognition Science. J-cost is defined by J(x) = ((x + x^{-1})/2) - 1 for x > 0 and measures deviation from the ground state at x = 1. The upstream lemma Jcost_eq_sq states that J(x) = (x-1)^2/(2x) for x ≠ 0, obtained by unfolding the definition followed by field_simp and ring simplification.
proof idea
The proof is a one-line term wrapper that invokes Cost.Jcost_eq_sq after converting the hypothesis x > 0 into x ≠ 0 via ne'.
why it matters
This is IC-005.3 and supplies the squared form used in jConvexityUniversalityCert and the complexity summary ic005_certificate. It makes the quadratic deviation from x = 1 explicit, supporting T5 J-uniqueness and convex minimization in the forcing chain. The identity underpins the claim that ground-state verification is linear while φ-rung computations remain exponentially costly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.