Choice

formal source

  58-/
  59
  60/-- Player choice: cooperate or defect. -/
  61inductive Choice where
  62  | cooperate
  63  | defect
  64  deriving DecidableEq, Inhabited
  65
  66/-- A 2-player joint outcome. -/
  67structure JointOutcome where
  68  p1 : Choice
  69  p2 : Choice
  70  deriving DecidableEq
  71
  72/-- The σ-charge of a joint outcome: `+1` for mutual cooperation
  73    (creating coordinated value), `0` for mixed, `-1` for mutual
  74    defection (destroying coordinated value).  This is the σ-Noether
  75    charge of the multi-agent move. -/
  76def jointSigma (o : JointOutcome) : ℝ :=
  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 σ. -/
  84theorem CC_sigma_pos :
  85    jointSigma ⟨.cooperate, .cooperate⟩ = 1 := rfl
  86
  87/-- The mutual-defection outcome has negative σ. -/
  88theorem DD_sigma_neg :
  89    jointSigma ⟨.defect, .defect⟩ = -1 := rfl
  90
  91/-- Mixed outcomes have σ = 0. -/