Choice
plain-language theorem explainer
The binary strategy set for each agent in a two-player game consists of cooperation and defection. Game theorists applying Recognition Science to sigma conservation cite this when building joint outcomes and checking conservation across moves. The declaration is a standard inductive type with two constructors that automatically derives decidable equality and inhabitedness.
Claim. The set of player strategies consists of the two elements cooperate and defect.
background
The module treats game-theoretic equilibria as J-cost minima on the multi-agent ledger, with Nash points as stationary points of the joint J-cost functional. The defect functional equals J(x) for positive x and vanishes at unity. Upstream results fix A as the active edge count per tick (equal to 1) and satisfy the phi-power balance identity at D=3; the actualization operator A maps a configuration to the J-minimizing successor.
proof idea
The declaration is an inductive definition that introduces the two constructors cooperate and defect, then derives DecidableEq and Inhabited.
why it matters
This supplies the strategy space for the structure JointOutcome, which records sigma charge (+1 for mutual cooperation). It supports the downstream result equilibrium_is_zero that establishes degeneracy at J=0. The definition fills the game-theory slot in the sigma-conservation analysis, linking directly to the module's claim that defect-defect is the unique non-conservative outcome and that reciprocal-altruism strategies preserve sigma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.