`cooperatorThreshold_lt_one`

proved

show as: view math explainer →

module: IndisputableMonolith.GameTheory.ESSFromSigma
domain: GameTheory
line: 44 · 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 44.

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

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

papers checked against this theorem

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