CooperationCascadeCert
plain-language theorem explainer
The CooperationCascadeCert structure collects three assertions: the cascade threshold equals the inverse of phi, crossing the threshold implies the fraction is an evolutionarily stable strategy, and the full-cooperation state satisfies the cascade predicate. Game theorists working from first principles in Recognition Science would cite this certificate to link the J-cost gradient to observed cooperation thresholds in multi-agent dilemmas. It is assembled directly from the module's prior definitions of cascades and isESS without further steps.
Claim. The structure asserts that the cascade threshold equals $1/φ$, that any real cooperator fraction satisfying the cascade predicate is an evolutionarily stable strategy, and that the full-cooperation fraction of 1 satisfies the cascade predicate.
background
In the Cooperation Cascade module the cascade predicate holds when the cooperator fraction meets or exceeds the cascadeThreshold, which is defined as the cooperatorThreshold imported from the ESS module. The isESS predicate requires the same threshold condition. This local setting follows the module statement that crossing $1/φ$ drives a kin-cluster to full cooperation via the J-cost gradient and matches n-person prisoner's dilemma experiments. Upstream results supply the cascades definition, the cascadeThreshold equality to cooperatorThreshold, and the isESS predicate from ESSFromSigma.
proof idea
The structure is defined by bundling three fields: an equality for the threshold, a universal quantification linking cascades to isESS, and the assertion that cascades holds at fraction 1. It draws on the cascades and cascadeThreshold definitions from the same module together with the isESS predicate from the ESSFromSigma import. No tactics are applied; the fields are populated by direct reference to prior results.
why it matters
This certificate serves as the master summary for the cascade side of game theory from first principles and feeds directly into the inhabited cooperationCascadeCert definition that confirms all three properties hold. It fills the §XXIII.C row by establishing the threshold match to $1/φ$ and the implication to ESS, consistent with the Recognition Science phi-ladder and J-cost framework. The result touches the open question of extending the n-agent statement to general mechanism design.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.