jcostHessianCoefficient_eq_one
plain-language theorem explainer
The declaration proves that the Hessian coefficient of the J-cost at equilibrium equals one. Equilibrium response calculations cite this to normalize the quadratic term in the local cost expansion. The proof is a direct algebraic reduction that unfolds the coefficient definitions and applies numerical simplification.
Claim. The Hessian coefficient of the J-cost function at equilibrium, defined as twice the leading quadratic Taylor coefficient of $J(1 + eps)$, equals 1.
background
In the C7 module on local J-cost expansion at equilibrium, the J-cost satisfies the exact algebraic kernel $J(1 + eps) = eps^2 / (2(1 + eps))$. The Taylor quadratic coefficient is defined as 1/2, capturing the leading eps^2/2 term. The Hessian coefficient is then twice this quadratic coefficient per the standard Taylor convention for the second-derivative term.
proof idea
The proof is a one-line wrapper that unfolds the definitions of jcostHessianCoefficient and jcostTaylorQuadraticCoefficient, then applies norm_num to verify the equality.
why it matters
This normalizes the response coefficient to 1 in the universal equilibrium response theorem, which applies the equality after unfolding responseCoefficient. It also supplies the hessian_one field in the JCostHessianCert structure. The result supports the local quadratic kernel used in equilibrium calculations, consistent with the J-uniqueness fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.