responseCoefficient
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove the coefficient equals 1.
- Does not compare empirical sensitivities across domains.
- Does not derive the quadratic coefficient 1/2.
- Does not address non-equilibrium cases.
Lean usage
theorem responseCoefficient_universal (D : EquilibriumDomain) : responseCoefficient D = 1 := by unfold responseCoefficient; exact jcostHessianCoefficient_eq_oneformal statement (Lean)
32noncomputable def responseCoefficient (_ : EquilibriumDomain) : ℝ :=
proof body
Definition body.
33 jcostHessianCoefficient
34