cascadeThreshold
plain-language theorem explainer
The cascade threshold is defined to equal the cooperator threshold from the ESS analysis. Game theorists modeling kin-selected populations in n-person dilemmas would cite it to mark the critical fraction above which the J-cost gradient drives full cooperation. The declaration is a direct abbreviation of the upstream cooperatorThreshold definition.
Claim. Let $1/phi$ denote the cooperator threshold. The cascade threshold is the real number $1/phi$.
background
The Cooperation Cascade module develops the game theory side of Recognition Science by showing how the J-cost gradient induces cooperation cascades in kin-clusters. The cascadeThreshold is set equal to cooperatorThreshold, which the upstream ESSFromSigma module defines as $1/phi approx 0.618$, the fraction at or above which a strategy is evolutionarily stable. The module documentation notes that this threshold matches experimental observations in n-person prisoner's dilemma games.
proof idea
One-line wrapper that applies the cooperatorThreshold definition from the ESSFromSigma module.
why it matters
This supplies the shared threshold value for the cascades predicate and the CooperationCascadeCert master certificate. It links the cascade behavior to the ESS threshold, supporting theorems such as full_cooperation_cascades and subcritical_does_not_cascade. The declaration completes the cascade side of the game theory from first principles section, tying into the phi-based fixed point from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.