isESS
plain-language theorem explainer
The ESS predicate holds for a cooperator fraction when it meets or exceeds the stability threshold of one over phi. Game theorists applying kin-selection models in Recognition Science would cite this predicate to check whether a strategy resists invasion by defectors. The definition consists of a direct inequality comparison to the pre-defined threshold value.
Claim. The predicate holds for cooperator fraction $f$ precisely when $f$ satisfies $f ≥ 1/φ$, where $φ$ is the golden ratio.
background
The module develops evolutionarily stable strategies from σ-conservation in game theory. It introduces cooperatorThreshold as the real number one divided by phi, serving as the minimal cooperator fraction for stability in kin-selected populations. As stated in the cooperatorThreshold definition, it is the cooperator-fraction threshold for ESS in a kin-selected population: 1/φ ≈ 0.618. This setup reframes Hamilton's rule by setting the cost-benefit ratio to the RS-native value one over phi.
proof idea
The definition is a one-line abbreviation that sets the predicate to the inequality between cooperatorThreshold and the input cooperator fraction. It applies the standard ordering on the reals with no additional lemmas required.
why it matters
This predicate forms the central definition feeding the ESSFromSigmaCert master certificate, which records the threshold bounds, the all-cooperator case as stable, and the no-cooperator case as unstable. It is invoked in cascade_implies_ESS to connect cooperation cascades to evolutionary stability. Within the framework it instantiates the phi fixed point from the forcing chain as the invasion threshold, completing the game-theoretic derivation from σ-conservation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.