cooperatorThreshold_lt_one
plain-language theorem explainer
The theorem shows that the ESS cooperator threshold 1/φ lies strictly below 1. Researchers modeling kin-selected populations cite it to confirm the invasion threshold sits inside the open unit interval. The short tactic proof unfolds the definition, pulls the bound φ > 1.5 from phi_gt_onePointFive, and applies the division inequality.
Claim. The cooperator-fraction threshold satisfies $1/φ < 1$.
background
In the Recognition Science treatment of game theory the cooperatorThreshold is defined as 1/φ. The module derives evolutionarily stable strategies from σ-conservation and reframes Hamilton's rule so that a strategy is ESS precisely when the cooperator fraction meets or exceeds 1/φ. The local setting supplies the threshold, the isESS predicate, and the master certificate ESSFromSigmaCert. Upstream, phi_gt_onePointFive supplies the concrete lower bound φ > 1.5 that drives the inequality.
proof idea
The proof unfolds cooperatorThreshold to 1/φ. It obtains 1 < φ from phi_gt_onePointFive via linarith. It then rewrites with div_lt_one (after phi_pos) and closes with the resulting inequality.
why it matters
This result feeds all_cooperator_isESS and populates the master certificate essFromSigmaCert. It confirms that the RS-native threshold 1/φ lies inside (0,1), consistent with the phi-ladder and the eight-tick octave structure. The module positions the inequality as the game-theoretic counterpart to the forcing chain T5-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.