subcritical_does_not_cascade
plain-language theorem explainer
The theorem establishes that a cooperator fraction below the cascade threshold cannot trigger a cooperation cascade. Evolutionary game theorists modeling n-person prisoner's dilemmas would cite it to bound the basin where full cooperation remains unreachable. The proof is a one-line term reduction that unfolds the cascade predicate and negates the defining inequality.
Claim. Let $f$ be the cooperator fraction in a kin-cluster and let $τ$ be the cascade threshold. If $f < τ$, then it is not the case that $f ≥ τ$.
background
The Cooperation Cascade Theorem states that crossing the cooperator fraction 1/φ drives a kin-cluster to full cooperation via the J-cost gradient, matching observed thresholds in prisoner's dilemma experiments. The module supplies the threshold equality to the ESS value, the implication from above-threshold to ESS, the negation below threshold, and the master certificate with three fields. The cascade predicate is defined to hold exactly when the fraction meets or exceeds the threshold; the threshold itself is set equal to the cooperator threshold from the ESS analysis.
proof idea
The proof is a direct term-mode reduction. It unfolds the cascade predicate to expose the threshold inequality, pushes the negation inward, and matches the supplied hypothesis exactly.
why it matters
This result supplies the missing lower bound in the cascade trichotomy, completing the module's coverage of subcritical, critical, and supercritical regimes. It feeds the master CooperationCascadeCert and anchors the game-theory side of the Recognition Science derivation that begins from J-uniqueness and the phi fixed point. The placement confirms that the J-cost mechanism produces a sharp threshold at 1/φ without intermediate stable states.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.