off_equilibrium
plain-language theorem explainer
Off-equilibrium deviation asserts that the J-cost is strictly positive for any positive ratio r not equal to one. Game theorists applying Recognition Science would cite this to confirm that unilateral deviations from Nash equilibrium incur positive recognition cost. The proof is a direct one-line application of the upstream positivity lemma for the J-cost function.
Claim. For every real number $r$ with $0 < r$ and $r ≠ 1$, the J-cost satisfies $0 < Jcost(r)$.
background
The module identifies Nash equilibrium with zero J-cost and treats any unilateral deviation as off-equilibrium with positive J-cost. This supplies the RS derivation of Nash's theorem, with five canonical game types corresponding to configDim D = 5. Jcost is the recognition cost function whose minimum is zero precisely at ratio one.
proof idea
One-line wrapper that applies the lemma Jcost_pos_of_ne_one from the Cost module (and its duplicates in JcostCore and LocalCache).
why it matters
This result supplies the off-equilibrium half of the Nash characterization inside GameTheoryCert, which packages five_types, nash_eq, and off_eq into a single certificate. It directly supports the module claim that RS recovers Nash's theorem from the J-cost minimizer. The parent GameTheoryCert definition consumes this theorem to close the economic application of the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.