jointSigma
jointSigma assigns the σ-Noether charge to each two-player outcome: +1 for mutual cooperation, 0 for mixed choices, and -1 for mutual defection. Game theorists in the Recognition Science setting cite it to separate σ-conserving moves from the unique violator in the 2x2 normal form. The definition proceeds by exhaustive case analysis on the four possible choice pairs.
claimLet σ map each joint outcome (a pair of choices, each cooperate or defect) to a real number via σ(CC) = 1, σ(CD) = σ(DC) = 0, σ(DD) = -1.
background
The CooperationFromSigma module treats game-theoretic equilibria as J-cost minima on the multi-agent ledger. JointOutcome is the structure that pairs one choice for each of two players. The upstream defect functional equals J for positive arguments and supplies the base cost measure used throughout the ledger.
proof idea
The definition is given directly by pattern matching on the two choices: mutual cooperation returns 1, each mixed pair returns 0, and mutual defection returns -1. No lemmas are invoked; the body is a pure case split.
why it matters in Recognition Science
This definition supplies the concrete σ values required by GameTheoryCert and game_theory_one_statement, which together certify element 84. It realizes the module claim that cooperation follows from σ-conservation, with defect-defect as the sole non-conservative outcome, and feeds the coordination dividend of 1/φ.
scope and limits
- Does not compute J-cost for individual strategies.
- Does not prove σ-conservation for any sequence of moves.
- Does not extend the charge to n-player coalitions.
- Does not reference the phi-ladder or mass formulas.
formal statement (Lean)
76def jointSigma (o : JointOutcome) : ℝ :=
proof body
Definition body.
77 match o.p1, o.p2 with
78 | .cooperate, .cooperate => 1
79 | .cooperate, .defect => 0
80 | .defect, .cooperate => 0
81 | .defect, .defect => -1
82
83/-- The mutual-cooperation outcome has positive σ. -/