essFromSigmaCert
plain-language theorem explainer
The master certificate for evolutionarily stable strategies is inhabited by direct field assignment from four sibling lemmas. Game theorists in the Recognition Science program cite it to confirm that the cooperator threshold at 1/phi is positive and less than one, that full cooperation is stable, and that zero cooperation is unstable. The construction is a one-line record definition that assembles the positivity, bound, and stability results.
Claim. Let $tau = 1/phi$. There exists a certificate $C$ such that $0 < tau$, $tau < 1$, the all-cooperator strategy is evolutionarily stable, and the zero-cooperator strategy is not evolutionarily stable.
background
In the Recognition Science treatment of game theory, an evolutionarily stable strategy (ESS) is one that cannot be invaded by a rare mutant once adopted by the majority. The module defines the cooperator threshold as $tau = 1/phi$, where $phi$ is the golden ratio, and declares a strategy with cooperator fraction $f$ to be an ESS precisely when $f >= tau$. This reframes Hamilton's rule in RS-native units as cooperator_fraction >= 1/phi.
proof idea
The definition constructs the certificate by direct field assignment. It sets threshold_pos to the theorem establishing positivity of the threshold via division of positives, threshold_lt_one to the bound proof that uses phi > 1.5 and the division inequality, all_coop_isESS to the lemma that applies the threshold comparison at full cooperation, and no_coop_not_isESS to the negation that pushes the threshold positivity into the definition of isESS.
why it matters
This declaration completes the ESSFromSigma module by exhibiting an inhabited master certificate, confirming consistency of the ESS threshold derived from sigma-conservation. It supports the claim that ESS exists iff the cooperator fraction is at least 1/phi and closes the game-theory side of the first-principles row in the framework. No downstream uses are recorded, but the certificate stands as the top-level existence statement for the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.