CD_sigma_zero

formal source

  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 :=
 107  jointSigma o ≥ 0
 108
 109/-- Mutual defection is not σ-conservative. -/
 110theorem DD_not_sigma_conservative :
 111    ¬ isSigmaConservative ⟨.defect, .defect⟩ := by
 112  unfold isSigmaConservative
 113  rw [DD_sigma_neg]
 114  push_neg
 115  norm_num
 116
 117/-- All other outcomes are σ-conservative. -/
 118theorem nonDD_sigma_conservative (o : JointOutcome)
 119    (h : ¬ (o.p1 = .defect ∧ o.p2 = .defect)) :
 120    isSigmaConservative o := by
 121  rcases o with ⟨p1, p2⟩
 122  cases p1 <;> cases p2