jEquilibriumUniversalityCert
plain-language theorem explainer
The definition assembles a single record certifying that Nash equilibrium, market equilibrium, and health equilibrium each reduce to the same J-cost vanishing condition at unit scale. Cross-domain researchers applying the Recognition framework would cite this certificate to transfer perturbation results between game theory, economics, and homeostasis models. The construction is a direct record literal that populates each field from the corresponding upstream theorem.
Claim. A certificate whose fields are the Nash equilibrium proposition, the market equilibrium proposition, the health equilibrium proposition, the statement that these three propositions coincide, and the assertion that the J-cost function is strictly positive for all positive arguments not equal to one.
background
The module C7 establishes J-Equilibrium Universality. It shows that the same condition Jcost 1 = 0 serves as the equilibrium condition in Nash game theory, efficient market hypothesis, and biological homeostasis. The upstream theorems nash_eq, market_eq, health_eq each set their respective equilibrium to Jcost_unit0, while all_three_equal proves the three are identical by reflexivity, and shared_sensitivity shows the positivity of Jcost away from 1 using Jcost_pos_of_ne_one.
proof idea
This definition is a direct record construction that assigns the nash field to nash_eq, the market field to market_eq, the health field to health_eq, the three_are_one field to all_three_equal, and the shared_pert field to shared_sensitivity.
why it matters
This definition supplies the concrete witness for the C7 structural claim that a single J-cost condition unifies equilibria across game theory, economics, and biology. It draws on the Recognition framework's core J-cost and the shared sensitivity at equilibrium. Since no downstream theorems depend on it yet, it leaves open the task of applying the shared perturbation multiplier in specific cross-domain models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.