DC_sigma_zero
plain-language theorem explainer
The mixed outcome with one defect and one cooperate carries zero joint sigma-charge on the Recognition Science ledger. Game theorists modeling cooperation via sigma-conservation would cite this to classify all non-mutual-defection outcomes as sigma-preserving. The proof is a direct reflexivity reduction on the case definition of jointSigma.
Claim. Let $o$ be the joint outcome with first player defect and second player cooperate. Then the joint sigma-charge satisfies $o = 0$.
background
In this module the jointSigma function assigns the sigma-charge to each pair of actions in a two-player game. By definition it returns +1 for mutual cooperation (creating coordinated value), 0 for mixed outcomes, and -1 for mutual defection (destroying coordinated value). This is the sigma-Noether charge of the multi-agent move. The defect functional equals J for positive arguments, while upstream results supply the active edge count A per fundamental tick and the simplicial ledger structure for edge lengths from psi.
proof idea
The proof is a one-line wrapper that applies reflexivity to the jointSigma definition on the specific constructor for defect-cooperate, which matches the mixed case returning 0.
why it matters
DC_sigma_zero is invoked by nonDD_sigma_conservative to show every outcome except mutual defection is sigma-conservative. It completes the four-outcome classification in the module, confirming defect-defect as the unique sigma-violator. This supports the claim that a two-player game is cooperative iff joint sigma is conserved across moves, consistent with the coordination dividend of 1/phi and the prediction that reciprocal-altruism strategies dominate iterated play.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.