HealthEquilibrium
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove that Jcost 1 equals zero; that equality is supplied by the lemma Jcost_unit0.
- Does not derive or restrict the explicit functional form of Jcost.
- Does not analyze stability, dynamics, or higher-order derivatives around the equilibrium.
Lean usage
theorem health_eq : HealthEquilibrium := Jcost_unit0formal statement (Lean)
34def HealthEquilibrium : Prop := Jcost 1 = 0
proof body
Definition body.
35