joint_homeostasis_zero_cost
plain-language theorem explainer
The declaration establishes that J-cost vanishes exactly when every agent operates at the recognition ratio of unity. Game theorists using recognition-cost models for symmetric games would cite this as the base case anchoring Nash stability. The argument is a direct one-line reduction to the unit lemma for the J-cost function.
Claim. At the joint homeostasis state where every agent's action ratio equals one, the J-cost is zero: $J(1)=0$.
background
In the Nash Equilibrium from J-Cost Minimisation module, each agent minimises its recognition cost J(r) with r the ratio of its action to the social norm. The cost function is given explicitly by J(x)=(x-1)^2/(2x) for x>0, which is nonnegative everywhere and zero only at x=1. Upstream lemmas establish that the cost of any recognition event equals its J-cost and that a multiplicative recognizer induces this cost on positive ratios.
proof idea
The proof is a one-line wrapper that applies the Jcost_unit0 lemma from the Cost module, which evaluates Jcost 1 directly by simplification of the defining expression.
why it matters
This supplies the homeostasis_optimal field inside the nashEquilibriumCert definition, which certifies that the zero-cost joint state is the Nash equilibrium. It realises the module's structural claim that Nash equilibria in symmetric games coincide with the unique recognitive minimum. The result aligns with the J-uniqueness property in the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.