jointSigma
plain-language theorem explainer
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.
Claim. Let σ 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
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/φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.