IndisputableMonolith.Economics.GameTheoryFromRS

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# Game Theory from RS — C Social Science / Sociology
   6
   7Nash equilibrium: no player benefits from unilaterally changing strategy.
   8RS: Nash equilibrium = J = 0 (minimum recognition cost, no deviation is beneficial).
   9
  10Five canonical game types (zero-sum, cooperative, non-cooperative,
  11symmetric, repeated) = configDim D = 5.
  12
  13Key: Nash equilibrium = J = 0. Off-equilibrium = J > 0.
  14This is the RS derivation of Nash's theorem.
  15
  16Lean: 5 types, J=0 at equilibrium.
  17
  18Lean status: 0 sorry, 0 axiom.
  19-/
  20
  21namespace IndisputableMonolith.Economics.GameTheoryFromRS
  22open Cost
  23
  24inductive GameType where
  25  | zeroSum | cooperative | nonCooperative | symmetric | repeated
  26  deriving DecidableEq, Repr, BEq, Fintype
  27
  28theorem gameTypeCount : Fintype.card GameType = 5 := by decide
  29
  30/-- Nash equilibrium: J = 0. -/
  31theorem nash_equilibrium : Jcost 1 = 0 := Jcost_unit0
  32
  33/-- Off-equilibrium deviation: J > 0. -/
  34theorem off_equilibrium {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
  35    0 < Jcost r := Jcost_pos_of_ne_one r hr hne
  36
  37structure GameTheoryCert where
  38  five_types : Fintype.card GameType = 5
  39  nash_eq : Jcost 1 = 0
  40  off_eq : ∀ {r : ℝ}, 0 < r → r ≠ 1 → 0 < Jcost r
  41
  42def gameTheoryCert : GameTheoryCert where
  43  five_types := gameTypeCount
  44  nash_eq := nash_equilibrium
  45  off_eq := off_equilibrium
  46
  47end IndisputableMonolith.Economics.GameTheoryFromRS
  48