GameTheoryCert
plain-language theorem explainer
The GameTheoryCert structure packages the σ-conservation rules for the prisoner's dilemma in Recognition Science, fixing joint σ = +1 on mutual cooperation, σ = -1 on mutual defection, conservation on all non-DD outcomes, the cooperation dividend in (0.617, 0.622), and strict coalition payoff superiority. Game theorists working inside the RS ledger would cite it to ground positive-sum equilibria. The declaration is a structure definition that assembles seven fields directly from sibling lemmas.
Claim. A game-theory certificate consists of: joint σ-charge = +1 on the mutual-cooperation outcome, = −1 on the mutual-defection outcome; mutual defection violates σ-conservation; every joint outcome that is not mutual defection conserves σ; the cooperation dividend lies in (0.617, 0.622) and satisfies 0 < dividend < 1; for every natural number n and every π_def > 0 the coalition payoff strictly exceeds n · π_def.
background
In this module a JointOutcome is a pair of choices (cooperate or defect) for two players. The jointSigma map assigns the σ-Noether charge of the move: +1 when both cooperate (creating coordinated value), −1 when both defect (destroying it), and 0 on mixed pairs. The cooperationDividend is defined as 1/φ, where φ is the self-similar fixed point forced by the T5–T6 steps of the unified forcing chain. The isSigmaConservative predicate holds precisely when the joint σ-charge is preserved under the move. Upstream, the defect functional equals the J-cost for positive arguments, and the Economics.GameTheoryFromRS.GameTheoryCert requires five game types together with Jcost(1) = 0 and positive Jcost off unity.
proof idea
The declaration is a structure definition whose seven fields are filled by direct reference to sibling results: CC_sigma_pos supplies the +1 value, DD_sigma_neg the −1 value, DD_not_sigma_conservative the violation, nonDD_sigma_conservative the universal conservation statement, cooperationDividend_band the numerical interval, and the coalitionPayoff definition the strict inequality.
why it matters
This supplies the master certificate (element 84) instantiated by the local gameTheoryCert definition and consumed by the GameTheoryCert structure in Economics.GameTheoryFromRS. It realizes the module claim that cooperation arises exactly when σ is conserved and that the coordination dividend equals 1/φ, thereby linking the two-player ledger to the J-uniqueness and eight-tick octave of the foundational forcing chain. The declaration closes the game-theoretic fragment by confirming the strict coalition advantage over n-fold defection.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.