DD_not_sigma_conservative
plain-language theorem explainer
Mutual defection produces joint σ equal to -1 and therefore violates σ-conservation. Researchers modeling iterated games under Recognition Science cite this to isolate defect-defect as the sole non-conservative outcome in the prisoner's dilemma. The proof is a direct term reduction that substitutes the explicit σ value and normalizes the resulting inequality.
Claim. The mutual-defection outcome fails σ-conservation: ¬(jointSigma(⟨defect, defect⟩) ≥ 0).
background
In the CooperationFromSigma module, game-theoretic equilibria arise as J-cost minima on the multi-agent ledger. The predicate isSigmaConservative holds precisely when jointSigma o ≥ 0 for a JointOutcome o. Upstream, DD_sigma_neg establishes that jointSigma of the mutual-defect pair equals -1, while defect denotes the defect choice in the joint outcome constructor.
proof idea
The term proof unfolds isSigmaConservative to expose the inequality on jointSigma, rewrites using DD_sigma_neg to obtain -1, pushes the negation, and applies norm_num to reach the arithmetic contradiction.
why it matters
This result supplies the DD_violates field inside gameTheoryCert and is invoked inside sigma_conservative_iff to establish the equivalence between σ-conservation and avoidance of mutual defection. It realizes the module prediction that defect-defect is the unique σ-non-conservative outcome, consistent with the Recognition Science claim of cooperation from σ-conservation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.