JointOutcome
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not encode payoff matrices or utility functions.
- Does not distinguish repeated from one-shot games.
- Does not impose any conservation property on the outcome itself.
- Does not reference the J-cost functional or phi-ladder.
formal statement (Lean)
67structure JointOutcome where
68 p1 : Choice
69 p2 : Choice
70 deriving DecidableEq
71
72/-- The σ-charge of a joint outcome: `+1` for mutual cooperation
73 (creating coordinated value), `0` for mixed, `-1` for mutual
74 defection (destroying coordinated value). This is the σ-Noether
75 charge of the multi-agent move. -/