module module moderate

`IndisputableMonolith.GameTheory.CooperationFromSigma`

The module defines a game-theoretic model in Recognition Science where binary player choices of cooperate or defect produce joint outcomes labeled by a sigma deviation measure. It establishes that sigma-conservative outcomes produce positive cooperation dividends while defect-defect pairs violate conservation. The structure consists of type definitions for Choice and JointOutcome, direct sigma assignments for each pair, and lemmas verifying signs and conservation properties.

claimLet $C$ denote cooperate and $D$ denote defect. For joint outcomes, define the sigma map such that $sigma(C,C)>0$, $sigma(D,D)<0$, and $sigma(C,D)=sigma(D,C)=0$. A joint outcome is sigma-conservative when total sigma is preserved, which yields a positive cooperation dividend.

background

The module imports the RS time quantum tau_0 = 1 tick from Constants and cost primitives from the Cost module. It introduces Choice as the binary enumeration of cooperate or defect. JointOutcome pairs these choices, and jointSigma assigns a real-valued deviation to each pair. The setting models interactions in which sigma encodes departure from cost conservation or the Recognition Composition Law.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module supplies the game-theoretic primitives that connect sigma conservation to cooperation within the Recognition Science framework. It aligns with the forcing chain by showing how positive sigma in mutual cooperation respects the phi-ladder structure while defect-defect outcomes break conservation. No downstream theorems are recorded in the current dependency graph.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (20)

inductive Choice L61
structure JointOutcome L67
def jointSigma L76
theorem CC_sigma_pos L84
theorem DD_sigma_neg L88
theorem CD_sigma_zero L92
theorem DC_sigma_zero L95
def isSigmaConservative L106
theorem DD_not_sigma_conservative L110
theorem nonDD_sigma_conservative L118
theorem sigma_conservative_iff L138
def cooperationDividend L158
theorem cooperationDividend_band L161
theorem cooperationDividend_pos L171
theorem cooperationDividend_lt_one L177
def coalitionPayoff L190
theorem coalition_strictly_better L194
structure GameTheoryCert L212
def gameTheoryCert L227
theorem game_theory_one_statement L247