def
definition
cascadeThreshold
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.GameTheory.CooperationCascade on GitHub at line 34.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
31noncomputable section
32
33/-- The cascade threshold (same as ESS threshold). -/
34def cascadeThreshold : ℝ := cooperatorThreshold
35
36/-- Cascade threshold equals `1/φ`. -/
37theorem cascadeThreshold_eq_inv_phi : cascadeThreshold = 1 / phi := rfl
38
39/-- Cooperation cascade predicate: fraction above threshold. -/
40def cascades (frac : ℝ) : Prop := cascadeThreshold ≤ frac
41
42/-- Cascade implies ESS. -/
43theorem cascade_implies_ESS (frac : ℝ) (h : cascades frac) :
44 isESS frac := h
45
46/-- Below threshold does not cascade. -/
47theorem subcritical_does_not_cascade (frac : ℝ) (h : frac < cascadeThreshold) :
48 ¬ cascades frac := by
49 unfold cascades
50 push_neg
51 exact h
52
53/-- Full cooperation cascades. -/
54theorem full_cooperation_cascades : cascades 1 := by
55 unfold cascades cascadeThreshold cooperatorThreshold
56 have hphi : 1 < phi := by have := phi_gt_onePointFive; linarith
57 rw [div_le_iff₀ phi_pos]
58 linarith
59
60/-! ## Master certificate -/
61
62/-- **COOPERATION CASCADE MASTER CERTIFICATE.** -/
63structure CooperationCascadeCert where
64 threshold_eq : cascadeThreshold = 1 / phi