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

ESSFromSigmaCert

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

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

  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.