jcost_squared_form
plain-language theorem explainer
For every positive real r the J-cost equals (r-1)^2 over 2r. Cross-domain convexity certificates and RS complexity-structure theorems cite this identity to expose the quadratic leading-order term near equilibrium. The proof is a one-line term that applies the core squared-form lemma after rewriting the positivity hypothesis.
Claim. For every real number $r > 0$, $J(r) = (r-1)^2 / (2r)$.
background
J-cost is the function J(x) = ((x + x^{-1})/2 - 1) for x > 0. Module C25 states that J-cost is convex on (0, ∞) with a unique minimum at r = 1 where J(1) = 0; the squared identity makes the local quadratic approximation J(r) ≈ (r-1)^2/2 explicit and supplies the universal sensitivity coefficient 1/2. Upstream lemma Jcost_eq_sq in Cost.lean derives the form by unfolding the definition, applying field_simp on the non-zero hypothesis, and closing with ring.
proof idea
One-line term wrapper that invokes Jcost_eq_sq after converting the hypothesis 0 < r into r ≠ 0 via ne_of_gt.
why it matters
Supplies the squared_form field inside the JConvexityUniversalityCert definition that aggregates all C25 properties. Downstream results such as jcost_at_one_plus_delta and the IC-005 certificate in PhysicsComplexityStructure apply the identity directly. The form underpins the leading-order sensitivity constant 1/2 stated in the module documentation and connects to the J-uniqueness step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.