cooperatorThreshold_lt_one
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not establish existence of ESS for any concrete population size.
- Does not derive the numerical value of the threshold; that is supplied by cooperatorThreshold.
- Does not address non-kin-selection models.
- Does not supply empirical calibration of φ in observed populations.
Lean usage
theorem all_cooperator_isESS : isESS 1 := le_of_lt cooperatorThreshold_lt_oneformal statement (Lean)
44theorem cooperatorThreshold_lt_one : cooperatorThreshold < 1 := by
proof body
Tactic-mode proof.
45 unfold cooperatorThreshold
46 have : 1 < phi := by have := phi_gt_onePointFive; linarith
47 rw [div_lt_one phi_pos]
48 exact this
49
50/-- The threshold is strictly positive. -/