game_theory_one_statement
plain-language theorem explainer
The theorem states that mutual cooperation carries joint sigma charge +1, mutual defection carries -1, the cooperation dividend lies in (0.617, 0.622), and any n-agent cooperative coalition strictly exceeds the n-fold defection payoff. Game theorists modeling equilibria as J-cost minima would cite this as the compact summary of sigma-driven cooperation. The proof is a one-line term that simply packages four prior lemmas, one for each clause.
Claim. In the multi-agent ledger the joint sigma charge satisfies sigma(cooperate, cooperate) = 1 and sigma(defect, defect) = -1; the cooperation dividend delta obeys 0.617 < delta < 0.622; and for every natural number n and positive real baseline payoff pi the coalition payoff (n + delta) pi strictly exceeds n pi.
background
The module treats game-theoretic equilibria as stationary points of the joint J-cost functional on strategy profiles. Joint sigma is the conserved charge whose sign distinguishes cooperative from defective outcomes; the cooperation dividend is the additive factor 1/phi that appears in coalition payoffs. Coalition payoff is defined as (n + dividend) times the defection baseline. Upstream, CC_sigma_pos shows sigma(cooperate, cooperate) = 1 by direct computation, while coalition_strictly_better uses the positivity of the dividend to obtain the strict inequality via nlinarith.
proof idea
The proof is the term tuple consisting of CC_sigma_pos, DD_sigma_neg, cooperationDividend_band and coalition_strictly_better. Each conjunct is discharged by a prior theorem already established in the same module; no additional tactics or reductions are required.
why it matters
This is the one-statement theorem labeled element 84 that condenses the game-theory predictions of Recognition Science. It directly encodes the claim that cooperation follows from sigma conservation while defect-defect is the sole sigma-violating outcome, with the numerical dividend 1/phi drawn from the phi-ladder. The result closes the CooperationFromSigma section and supplies the concrete falsifiers listed in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.