cooperationDividend_lt_one
plain-language theorem explainer
Recognition Science game theory bounds the cooperation dividend strictly below 1, confirming that σ-conservative cooperation yields a positive surplus over defection baselines without doubling per-agent payoffs. Analysts of J-cost Nash equilibria in multi-agent ledgers cite this bound when deriving coalition scaling from the phi-forcing constants. The proof is a one-line wrapper that extracts the upper estimate from the dividend band lemma and concludes via linear arithmetic.
Claim. In σ-conservative games the cooperation dividend δ satisfies δ < 1, where the total payoff for an n-agent coalition equals (n + δ) π_def with δ = φ^{-1} the canonical coordination bonus.
background
The module treats game-theoretic equilibria as stationary points of the joint J-cost functional on strategy spaces, with J the Recognition cost derived from the phi-forcing chain (T5–T6). σ-conservation distinguishes cooperative outcomes from the unique non-conservative defect-defect case in the prisoner's dilemma normal form. The coordination dividend is the extra factor 1/φ arising for coalitions, with φ the self-similar fixed point fixed by the forcing chain.
proof idea
The proof is a one-line wrapper. It obtains the bounding pair from the cooperationDividend_band lemma (itself resting on phi-forcing and ledger factorization structures) and applies linarith to extract the strict inequality δ < 1 from the upper component of the band.
why it matters
The result populates the master gameTheoryCert certificate and completes the coordination-dividend claim in Element 84 of the module. It directly instantiates the phi-ladder bonus (1/φ ≈ 0.618) predicted by T6 and the eight-tick octave, while the module falsifier list flags any empirical dividend measured outside the band as a potential refutation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.