cooperationDividend_pos
plain-language theorem explainer
The cooperation dividend equals 1/φ and is strictly positive. Game theorists working in Recognition Science cite the result to confirm that cooperative strategies produce a positive per-agent surplus over mutual defection in σ-conserving games. The proof is a term-mode one-liner that unfolds the definition and applies div_pos to the numerator 1 and the denominator φ.
Claim. $0 < 1/φ$, where $φ$ is the golden-ratio fixed point of the Recognition Science forcing chain.
background
In the CooperationFromSigma module, game-theoretic equilibria are J-cost minima on the multi-agent ledger. The coordination dividend is defined directly as cooperationDividend := 1/φ, supplying the canonical RS coordination bonus of approximately 0.618. The module states that a coalition of n players yields total payoff n · π_coop = (n + 1/φ) · π_def, strictly larger than n-fold defection for n ≥ 1. Upstream, φ arises as the self-similar fixed point (T6) in the UnifiedForcingChain, and its positivity is presupposed by the forcing construction.
proof idea
The proof is a term-mode one-liner. It unfolds the definition of cooperationDividend to 1/φ, then applies the lemma div_pos to the numerator 1 (discharged by norm_num) and the denominator φ (discharged by phi_pos).
why it matters
This theorem supplies the positivity hypothesis required by coalition_strictly_better, which shows coalition payoff strictly exceeds n-fold defection, and by the master certificate gameTheoryCert. It instantiates the coordination bonus 1/φ predicted by the self-similar fixed point φ (T6) and the eight-tick octave (T7). The result closes one link from σ-conservation to observable cooperation dividends in the GameTheory domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.