CC_sigma_pos
plain-language theorem explainer
Mutual cooperation carries σ-charge +1 under the joint outcome definition. Game theorists modeling J-cost minima on the multi-agent ledger cite this to separate cooperative from defective equilibria. The proof is a direct reflexivity reduction on the case analysis of the joint σ function.
Claim. The σ-charge of the mutual-cooperation outcome equals 1.
background
The module treats game-theoretic equilibria as J-cost minima on the multi-agent ledger. The jointSigma definition assigns σ = +1 to mutual cooperation (creating coordinated value), σ = 0 to mixed outcomes, and σ = -1 to mutual defection (destroying coordinated value); this σ acts as the Noether charge of the multi-agent move. The local setting states that a two-player game is cooperative precisely when joint σ is conserved across moves, with the coordination dividend fixed at the factor 1/φ.
proof idea
This is a term-mode proof consisting of a single reflexivity reduction that matches the cooperate-cooperate case in the jointSigma definition.
why it matters
The result supplies the CC_sigma field of the gameTheoryCert certificate and the first conjunct of the game_theory_one_statement theorem. It completes the positive half of the σ-conservation claim for element 84, confirming that only mutual defection violates σ while cooperation preserves it and supports dominance of reciprocal-altruism strategies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.