`cooperatorThreshold_pos`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.GameTheory.ESSFromSigma on GitHub at line 51.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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

papers checked against this theorem

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