EquilibriumDomain
EquilibriumDomain enumerates the three application settings (game theory, financial markets, health states) that share an identical J-cost Hessian in Recognition Science. Cross-domain equilibrium researchers cite this enumeration to ground the claim that Nash, market, and health equilibria obey the same quadratic response at r=1. The declaration is a direct inductive type with automatic Fintype derivation, enabling immediate cardinality and universal quantification in sibling theorems.
claimLet $D$ be the inductive type whose constructors are gameTheory, financialMarket, and healthState, representing the domains of game-theoretic equilibria, financial-market equilibria, and health-state equilibria. The type is equipped with decidable equality and has finite cardinality 3.
background
Module C7 establishes the universal equilibrium response under the shared local J-cost kernel imported from JCostHessianC7. In Recognition Science the J-cost function supplies the quadratic kernel whose Hessian coefficient is fixed at 1, yielding identical response coefficients of 1/2 across any modeled equilibrium. The three constructors supply the concrete domains in which this kernel is asserted to operate uniformly.
proof idea
The declaration is an inductive type definition with three constructors and a deriving clause that generates DecidableEq, Repr, and Fintype instances. No separate proof body exists; the Fintype instance is produced automatically to support the downstream cardinality theorem equilibriumDomain_count.
why it matters in Recognition Science
This definition supplies the domain set for responseCoefficient, responseCoefficient_universal, and the UniversalResponseCert structure. It realizes the module claim that any RS equilibrium inherits the same Hessian coefficient 1, providing the formal core for equating Nash, market, and health equilibria at r=1. The construction closes the scaffolding for cross-field comparisons while leaving empirical sensitivity data outside the formal scope.
scope and limits
- Does not prove empirical equivalence of response sensitivities across domains.
- Does not derive the J-cost Hessian coefficient value.
- Does not address scaling parameter r outside the r=1 case.
- Does not enumerate domains beyond the three listed constructors.
formal statement (Lean)
23inductive EquilibriumDomain where
24 | gameTheory
25 | financialMarket
26 | healthState
27 deriving DecidableEq, Repr, Fintype
28