isESS
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not compute or prove the value of the threshold.
- Does not apply to populations without kin selection.
- Does not model invasion dynamics or time evolution.
- Does not certify specific population fractions beyond the predicate definition.
formal statement (Lean)
40def isESS (cooperator_fraction : ℝ) : Prop :=
proof body
Definition body.
41 cooperatorThreshold ≤ cooperator_fraction
42
43/-- The threshold is strictly less than 1. -/