pith. machine review for the scientific record. sign in
theorem

no_cooperator_not_isESS

proved
show as:
view math explainer →
module
IndisputableMonolith.GameTheory.ESSFromSigma
domain
GameTheory
line
60 · 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 60.

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

  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

papers checked against this theorem

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