full_cooperation_cascades
plain-language theorem explainer
The theorem establishes that the cascade predicate holds when the cooperator fraction reaches 1. Game theorists working on kin-selection models would cite it to confirm full cooperation lies in the cascade regime. The proof unfolds the cascade and threshold definitions, invokes the phi > 1.5 bound, and closes the resulting inequality with linear arithmetic.
Claim. The cascade predicate holds at cooperator fraction 1, i.e., cascadeThreshold ≤ 1 where cascadeThreshold equals 1/φ and φ denotes the golden ratio.
background
The module treats the cascade side of game theory derived from first principles in Recognition Science. The predicate cascades(frac) asserts that the cooperator fraction frac is at least the cascade threshold. This threshold equals the cooperatorThreshold from ESSFromSigma, defined as 1/phi. The module context is that a kin-cluster cooperator fraction crossing 1/phi triggers a J-cost gradient to full cooperation, aligning with experimental thresholds in n-person prisoner's dilemma games. The upstream result phi_gt_onePointFive provides the strict inequality 1.5 < phi used to establish the bound.
proof idea
The tactic proof first unfolds cascades, cascadeThreshold, and cooperatorThreshold. It obtains the fact 1 < phi from the lemma phi_gt_onePointFive. The division inequality is rewritten via div_le_iff₀, after which linarith closes the goal.
why it matters
This declaration populates the full_cooperation field in the master certificate CooperationCascadeCert. It completes the cascade implications in the game-theory section, showing that the phi-derived threshold permits full cooperation. The result ties the J-cost mechanism to observable cooperation dynamics and sits within the phi-ladder structure of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.