UniversalResponseCert
plain-language theorem explainer
The UniversalResponseCert structure certifies that the three equilibrium domains share a response coefficient of exactly 1 under the common J-cost Hessian. Cross-domain equilibrium modelers in Recognition Science would cite it to formalize the shared kernel behind Nash-market-health analogies at unit radius. It is realized as a bare structure definition that directly assembles the cardinality fact, the universal response equality, and the imported Hessian certificate.
Claim. Let $E$ be the inductive type whose constructors are game theory, financial markets, and health states. A universal response certificate is a structure asserting that the cardinality of $E$ equals 3, that the response coefficient equals 1 for every element of $E$, and that the J-cost Hessian certificate holds.
background
The module C7 formalizes the claim that any RS equilibrium modeled by the same local J-cost kernel inherits quadratic coefficient 1/2 and Hessian coefficient 1. EquilibriumDomain is the inductive type with three constructors: gameTheory, financialMarket, healthState. The sibling definition responseCoefficient maps every domain to the constant jcostHessianCoefficient. JCostHessianCert requires that the local kernel obeys Jcost(1 + eps) * (2 * (1 + eps)) = eps^2 for eps ≠ -1, together with the Taylor quadratic coefficient 1/2 and Hessian coefficient 1.
proof idea
The declaration is a structure definition with an empty proof body. It packages three fields: the Fintype.card equality on EquilibriumDomain, the universal quantification that responseCoefficient returns 1 on every domain, and an instance of JCostHessianCert.
why it matters
UniversalResponseCert supplies the type for the downstream universalResponseCert definition, which constructs an explicit instance via equilibriumDomain_count, responseCoefficient_universal, and jcostHessianCert. It realizes the C7 common-core claim that every RS equilibrium inherits the same 1/2 quadratic and unit Hessian coefficients, grounding the prose statement that Nash, market, and health equilibria coincide at r = 1. The file does not address empirical cross-field sensitivities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.