responseCoefficient
plain-language theorem explainer
responseCoefficient supplies the J-cost Hessian coefficient to each equilibrium domain. Cross-domain analysts cite it to ground the shared local kernel behind Nash, market, and health equilibria at r=1. The definition is a direct one-line alias to jcostHessianCoefficient.
Claim. Let $D$ be an equilibrium domain. The response coefficient of $D$ is the Hessian coefficient of the J-cost function, equal to twice the quadratic coefficient in the Taylor expansion of the J-cost.
background
The module formalizes the universal equilibrium response under C7. EquilibriumDomain is the inductive type with three constructors: gameTheory, financialMarket, and healthState. The upstream jcostHessianCoefficient is defined as twice the quadratic Taylor coefficient of the J-cost, following the convention that the Hessian equals twice the quadratic term. This supplies the common core for the claim that any RS equilibrium modeled by the same local J-cost kernel inherits the same quadratic coefficient 1/2 and Hessian coefficient 1.
proof idea
The definition is a one-line alias that returns the value of jcostHessianCoefficient.
why it matters
It is referenced by responseCoefficient_universal, which proves the coefficient equals 1 for every domain, and by UniversalResponseCert, which records the three-domain count together with the universal response property and the J-cost Hessian certificate. This realizes the shared J-kernel at the core of the C7 claim that Nash, market, and health equilibria coincide at r=1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.