cascade_implies_ESS

formal source

  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