IndisputableMonolith.GameTheory.CooperationCascade

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.GameTheory.ESSFromSigma
   4
   5/-!
   6# Cooperation Cascade Theorem
   7
   8## §XXIII.C row "Game theory from first principles" — cascade side.
   9
  10If the cooperator fraction in a kin-cluster crosses `1/φ`, the
  11J-cost gradient drives the entire cluster to full cooperation.
  12This matches the observed cooperation thresholds in n-person
  13prisoner's dilemma experiments.
  14
  15## What this module provides
  16
  171. `cascade_threshold_eq_inv_phi`: the cascade threshold equals
  18   the ESS threshold from `ESSFromSigma`.
  192. `cascade_implies_ESS`: above-threshold implies ESS.
  203. `subcritical_does_not_cascade`: below-threshold does not.
  214. Master cert `CooperationCascadeCert` with 3 fields.
  22-/
  23
  24namespace IndisputableMonolith
  25namespace GameTheory
  26namespace CooperationCascade
  27
  28open Constants
  29open ESSFromSigma
  30
  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
  65  cascade_implies_ess : ∀ frac : ℝ, cascades frac → isESS frac
  66  full_cooperation : cascades 1
  67
  68/-- The master certificate is inhabited. -/
  69def cooperationCascadeCert : CooperationCascadeCert where
  70  threshold_eq := rfl
  71  cascade_implies_ess := cascade_implies_ESS
  72  full_cooperation := full_cooperation_cascades
  73
  74end
  75
  76end CooperationCascade
  77end GameTheory
  78end IndisputableMonolith
  79