deviation_increases_cost
plain-language theorem explainer
Any unilateral deviation from the social norm ratio r=1 strictly increases an agent's J-cost in the Recognition Science decision model. Game theorists and decision theorists working in RS would cite this to establish that the zero-cost joint state is the unique Nash equilibrium. The proof is a direct one-line application of the positivity lemma for the J-cost function.
Claim. For every positive real number $r$ with $r ≠ 1$, the recognition cost satisfies $0 < J(r)$, where $J(r)$ denotes the J-cost of the action-to-norm ratio $r$.
background
In the Nash Equilibrium from J-Cost Minimisation module, every agent minimises its recognition cost J(r) where r is the ratio of its action to the social norm. The module states that Nash equilibrium equals the joint J-cost minimum, with all agents at r=1 where recognition cost is zero. The upstream lemma Jcost_pos_of_ne_one from the Cost module establishes J(x) > 0 for x > 0 and x ≠ 1 by rewriting Jcost via Jcost_eq_sq and applying positivity of squares and division.
proof idea
This is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one from IndisputableMonolith.Cost, passing the hypotheses hr : 0 < r and hne : r ≠ 1 directly to obtain 0 < Jcost r.
why it matters
This theorem supplies the deviation_costly field inside the nashEquilibriumCert definition, which certifies Nash stability in the RS decision framework. It fills the structural claim that any unilateral deviation from the zero-cost joint state increases cost, thereby proving recognitive stability of the Nash equilibrium. It connects to the Recognition Science result that J vanishes only at r=1 and supports the one-paragraph proof that Nash equilibria in symmetric games are recognitively stable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.