jointSigma

formal source

  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. -/
  92theorem CD_sigma_zero :
  93    jointSigma ⟨.cooperate, .defect⟩ = 0 := rfl
  94
  95theorem DC_sigma_zero :
  96    jointSigma ⟨.defect, .cooperate⟩ = 0 := rfl
  97
  98/-! ## §2. σ-conservation predicate
  99
 100A joint outcome is σ-conservative iff its σ ≥ 0; it preserves or
 101creates coordinated value.  Mutual defection is the unique
 102σ-violator in the four-outcome space.
 103-/
 104
 105/-- σ-conservative outcomes: mutual cooperation or mixed. -/
 106def isSigmaConservative (o : JointOutcome) : Prop :=