pith. sign in
module module high

IndisputableMonolith.GameTheory.CooperationCascade

show as:
view Lean formalization →

The CooperationCascade module defines the cooperation cascade threshold and shows it equals the ESS threshold of 1/phi. Researchers working on evolutionary stability or RS-derived game theory would cite it to connect static ESS conditions to dynamical cascade behavior. The module organizes definitions and equality lemmas that import the phi-based threshold directly from the upstream ESSFromSigma result.

claimThe cascade threshold equals the ESS threshold and is given by $\phi^{-1}$, where $\phi$ is the golden ratio fixed point of the Recognition Composition Law.

background

The module sits inside the GameTheory domain and imports the RS time quantum $\tau_0 = 1$ tick from Constants together with the ESS existence criterion from ESSFromSigma. The upstream doc-comment states: "An evolutionarily stable strategy (ESS) is a strategy that, once adopted by the majority, cannot be invaded by a rare mutant. In RS, ESS exists iff the cooperator fraction is at least 1/phi in a kin-selected population." The cascade threshold is introduced as the dynamical counterpart to this static stability bound.

proof idea

This is a definition module, no proofs. It supplies the cascadeThreshold definition, the equality cascadeThreshold_eq_inv_phi, and supporting lemmas that link the threshold to the phi-ladder already established in ESSFromSigma.

why it matters in Recognition Science

The module supplies the cascade threshold that matches the ESS threshold, thereby extending the "Game theory from first principles" row of §XXIII.C. It feeds the parent claim that cooperation dynamics are governed by the same 1/phi bound derived from sigma-conservation. No downstream uses are recorded yet.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)