DD_sigma_neg
plain-language theorem explainer
Mutual defection carries joint σ-charge of -1. Analysts of σ-conservation in two-player games cite this when establishing defect-defect as the sole violator in the prisoner's dilemma normal form. The proof reduces immediately to the case definition of the joint σ-charge function.
Claim. The σ-charge of the mutual-defection outcome satisfies $σ(⟨defect, defect⟩) = -1$.
background
The joint σ-charge function assigns values to two-player outcomes: +1 for mutual cooperation (creating coordinated value), 0 for mixed strategies, and -1 for mutual defection (destroying coordinated value). This σ acts as the Noether charge of the multi-agent move on the J-cost ledger. The defect choice itself equals the J-functional applied to positive reals, per the upstream Law of Existence definition.
proof idea
The proof is a one-line wrapper that applies the definition of the joint σ-charge function to the defect-defect pair, which matches the -1 case by reflexivity.
why it matters
This supplies the negative σ value required for the game theory certificate and the one-statement theorem that collects the four clauses of element 84. It confirms mutual defection as the unique σ-non-conservative outcome in the 2x2 normal form, which explains why σ-preserving strategies dominate iterated play. The result anchors the module claim that cooperation arises precisely when joint σ is conserved across moves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.