EconCSLib.GameTheory.StrategicGame.ZeroSum.Basic

Zero-sum and constant-sum two-player games.

Main definitions

• IsZeroSum — payoffs sum to zero at every profile [MSZ 4.39]
• IsConstantSum — payoffs sum to a constant at every profile

Main results

• isZeroSum_iff_isConstantSum_zero — IsZeroSum G ↔ IsConstantSum G 0
• IsZeroSum.welfare_eq_zero — two-player zero-sum welfare collapses to 0
• IsConstantSum.welfare_eq — constant-sum welfare equals the constant
• IsConstantSum.neg — player 1's payoff equals c - player 0's payoff
• IsZeroSum.neg — one player's payoff is the negation of the other's
• IsZeroSum.nash_payoff_eq — all Nash equilibria yield the same payoff [MSZ 4.44]
• IsConstantSum.nash_payoff_eq — same for constant-sum games [MSZ 4.44–4.45]
• IsZeroSum.expectedPayoff_neg — mixed-strategy lift of IsZeroSum.neg
• IsZeroSum.decidable — IsZeroSum is decidable for finite-strategy games

References

• [MSZ] Maschler, Solan, Zamir, Game Theory, Chapter 4, Sections 4.4–4.6

Definitions

def StrategicGame.IsZeroSum {U : Type u_1} [Add U] [Zero U] (G : StrategicGame (Fin 2) U) : Prop

A two-player game is zero-sum if payoffs sum to zero at every profile. [MSZ 4.39]

Equations

• G.IsZeroSum = ∀ (σ : G.Profile), G.payoff σ 0 + G.payoff σ 1 = 0

def StrategicGame.IsConstantSum {U : Type u_1} [Add U] (G : StrategicGame (Fin 2) U) (c : U) : Prop

A two-player game is constant-sum if payoffs sum to c at every profile.

Equations

• G.IsConstantSum c = ∀ (σ : G.Profile), G.payoff σ 0 + G.payoff σ 1 = c

Zero-sum ↔ constant-sum zero

IsZeroSum and IsConstantSum G 0 unfold to the exact same proposition; the conversion lemmas let later API migrate between the two phrasings. We do not mark them @[simp]: rewriting one definition into another in either direction would just bounce simp between equivalent forms.

theorem StrategicGame.isZeroSum_iff_isConstantSum_zero {U : Type u_1} [Add U] [Zero U] {G : StrategicGame (Fin 2) U} : G.IsZeroSum ↔ G.IsConstantSum 0

IsZeroSum G and IsConstantSum G 0 are the same proposition.

theorem StrategicGame.IsZeroSum.toIsConstantSum {U : Type u_1} [Add U] [Zero U] {G : StrategicGame (Fin 2) U} (hzs : G.IsZeroSum) : G.IsConstantSum 0

A zero-sum game is a constant-sum game with constant 0.

theorem StrategicGame.IsConstantSum.zero_isZeroSum {U : Type u_1} [Add U] [Zero U] {G : StrategicGame (Fin 2) U} (h : G.IsConstantSum 0) : G.IsZeroSum

A constant-sum game whose constant is 0 is zero-sum.

Welfare collapse

welfare (from StrategicGame.Basic) sums payoffs. For two players this is just payoff σ 0 + payoff σ 1, so the zero-sum / constant-sum predicates collapse it directly.

theorem StrategicGame.IsZeroSum.welfare_eq_zero {U : Type u_1} [AddCommMonoid U] {G : StrategicGame (Fin 2) U} (hzs : G.IsZeroSum) (σ : G.Profile) : G.welfare σ = 0

Two-player zero-sum games have zero social welfare at every profile.

theorem StrategicGame.IsConstantSum.welfare_eq {U : Type u_1} [AddCommMonoid U] {G : StrategicGame (Fin 2) U} {c : U} (hcs : G.IsConstantSum c) (σ : G.Profile) : G.welfare σ = c

Two-player constant-sum games have constant social welfare at every profile.

theorem StrategicGame.IsConstantSum.neg {U : Type u_1} [AddCommGroup U] {G : StrategicGame (Fin 2) U} {c : U} (hcs : G.IsConstantSum c) (σ : G.Profile) : G.payoff σ 1 = c - G.payoff σ 0

In a constant-sum game, player 1's payoff is c minus player 0's.

AddCommGroup is needed (not just AddGroup): the RHS uses Sub, which AddGroup defines as c - a = c + -a; matching it to -a + c (the canonical rearrangement of a + b = c) requires commutativity.

theorem StrategicGame.IsZeroSum.neg {U : Type u_1} [AddGroup U] {G : StrategicGame (Fin 2) U} (hzs : G.IsZeroSum) (σ : G.Profile) : G.payoff σ 1 = -G.payoff σ 0

In a zero-sum game, player 1's payoff is the negation of player 0's.

Purely algebraic: holds in any additive group, no order or field needed.

theorem StrategicGame.IsZeroSum.neg' {U : Type u_1} [AddGroup U] {G : StrategicGame (Fin 2) U} (hzs : G.IsZeroSum) (σ : G.Profile) : G.payoff σ 0 = -G.payoff σ 1

In a zero-sum game, player 0's payoff is the negation of player 1's.

