HealthEquilibrium
plain-language theorem explainer
HealthEquilibrium defines the health equilibrium condition as the vanishing of the J-cost at unit scale. Researchers unifying equilibria across game theory, economics, and biology under Recognition Science cite this definition to establish domain-independent sensitivity. The declaration is a direct one-line abbreviation that sets the proposition equal to Jcost 1 = 0.
Claim. The health equilibrium condition is the statement that the J-cost function satisfies $J(1) = 0$.
background
The CrossDomain.JEquilibriumUniversality module shows that the single condition Jcost 1 = 0 serves as the equilibrium definition in three domains: Nash equilibrium from game theory, market equilibrium from efficient-market models, and health equilibrium from homeostasis. Jcost is the recognition cost function imported from the Cost module; the module documentation states that all three domains reduce to the same line via Jcost_unit0, so that the Hessian of J at r = 1 is shared. This local setting follows the Recognition Science forcing chain in which J-cost governs universal equilibrium behavior.
proof idea
The declaration is a one-line definition that directly sets HealthEquilibrium to the proposition Jcost 1 = 0.
why it matters
This definition supplies the health component inside the JEquilibriumUniversalityCert structure and is used by the theorems health_eq, market_eq_health, and all_three_equal. The parent result all_three_equal states that NashEquilibrium = MarketEquilibrium ∧ MarketEquilibrium = HealthEquilibrium, confirming that a perturbation of J yields the same multiplier in every domain. It realizes the module claim of J-equilibrium universality and aligns with the Recognition Science landmarks that J(x) = (x + x^{-1})/2 - 1 forces the same equilibrium condition across fields.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.