deviation_increases_cost
plain-language theorem explainer
Any unilateral deviation from the recognition ratio r=1 strictly raises an agent's J-cost. Game theorists working in recognition-science models cite this to establish stability of the joint homeostasis state. The proof is a one-line wrapper invoking the positivity lemma for Jcost away from unity.
Claim. For every real $r$ with $0 < r$ and $r ≠ 1$, the recognition cost satisfies $0 < J(r)$.
background
The module treats agents that minimise recognition cost J(r), where r is the ratio of an agent's action to the prevailing social norm. Nash equilibrium is identified with the joint J-cost minimum attained when every agent sits at r=1. The upstream lemma Jcost_pos_of_ne_one states that J(x) > 0 for x ≠ 1 and x > 0; its proof rewrites Jcost via the squared identity Jcost_eq_sq and invokes positivity of the resulting square term.
proof idea
One-line wrapper that applies Jcost_pos_of_ne_one r hr hne.
why it matters
Supplies the deviation_costly component of nashEquilibriumCert, which certifies that the zero-cost homeostasis state is a Nash equilibrium. It realises the module claim that Nash equilibrium equals joint J-cost minimum and that unilateral deviation from r=1 is strictly costly. The result therefore closes the recognition-science argument that the unique zero-cost joint state is stable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.