jcostHessianCert
plain-language theorem explainer
The definition assembles the JCostHessianCert structure that certifies the exact quadratic kernel for J-cost near equilibrium. Equilibrium response calculations in the C7 framework cite it to obtain the unit Hessian without derivative operators. The construction is a direct field assignment that bundles the local kernel identity with the two coefficient equalities.
Claim. The structure holds when the local kernel satisfies $Jcost(1 + eps) · 2(1 + eps) = eps^2$ for all real $eps ≠ -1$, the Taylor quadratic coefficient equals $1/2$, and the Hessian coefficient equals 1.
background
Module C7 derives the exact local algebraic expansion of the J-cost function at the equilibrium point r = 1. The identity Jcost(1 + eps) = eps² / (2(1 + eps)) for eps ≠ -1 supplies the quadratic numerator directly and is stronger than a second-order Taylor claim away from eps = -1. The module records the formal Taylor coefficient 1/2 so that the Hessian coefficient is 1 in the usual normalization.
proof idea
The definition populates the three fields of the JCostHessianCert structure. It assigns the local_kernel field to the theorem jcost_local_quadratic_kernel, the coefficient_half field to jcostTaylorQuadraticCoefficient_eq, and the hessian_one field to jcostHessianCoefficient_eq_one.
why it matters
It supplies the kernel field required by the universalResponseCert definition in Applied.UniversalEquilibriumResponseC7. This completes the C7 plan for the exact local J-cost expansion at r = 1 and the unit Hessian in standard normalization, enabling the universal response coefficient while avoiding Mathlib derivative APIs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.