Decidability

For a finite-strategy two-player game with decidable equality on payoffs, IsZeroSum is checkable by decide / native_decide. The proof reduces to Fintype.decidableForallFintype on the underlying ∀ σ : G.Profile, … form.

@[implicit_reducible]

instance StrategicGame.IsZeroSum.decidable {U : Type u_1} [Add U] [Zero U] [DecidableEq U] {G : StrategicGame (Fin 2) U} [(i : Fin 2) → Fintype (G.strategy i)] : Decidable G.IsZeroSum

Equations

• StrategicGame.IsZeroSum.decidable = Fintype.decidableForallFintype

Properties over a linearly ordered field

We use [Field U] [LinearOrder U] [IsStrictOrderedRing U] which is the Mathlib replacement for the deprecated [LinearOrderedField U].

Note: The definitions and the lemmas above only need much weaker classes ([Add U] [Zero U], [AddGroup U], [AddCommMonoid U]). The theorems below need more structure for linarith and Nash equilibrium comparisons. See docs/research/zerosum_assumptions.md for a detailed analysis of minimal assumptions per concept.

theorem StrategicGame.IsZeroSum.nash_payoff_eq {U : Type u_1} [Field U] [LinearOrder U] [IsStrictOrderedRing U] {G : StrategicGame (Fin 2) U} (hzs : G.IsZeroSum) {σ τ : G.Profile} (hσ : IsNashEquilibrium G σ) (hτ : IsNashEquilibrium G τ) : G.payoff σ 0 = G.payoff τ 0

In a zero-sum game, all Nash equilibria yield the same payoff for player 0. [MSZ Theorem 4.44-4.45]

theorem StrategicGame.IsZeroSum.nash_payoff_eq_p1 {U : Type u_1} [Field U] [LinearOrder U] [IsStrictOrderedRing U] {G : StrategicGame (Fin 2) U} (hzs : G.IsZeroSum) {σ τ : G.Profile} (hσ : IsNashEquilibrium G σ) (hτ : IsNashEquilibrium G τ) : G.payoff σ 1 = G.payoff τ 1

In a zero-sum game, all Nash equilibria yield the same payoff for player 1.

Constant-sum Nash payoff uniqueness [MSZ 4.44–4.45]

The same argument as IsZeroSum.nash_payoff_eq goes through verbatim: the only use of hzs.neg becomes the constant-sum equation payoff σ 0 + payoff σ 1 = c fed to linarith.

theorem StrategicGame.IsConstantSum.nash_payoff_eq {U : Type u_1} [Field U] [LinearOrder U] [IsStrictOrderedRing U] {G : StrategicGame (Fin 2) U} {c : U} (hcs : G.IsConstantSum c) {σ τ : G.Profile} (hσ : IsNashEquilibrium G σ) (hτ : IsNashEquilibrium G τ) : G.payoff σ 0 = G.payoff τ 0

In a constant-sum game, all Nash equilibria yield the same payoff for player 0. [MSZ Theorem 4.44–4.45]

theorem StrategicGame.IsConstantSum.nash_payoff_eq_p1 {U : Type u_1} [Field U] [LinearOrder U] [IsStrictOrderedRing U] {G : StrategicGame (Fin 2) U} {c : U} (hcs : G.IsConstantSum c) {σ τ : G.Profile} (hσ : IsNashEquilibrium G σ) (hτ : IsNashEquilibrium G τ) : G.payoff σ 1 = G.payoff τ 1

In a constant-sum game, all Nash equilibria yield the same payoff for player 1.

Mixed-strategy lift

The zero-sum property propagates linearly through expected payoff (a finite sum of products of pure payoffs). These let downstream files avoid hand-rolled sum manipulations at every mixed-strategy use site.

theorem StrategicGame.IsZeroSum.expectedPayoff_neg {U : Type u_1} [Field U] [LinearOrder U] [IsStrictOrderedRing U] {G : StrategicGame (Fin 2) U} [(i : Fin 2) → Fintype (G.strategy i)] (hzs : G.IsZeroSum) (p : G.MixedProfile) : G.expectedPayoff p 1 = -G.expectedPayoff p 0

In a zero-sum game, player 1's expected payoff is the negation of player 0's.

theorem StrategicGame.IsZeroSum.expectedPayoff_neg' {U : Type u_1} [Field U] [LinearOrder U] [IsStrictOrderedRing U] {G : StrategicGame (Fin 2) U} [(i : Fin 2) → Fintype (G.strategy i)] (hzs : G.IsZeroSum) (p : G.MixedProfile) : G.expectedPayoff p 0 = -G.expectedPayoff p 1

In a zero-sum game, player 0's expected payoff is the negation of player 1's.

@[simp]

theorem StrategicGame.IsZeroSum.expectedPayoff_add_zero {U : Type u_1} [Field U] [LinearOrder U] [IsStrictOrderedRing U] {G : StrategicGame (Fin 2) U} [(i : Fin 2) → Fintype (G.strategy i)] (hzs : G.IsZeroSum) (p : G.MixedProfile) : G.expectedPayoff p 0 + G.expectedPayoff p 1 = 0

Mixed-strategy version of the zero-sum axiom: expected payoffs sum to 0.