jcost_quadratic_identity
plain-language theorem explainer
The theorem states that for real δ with 1 + δ > 0 the J-cost satisfies J(1 + δ) ⋅ 2(1 + δ) = δ². Equilibrium analysts in Recognition Science cite it to extract the universal sensitivity coefficient 1/2 from the local quadratic form. The proof is a one-line wrapper that substitutes the explicit quadratic-leading-order expression and clears denominators by field simplification.
Claim. For real δ with 1 + δ > 0, the J-cost function obeys J(1 + δ) ⋅ 2(1 + δ) = δ².
background
The J-cost is the function J(r) = (r − 1)² / (2r) for r > 0, convex with minimum value zero at r = 1. The module derives the local quadratic behavior near equilibrium that fixes the universal sensitivity constant 1/2 for small deviations in all RS models. The upstream theorem jcost_at_one_plus_delta supplies the explicit form J(1 + δ) = δ² / (2(1 + δ)), which is the direct algebraic input.
proof idea
Substitute the expression from jcost_at_one_plus_delta and apply field_simp to cancel the common factor 2(1 + δ) and obtain the identity.
why it matters
The identity is collected inside the JConvexityUniversalityCert definition that bundles the core convexity properties. It supplies the local Hessian computation required by the C25 claim, confirming the leading-order sensitivity 1/2 that propagates through RS equilibria. The result closes the local expansion step that underlies the phi-ladder mass formulas without leaving an open scaffolding gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.