theorem
proved
no_cooperator_not_isESS
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.GameTheory.ESSFromSigma on GitHub at line 60.
browse module
All declarations in this module, on Recognition.
explainer page
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