`cooperatorThreshold`

definition

show as: view math explainer →

module: IndisputableMonolith.GameTheory.ESSFromSigma
domain: GameTheory
line: 37 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.GameTheory.ESSFromSigma on GitHub at line 37.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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.** -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.