CD_sigma_zero
plain-language theorem explainer
CD_sigma_zero establishes that the joint σ-charge equals zero for the mixed cooperate-defect outcome. Game theorists working in Recognition Science would cite this when partitioning two-player outcomes into σ-conservative and non-conservative classes under the prisoner's dilemma normal form. The equality follows by direct computation from the case definition of jointSigma.
Claim. Let σ denote the joint σ-charge on a JointOutcome. Then σ(cooperate, defect) = 0.
background
The module CooperationFromSigma models game-theoretic equilibria as J-cost minima on the multi-agent ledger. The central object is the joint σ-charge, defined by cases on the pair of actions: +1 for mutual cooperation (creating coordinated value), 0 for mixed outcomes, and -1 for mutual defection (destroying coordinated value). This σ serves as the Noether charge of the multi-agent move, consistent with the Recognition Composition Law.
proof idea
The proof is a one-line reflexivity step on the definition of jointSigma. The match expression returns 0 explicitly for the cooperate-defect case, so the equality holds by computation.
why it matters
This result supplies the zero value for mixed outcomes in the trichotomy used by the parent theorem nonDD_sigma_conservative, which proves every outcome except defect-defect is σ-conservative. It completes the classification required by the module's statement that only mutual defection violates σ-conservation, thereby supporting the claims on reciprocal altruism and the coordination dividend. The fact aligns with T5 J-uniqueness and the σ-Noether interpretation in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.