cascades
plain-language theorem explainer
The cascades predicate holds for a cooperator fraction precisely when that fraction meets or exceeds the cascade threshold. Evolutionary game theorists modeling n-person prisoner's dilemma would cite this definition to mark the point at which J-cost gradients drive a kin-cluster to full cooperation. It is a one-line abbreviation of the inequality against the threshold value.
Claim. Let $f$ be the cooperator fraction and let $1/φ$ be the cascade threshold (equal to the ESS threshold). The predicate cascades$(f)$ holds if and only if $f ≥ 1/φ$.
background
The Cooperation Cascade module develops the game-theory side of Recognition Science. If the cooperator fraction in a kin-cluster crosses $1/φ$, the J-cost gradient drives the cluster to full cooperation, matching observed thresholds in n-person prisoner's dilemma experiments. The upstream cascadeThreshold definition sets the threshold equal to cooperatorThreshold and states that this value equals $1/φ$.
proof idea
One-line definition that directly encodes the inequality cascadeThreshold ≤ frac. No lemmas or tactics are required beyond the definition of cascadeThreshold itself.
why it matters
This definition supplies the predicate used by cascade_implies_ESS (which states that cascades imply isESS), by the CooperationCascadeCert structure (which records threshold equality, the implication to ESS, and full cooperation), and by full_cooperation_cascades together with subcritical_does_not_cascade. It completes the cascade side of the §XXIII.C development, linking the J-cost gradient to the phi fixed point from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.