sigma_conservative_iff
plain-language theorem explainer
The declaration proves that a joint outcome is σ-conservative precisely when it avoids mutual defection. Game theorists applying Recognition Science to equilibria would cite this to separate cooperative from non-cooperative moves via the σ-Noether charge. The proof is a short tactic script that splits the biconditional and invokes the two auxiliary lemmas after case analysis on the outcome pair.
Claim. For a joint outcome $o = (p_1, p_2)$, $o$ is σ-conservative if and only if it is not the case that both $p_1$ and $p_2$ are defect.
background
In this module joint outcomes are pairs of choices for two players. The σ-charge of such an outcome is defined as +1 for mutual cooperation, 0 for mixed pairs, and -1 for mutual defection; it functions as the Noether charge attached to the multi-agent move. The module states that two-player games are cooperative exactly when joint σ is conserved across moves, with defect-defect the unique non-conservative case. This rests on the defect functional (equal to J for positive arguments) and on the arithmetic constructions that supply the underlying integers and rationals.
proof idea
The tactic proof opens with refine to produce both directions of the biconditional. The forward direction applies nonDD_sigma_conservative to the assumption that the outcome is not defect-defect. The converse assumes σ-conservative and defect-defect, rewrites the outcome to the explicit defect pair via cases and simp, then applies DD_not_sigma_conservative.
why it matters
The equivalence supplies the precise link between σ-conservation and cooperative (positive-sum) outcomes required by the module's second prediction. It thereby supports the claim that reciprocal-altruism strategies dominate iterated play because they preserve σ. Within the broader framework it connects the J-cost minima characterization of Nash equilibria to the coordination dividend of 1/φ. No downstream theorems yet depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.