cooperationCascadeCert
plain-language theorem explainer
The cooperationCascadeCert definition inhabits the master certificate for the cooperation cascade. It certifies that the threshold equals 1/φ, that any cascading fraction is evolutionarily stable, and that full cooperation cascades. The construction uses reflexivity on the threshold equality together with direct insertion of the cascade_implies_ESS and full_cooperation_cascades theorems.
Claim. There exists a certificate $C$ such that $C$ asserts cascadeThreshold $= 1/φ$, that cascades(frac) implies isESS(frac) for any real frac, and that cascades(1) holds.
background
In this module the predicate cascades(frac) holds precisely when the cooperator fraction frac meets or exceeds cascadeThreshold. The structure CooperationCascadeCert packages three claims: equality of that threshold to $1/φ$, the implication from cascades to evolutionary stability (isESS), and the fact that the fraction 1 cascades. Upstream, cascade_implies_ESS reduces the implication to the hypothesis itself, while full_cooperation_cascades proves cascades(1) by unfolding the definitions and applying phi > 1.5 together with the inequality 1 < phi.
proof idea
The definition builds the CooperationCascadeCert record by assigning threshold_eq via rfl, cascade_implies_ess via the theorem cascade_implies_ESS, and full_cooperation via the theorem full_cooperation_cascades. No additional tactics or reductions are performed.
why it matters
This definition supplies the inhabited master certificate for the Cooperation Cascade Theorem in §XXIII.C, confirming the threshold match with the ESS side and the implications to stability and full cooperation. It links the phi fixed point (T6) and J-uniqueness (T5) to observed thresholds in n-person prisoner's dilemma experiments. No downstream uses are recorded, so the certificate stands as a terminal packaging step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.