jcost_at_one_plus_delta
plain-language theorem explainer
Researchers studying local expansions of J-cost near its minimum in Recognition Science equilibria cite this result for the explicit quadratic leading order. It states that J(1 + δ) equals δ² over 2(1 + δ) for real δ with 1 + δ positive. The proof is a one-line wrapper that substitutes the global squared-form identity for J-cost and normalizes the resulting algebraic expression via congruence and ring tactics.
Claim. For real δ with 1 + δ > 0, the J-cost satisfies $J(1 + δ) = δ^2 / (2(1 + δ))$.
background
The J-cost function satisfies the identity J(r) = (r - 1)^2 / (2 r) for r > 0, as given by the squared-form theorem. This module develops convexity of J-cost on (0, ∞) with global minimum zero at r = 1; the local quadratic behavior near r = 1 fixes the universal sensitivity coefficient 1/2 for small deviations in RS equilibria. Upstream results include the squared-form identity from JCostGeometry, which supplies the explicit expression J(r) = (r - 1)^2 / (2 r) used directly here.
proof idea
The proof is a one-line wrapper that invokes the squared-form identity at the point 1 + δ (valid under the positivity hypothesis) and then applies congruence followed by the ring tactic to match the target δ² / (2(1 + δ)).
why it matters
This result supplies the explicit local expansion required by the quadratic-identity theorem and the symmetric-pair theorem in the same module. It realizes the leading-order coefficient stated in the C25 module documentation, confirming the universal sensitivity of 1/2. The identity connects to the forcing chain through the J-uniqueness property that underlies the squared form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.