ESSFromSigmaCert
plain-language theorem explainer
The ESSFromSigmaCert structure packages four properties establishing that the cooperator threshold 1/φ yields an evolutionarily stable strategy in the Recognition Science game-theoretic model. Game theorists working in kin-selection or Hamilton-rule contexts would cite it to anchor the ESS existence claim. The definition is a direct structure declaration that assembles already-proved lemmas on positivity, boundedness, and the ESS predicate at the boundary points.
Claim. The master certificate asserts that the cooperator threshold satisfies $0 < 1/φ < 1$, that the strategy of universal cooperation meets the ESS predicate, and that the strategy of universal defection does not.
background
In the module on Evolutionarily Stable Strategies from σ-Conservation, the cooperator threshold is defined as $1/φ ≈ 0.618$, where φ is the golden ratio arising as the self-similar fixed point in the Recognition Science forcing chain. The predicate isESS(cooperator_fraction) holds precisely when cooperator_fraction ≥ 1/φ. This reframes Hamilton's rule r > c/b as the inequality cooperator_fraction ≥ 1/φ in RS-native units. Upstream results include the definition of the cooperator threshold and the ESS predicate, together with positivity and strict inequality lemmas.
proof idea
This is a structure definition that directly assembles four fields: the positivity and upper bound on the threshold from the corresponding lemmas, together with the boundary cases for the ESS predicate at full cooperation and no cooperation. No tactics are required; it is a pure data structure whose fields are supplied by sibling lemmas.
why it matters
This certificate is the master object that demonstrates the ESS threshold is well-defined and satisfies the required stability properties. It is used by the downstream definition that exhibits an explicit inhabitant, closing the existence claim for the ESS in the σ-conservation framework. Within the Recognition Science program it supplies the game-theoretic counterpart to the forcing-chain results T5–T8, confirming that the phi-ladder yields a stable cooperation threshold at 1/φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.