JointOutcome
plain-language theorem explainer
JointOutcome packages a pair of individual choices into a single record for two-player games. Game theorists citing the Recognition Science account of cooperation via σ-conservation use it to define the Noether charge of coordinated moves. The structure is introduced as a direct record with a deriving clause that supplies decidable equality for subsequent case analysis.
Claim. A joint outcome is a pair $(c_1, c_2)$ where each $c_i$ is an element of the two-element set of player moves (cooperate or defect).
background
The module develops game-theoretic equilibria as J-cost minima on the product of strategy spaces, with σ-conservation distinguishing cooperative from non-cooperative outcomes. Choice is the inductive type whose constructors are cooperate and defect. JointOutcome aggregates one choice from each player so that the joint σ-charge can be assigned by cases on the pair, inheriting decidable equality to support pattern matching in downstream definitions.
proof idea
The declaration is a plain structure definition that records two fields of type Choice and derives DecidableEq. No lemmas are invoked; the construction is direct and carries no proof obligations.
why it matters
JointOutcome supplies the domain for jointSigma, which assigns the values +1 (mutual cooperation), 0 (mixed), and -1 (mutual defection). It is the carrier object for the GameTheoryCert that certifies mutual defection as the unique σ-non-conservative outcome and for the equivalence between σ-conservation and non-DD outcomes. The structure therefore closes the element-84 development linking σ-conservation to the emergence of cooperation in the Recognition Science ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.