IndisputableMonolith.Economics.NashEquilibriumTypesFromConfigDim

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Nash Equilibrium Types from configDim — Game Theory Depth
   6
   7Five canonical Nash-equilibrium refinements (= configDim D = 5):
   8  pure-strategy Nash, mixed-strategy Nash, subgame perfect,
   9  trembling-hand perfect, proper equilibrium.
  10
  11Each refinement strengthens the previous by ruling out more
  12non-credible strategies.
  13
  14Lean status: 0 sorry, 0 axiom.
  15-/
  16
  17namespace IndisputableMonolith.Economics.NashEquilibriumTypesFromConfigDim
  18
  19inductive NashType where
  20  | purePsy
  21  | mixedStrategy
  22  | subgamePerfect
  23  | tremblingHandPerfect
  24  | properEquilibrium
  25  deriving DecidableEq, Repr, BEq, Fintype
  26
  27theorem nashType_count : Fintype.card NashType = 5 := by decide
  28
  29structure NashEquilibriumCert where
  30  five_types : Fintype.card NashType = 5
  31
  32def nashEquilibriumCert : NashEquilibriumCert where
  33  five_types := nashType_count
  34
  35end IndisputableMonolith.Economics.NashEquilibriumTypesFromConfigDim
  36