OffEquilibriumGameCost
plain-language theorem explainer
The off-equilibrium game cost proposition asserts that the J-cost exceeds zero for every positive real ratio different from one. Game theorists modeling non-equilibrium strategies cite this as the penalty for deviation from the recognition fixed point. It is one of seven domain labels for the identical universal statement, with their equality shown by a single theorem.
Claim. The statement $J(r) > 0$ holds for all $r > 0$ with $r ≠ 1$, where $J$ is the J-cost function.
background
Recognition Science defines the J-cost function to quantify departure from the self-similar fixed point. Module C16 extends the equilibrium result C7 by labeling the same positivity claim across seven domains. The upstream lemma establishing J-cost positivity for ratios not equal to one supplies the inequality in every case.
proof idea
This is a direct definition of the proposition. The associated theorem applies the core positivity lemma to obtain the result for the game domain.
why it matters
The definition enters the certificate structure that collects all seven domain instances and the theorem proving they coincide. It realizes the C16 extension of the equilibrium zero-cost result to off-equilibrium cases. The construction relies on the J-uniqueness property and ensures positive cost away from the fixed point in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.