equilibriumDomain_count
EquilibriumDomain is shown to contain exactly three elements by enumerating its inductive constructors for game theory, financial markets, and health states. Researchers modeling unified equilibria across these fields in Recognition Science reference this count to anchor the universal response certification. The proof reduces to a single decide tactic on the derived Fintype instance.
claimThe finite type of equilibrium domains has cardinality three, where the domains are game theory, financial markets, and health states: $3 = |$game theory$, $financial market$, $health state$|$
background
The C7 module establishes that any recognition science equilibrium shares the same local J-cost kernel, yielding a quadratic coefficient of 1/2 and Hessian coefficient of 1. This common core underpins the identification of Nash equilibria with market and health equilibria at unit scaling. EquilibriumDomain is the inductive type with three constructors gameTheory, financialMarket, healthState, each equipped with decidable equality and finite type structure.
proof idea
A one-line wrapper applies the decide tactic, which evaluates the cardinality computation using the Fintype instance automatically derived from the inductive definition of EquilibriumDomain.
why it matters in Recognition Science
The result populates the three_domains field in universalResponseCert, which assembles the full certification including the universal response coefficient and the J-cost Hessian certificate. It directly supports the module's formalization of the shared J-kernel across domains, consistent with the Recognition Science forcing chain and J-uniqueness. The enumeration closes the finite model for the three-domain equilibrium response.
scope and limits
- Does not prove that the J-cost kernel is identical across the three domains.
- Does not derive the quadratic coefficient 1/2 or Hessian coefficient 1.
- Does not extend the model to more than three equilibrium domains.
- Does not compare empirical sensitivities between the domains.
Lean usage
noncomputable def universalResponseCert : UniversalResponseCert where three_domains := equilibriumDomain_count universal_response := responseCoefficient_universal kernel := jcostHessianCertformal statement (Lean)
29theorem equilibriumDomain_count : Fintype.card EquilibriumDomain = 3 := by
proof body
Decided by rfl or decide.
30 decide
31