IndisputableMonolith.GameTheory.ESSFromSigma

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Evolutionarily Stable Strategies from σ-Conservation
   6
   7## §XXIII.C row "Game theory from first principles" — ESS side.
   8
   9An evolutionarily stable strategy (ESS) is a strategy that, once
  10adopted by the majority, cannot be invaded by a rare mutant.  In
  11RS, ESS exists iff the cooperator fraction is at least `1/φ` in a
  12kin-selected population.
  13
  14This is Hamilton's rule reframed: the Hamilton coefficient
  15`r > c/b` becomes `cooperator_fraction ≥ 1/φ`, where `c/b` is the
  16cost-benefit ratio in the canonical RS-native units.
  17
  18## What this module provides
  19
  201. `cooperatorThreshold`: `1/φ`.
  212. `isESS`: `cooperator_fraction ≥ 1/φ`.
  223. `cooperatorThreshold_lt_one`: `1/φ < 1`.
  234. `cooperatorThreshold_pos`: `1/φ > 0`.
  245. Master cert `ESSFromSigmaCert` with 4 fields.
  25-/
  26
  27namespace IndisputableMonolith
  28namespace GameTheory
  29namespace ESSFromSigma
  30
  31open Constants
  32
  33noncomputable section
  34
  35/-- The cooperator-fraction threshold for ESS in a kin-selected
  36    population: `1/φ ≈ 0.618`. -/
  37def cooperatorThreshold : ℝ := 1 / phi
  38
  39/-- ESS predicate: cooperator fraction is at or above the threshold. -/
  40def isESS (cooperator_fraction : ℝ) : Prop :=
  41  cooperatorThreshold ≤ cooperator_fraction
  42
  43/-- The threshold is strictly less than 1. -/
  44theorem cooperatorThreshold_lt_one : cooperatorThreshold < 1 := by
  45  unfold cooperatorThreshold
  46  have : 1 < phi := by have := phi_gt_onePointFive; linarith
  47  rw [div_lt_one phi_pos]
  48  exact this
  49
  50/-- The threshold is strictly positive. -/
  51theorem cooperatorThreshold_pos : 0 < cooperatorThreshold := by
  52  unfold cooperatorThreshold
  53  exact div_pos one_pos phi_pos
  54
  55/-- All-cooperator strategy is an ESS. -/
  56theorem all_cooperator_isESS : isESS 1 :=
  57  le_of_lt cooperatorThreshold_lt_one
  58
  59/-- Empty-cooperator strategy is not an ESS. -/
  60theorem no_cooperator_not_isESS : ¬ isESS 0 := by
  61  unfold isESS
  62  push_neg
  63  exact cooperatorThreshold_pos
  64
  65/-! ## Master certificate -/
  66
  67/-- **ESS FROM SIGMA MASTER CERTIFICATE.** -/
  68structure ESSFromSigmaCert where
  69  threshold_pos : 0 < cooperatorThreshold
  70  threshold_lt_one : cooperatorThreshold < 1
  71  all_coop_isESS : isESS 1
  72  no_coop_not_isESS : ¬ isESS 0
  73
  74/-- The master certificate is inhabited. -/
  75def essFromSigmaCert : ESSFromSigmaCert where
  76  threshold_pos := cooperatorThreshold_pos
  77  threshold_lt_one := cooperatorThreshold_lt_one
  78  all_coop_isESS := all_cooperator_isESS
  79  no_coop_not_isESS := no_cooperator_not_isESS
  80
  81end
  82
  83end ESSFromSigma
  84end GameTheory
  85end IndisputableMonolith
  86