cascade_implies_ESS
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not compute the numerical value of either threshold.
- Does not prove that cascades occur for any specific fraction.
- Does not address subcritical dynamics or non-cascade behavior.
- Does not derive the underlying J-cost gradient or RCL.
Lean usage
cooperationCascadeCert where cascade_implies_ess := cascade_implies_ESSformal statement (Lean)
43theorem cascade_implies_ESS (frac : ℝ) (h : cascades frac) :
44 isESS frac := h
proof body
Term-mode proof.
45
46/-- Below threshold does not cascade. -/