no_cooperator_not_isESS
plain-language theorem explainer
The theorem shows that a population with zero cooperators cannot satisfy the ESS predicate in the Recognition Science model. Game theorists citing Hamilton's rule reframed via σ-conservation would reference it to enforce the strict lower bound on cooperation. The proof is a one-line term reduction that unfolds isESS and invokes the positivity of the threshold 1/φ.
Claim. The zero-cooperator strategy fails to be evolutionarily stable: it is not the case that cooperator fraction zero meets or exceeds the threshold, i.e., ¬(1/φ ≤ 0), where φ is the golden ratio fixed by the self-similar point in the forcing chain.
background
The module derives evolutionarily stable strategies from σ-conservation. It defines cooperatorThreshold as 1/φ and isESS(cooperator_fraction) as the predicate cooperatorThreshold ≤ cooperator_fraction. This reframes Hamilton's rule r > c/b into the requirement that the cooperator fraction is at least 1/φ in RS-native units.
proof idea
The term-mode proof unfolds the definition of isESS to expose the inequality cooperatorThreshold ≤ 0. Push_neg converts the negated goal into 0 < cooperatorThreshold. The goal is discharged exactly by the upstream lemma cooperatorThreshold_pos.
why it matters
The result supplies one of the four fields required by the master certificate essFromSigmaCert, confirming that the ESS predicate behaves correctly at the lower boundary. It closes the lower-bound half of the claim that ESS exists precisely when the cooperator fraction is at least 1/φ, completing the game-theoretic side of the σ-derived Hamilton reformulation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.