cascadeThreshold
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the threshold value from the Recognition Composition Law.
- Does not specify the J-cost function explicitly.
- Does not prove stability for non-kin populations.
- Does not compute numerical values for specific dilemma payoffs.
formal statement (Lean)
34def cascadeThreshold : ℝ := cooperatorThreshold
proof body
Definition body.
35
36/-- Cascade threshold equals `1/φ`. -/