off_equilibrium_game_cost
plain-language theorem explainer
Off equilibrium game cost asserts that the J-cost function is strictly positive for every positive real ratio not equal to one. Researchers extending Recognition Science to game theory and other non-equilibrium domains cite this result. The proof is a one-line term that applies the core Jcost positivity lemma to the supplied hypotheses.
Claim. In off-equilibrium game theory the J-cost is positive away from the fixed point: for all real numbers $r$, if $0 < r$ and $r ≠ 1$ then $0 < Jcost(r)$.
background
This declaration sits in the CrossDomain.JPositivityUniversality module, which develops C16: J-Cost Positivity Universality. The module shows that a single lemma supplies non-equilibrium cost in every domain where J-cost applies, as the off-equilibrium analogue of C7. OffEquilibriumGameCost is defined as the universal quantification over positive reals r not equal to 1 of the strict positivity of Jcost r.
proof idea
The proof is a term-mode one-liner: it constructs the witness function by forwarding the parameters r, hr and hne straight to the lemma Jcost_pos_of_ne_one from the Cost module. No further rewriting or case analysis occurs at this level.
why it matters
The result populates the off_game slot inside jPositivityUniversalityCert, which assembles the full cross-domain certificate. It completes the C16 structural claim by labeling the game-theoretic instance of the universal positivity statement. Within the Recognition Science framework this supports the J-uniqueness property and the Recognition Composition Law by guaranteeing positive cost for any deviation from the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.