off_equilibrium
Off-equilibrium deviation establishes that recognition cost J(r) exceeds zero for any positive real deviation parameter r not equal to unity. Researchers deriving Nash equilibria from recognition cost minimization would reference this result to confirm that unilateral deviations incur positive cost. The proof consists of a direct invocation of the J-cost positivity lemma under the given positivity and inequality hypotheses.
claimFor any real number $r > 0$ with $r ≠ 1$, the recognition cost satisfies $J(r) > 0$.
background
The module identifies Nash equilibrium with zero J-cost (minimum recognition cost, no beneficial unilateral deviation) and off-equilibrium states with positive J-cost. J-cost is defined via the square formula J(r) = (r-1)^2 divided by a positive denominator when r > 0, as established in the upstream Cost module. The local theoretical setting equates the five canonical game types to configDim D = 5 and treats Nash equilibrium as the J = 0 minimum.
proof idea
One-line wrapper that applies the Jcost_pos_of_ne_one lemma from the Cost module (and its duplicates in JcostCore and LocalCache).
why it matters in Recognition Science
This result supplies the off-equilibrium half of the game theory certification, feeding directly into gameTheoryCert which bundles five_types, nash_eq at J = 0, and off_eq at J > 0. It supports the RS derivation of Nash's theorem from recognition cost minimization, consistent with the framework's identification of equilibria as cost minima. No open questions are touched.
scope and limits
- Does not establish existence of Nash equilibria.
- Does not enumerate or prove the five canonical game types.
- Does not compute explicit numerical values of J(r).
- Does not address repeated games or dynamic extensions.
Lean usage
def gameTheoryCert : GameTheoryCert where five_types := gameTypeCount nash_eq := nash_equilibrium off_eq := off_equilibriumformal statement (Lean)
34theorem off_equilibrium {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
35 0 < Jcost r := Jcost_pos_of_ne_one r hr hne
proof body
36