isSigmaConservative
plain-language theorem explainer
The definition classifies a two-player joint outcome as sigma-conservative precisely when its sigma-charge is non-negative. Game theorists applying Recognition Science to the prisoner's dilemma cite this to identify which outcomes conserve the Noether charge sigma. It is implemented as a direct one-line abbreviation of the non-negativity condition on the sigma-charge function.
Claim. A joint outcome $o$ is $sigma$-conservative if $sigma(o) geq 0$, where $sigma(o)$ denotes the charge taking value $+1$ on mutual cooperation, $0$ on mixed strategies, and $-1$ on mutual defection.
background
In the module on Cooperation From sigma-Conservation, game-theoretic equilibria are characterized as J-cost minima on the multi-agent ledger. A JointOutcome pairs two player choices, each cooperate or defect. The sigma-charge function assigns +1 to mutual cooperation (creating coordinated value), 0 to mixed outcomes, and -1 to mutual defection (destroying coordinated value); this charge is the sigma-Noether charge of the multi-agent move.
proof idea
The declaration is a one-line definition that applies the sigma-charge function to the given outcome and asserts its non-negativity.
why it matters
This definition is used by the GameTheoryCert structure to certify the properties of sigma-conservation, including that mutual defection violates it while all other outcomes satisfy it. It realizes the second prediction of the module: cooperation from sigma-conservation, which explains the dominance of reciprocal-altruism strategies that preserve sigma. The result sits within the Recognition Science framework as part of element 84 in the game theory domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.