`cascadeThreshold_eq_inv_phi`

proved

show as: view math explainer →

module: IndisputableMonolith.GameTheory.CooperationCascade
domain: GameTheory
line: 37 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.GameTheory.CooperationCascade on GitHub at line 37.

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

cascadeThreshold IndisputableMonolith.GameTheory.CooperationCascade

formal source

  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
  65  cascade_implies_ess : ∀ frac : ℝ, cascades frac → isESS frac
  66  full_cooperation : cascades 1
  67

papers checked against this theorem

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