all_cooperator_isESS
plain-language theorem explainer
All-cooperator strategy satisfies the ESS predicate because the cooperator threshold 1/φ lies strictly below unity. Researchers deriving Hamilton-rule equivalents from σ-conservation in Recognition Science cite this result to bound the stable regime from above. The proof is a one-line wrapper that invokes the already-proved strict inequality cooperatorThreshold_lt_one via the order lemma le_of_lt.
Claim. The strategy in which every agent cooperates is evolutionarily stable: if the cooperator threshold equals 1/φ then 1/φ ≤ 1, where φ denotes the golden ratio fixed point of the Recognition Composition Law.
background
The module defines an evolutionarily stable strategy via the predicate isESS(cooperator_fraction) ≔ cooperatorThreshold ≤ cooperator_fraction, with cooperatorThreshold set to 1/φ. This construction reframes Hamilton’s rule inside RS-native units so that the cost-benefit ratio c/b becomes the reciprocal of the golden ratio. The local setting is the σ-conservation row of the game-theory development, which treats ESS existence as equivalent to the cooperator fraction lying in the closed interval [1/φ, 1].
proof idea
The proof is a one-line wrapper that applies the upstream lemma cooperatorThreshold_lt_one (which states 1/φ < 1) together with the order-preserving map le_of_lt to obtain the required non-strict inequality.
why it matters
The theorem supplies the all_coop_isESS field of the master certificate essFromSigmaCert, thereby completing the four-field certificate that the module advertises. It instantiates the upper endpoint of the ESS interval required by the σ-conservation argument and links directly to the self-similar fixed point (T6) of the forcing chain. No open scaffolding remains inside the file once this result and its sibling no_cooperator_not_isESS are in place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.