cascade_implies_ESS
plain-language theorem explainer
A cooperator fraction above the cascade threshold satisfies the evolutionary stable strategy predicate. Game theorists modeling n-person prisoner's dilemma cooperation thresholds cite this link between cascade dynamics and ESS. The proof is a direct one-line wrapper applying the hypothesis, using the prior equality of the two thresholds.
Claim. Let $f$ be the cooperator fraction. If $f$ satisfies cascades (i.e., cascadeThreshold $leq f$), then $f$ satisfies isESS (i.e., cooperatorThreshold $leq f$).
background
The module derives the Cooperation Cascade Theorem from first principles: when the cooperator fraction in a kin-cluster crosses $1/phi$, the J-cost gradient forces the cluster to full cooperation, matching n-person prisoner's dilemma data. cascades frac is the predicate cascadeThreshold $leq$ frac. isESS frac is the predicate cooperatorThreshold $leq$ frac. Upstream result cascadeThreshold_eq_inv_phi establishes that the thresholds are identical.
proof idea
One-line wrapper that applies the hypothesis h : cascades frac directly to discharge the goal isESS frac, after the thresholds have been shown equal in the upstream equality lemma.
why it matters
This theorem supplies the cascade_implies_ess field of the master certificate CooperationCascadeCert, which is inhabited by construction. It completes the cascade side of the game-theory derivation in module §XXIII.C, tying the threshold to the phi-ladder and the eight-tick octave. The result supports the claim that supercritical fractions are evolutionarily stable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.