health_eq
plain-language theorem explainer
The declaration establishes health equilibrium by the vanishing of J-cost at argument one. Researchers unifying equilibria across game theory, economics, and biology in the Recognition Science framework cite it to demonstrate shared algebraic conditions. The proof is a direct term application of the Jcost unit lemma that simplifies the cost definition to zero.
Claim. The health equilibrium condition holds: $J(1) = 0$, where $J(x) = (x-1)^2 / (2x)$.
background
In the J-Equilibrium Universality module the health equilibrium is defined as the proposition that J-cost at 1 equals zero. The J-cost function is supplied by the Cost module as $J(x) = (x-1)^2 / (2x)$, which vanishes exactly at unity. The module's local setting is that this identical condition serves as equilibrium for Nash games, efficient markets, and biological homeostasis, so that the Hessian at r=1 is shared across fields. Upstream, the Jcost_unit0 lemma proves the equality by direct simplification of the cost definition.
proof idea
The proof is a one-line term wrapper that applies the Jcost_unit0 lemma from the Cost module. That lemma itself uses simp on the Jcost definition to obtain zero at unity.
why it matters
This theorem supplies the health instance inside the jEquilibriumUniversalityCert structure that bundles the three equilibria and certifies their definitional identity together with shared perturbation sensitivity. It realizes the module claim that Nash, market, and health propositions all reduce to the same Jcost 1 = 0 line, enabling cross-domain transfer of results. The result aligns with the Recognition Science core where J-cost zero marks the equilibrium fixed point on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.