nonDD_sigma_conservative
plain-language theorem explainer
Every joint outcome except mutual defection preserves non-negative joint σ in the Recognition Science two-player model. Game theorists working with J-cost minima would cite the result to isolate cooperative equilibria from the unique defective one. The proof exhausts the four choice pairs, rewrites with the precomputed σ values for the three non-DD cases, and derives a contradiction from the hypothesis on the DD case.
Claim. Let $o$ be a joint outcome of two players' choices. If $o$ is not mutual defection, then the joint σ-charge satisfies $σ(o) ≥ 0$.
background
JointOutcome pairs one Choice for each of two players. The function jointSigma returns +1 on mutual cooperation, 0 on mixed outcomes, and -1 on mutual defection; this is the σ-Noether charge of the joint move. isSigmaConservative holds exactly when jointSigma o ≥ 0.
proof idea
The term proof begins with rcases on the outcome structure, then cases on both choices. The CC case rewrites with CC_sigma_pos and normalizes; the CD and DC cases rewrite with the zero theorems; the DD case is discharged by exfalso applied to the non-DD hypothesis.
why it matters
The theorem supplies the forward implication for sigma_conservative_iff and populates the nonDD_conservative field of gameTheoryCert. It realizes the module claim that defect-defect is the sole σ-non-conservative outcome, thereby grounding the prediction that reciprocal-altruism strategies dominate iterated play. It closes the σ-conservation step of Element 84 in the GameTheory domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.