cooperatorThreshold_pos
plain-language theorem explainer
The cooperator threshold for evolutionary stability equals 1/φ and is strictly positive. Game theorists applying Hamilton's rule in kin-selected populations cite this to confirm the threshold lies in (0,1). The proof is a one-line term that unfolds the definition and invokes positivity of division by a positive quantity.
Claim. $0 < 1/φ$, where $φ$ is the golden-ratio fixed point of the Recognition Composition Law.
background
The module derives evolutionarily stable strategies from σ-conservation. An ESS exists precisely when the cooperator fraction meets or exceeds the threshold 1/φ ≈ 0.618, reframing Hamilton's rule as cooperator_fraction ≥ 1/φ in RS-native units. The definition cooperatorThreshold := 1/φ supplies the numerical value used throughout the module.
proof idea
Unfold cooperatorThreshold to obtain 1/φ, then apply the term div_pos one_pos phi_pos. The lemmas one_pos and phi_pos supply the two positivity hypotheses required by div_pos.
why it matters
The result populates the threshold_pos field of the master certificate essFromSigmaCert. It closes the positivity half of the interval (0,1) for the ESS predicate, consistent with the self-similar fixed point φ forced at T6 and the eight-tick octave. The companion theorem no_cooperator_not_isESS re-uses the same positivity to show the empty-cooperator strategy fails to be stable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.