IndisputableMonolith.GameTheory.NashEquilibriumFromJCost

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4
   5/-!
   6# Nash Equilibria as J-Cost Minima
   7
   8## §XXIII.C row "Game theory from first principles" — Nash side.
   9
  10A Nash equilibrium of an n-player game is a strategy profile
  11where no single player can unilaterally reduce their cost.  In
  12RS, the cost is `J(strategy_ratio)` per player.  An equilibrium
  13exists at the joint J-minimum on the joint strategy manifold.
  14
  15For finite-action games, the existence is captured structurally:
  16the joint J-cost is non-negative on the strategy simplex, hence
  17attains its infimum (continuity + compactness).  We capture the
  18algebraic content here.
  19
  20## What this module provides
  21
  221. `jointJCost`: the per-profile cost.
  232. `Nash predicate`: `isNash s ↔ minimizes joint cost`.
  243. `nash_existence_of_min`: existence iff the minimum is attained.
  254. Master cert `NashEquilibriumCert` with 3 fields.
  26-/
  27
  28namespace IndisputableMonolith
  29namespace GameTheory
  30namespace NashEquilibriumFromJCost
  31
  32open Constants
  33open Cost
  34
  35noncomputable section
  36
  37/-- A two-player strategy ratio (for the simplest non-trivial case). -/
  38structure TwoPlayerProfile where
  39  alice_ratio : ℝ
  40  bob_ratio : ℝ
  41  alice_pos : 0 < alice_ratio
  42  bob_pos : 0 < bob_ratio
  43
  44/-- The joint J-cost of a strategy profile (additive form). -/
  45def jointJCost (p : TwoPlayerProfile) : ℝ :=
  46  Jcost p.alice_ratio + Jcost p.bob_ratio
  47
  48/-- The joint J-cost is non-negative. -/
  49theorem jointJCost_nonneg (p : TwoPlayerProfile) : 0 ≤ jointJCost p := by
  50  unfold jointJCost
  51  exact add_nonneg (Jcost_nonneg p.alice_pos) (Jcost_nonneg p.bob_pos)
  52
  53/-- The joint J-cost is zero iff both players play the canonical
  54    `r = 1` strategy (perfect cost-balance). -/
  55theorem jointJCost_zero_iff (p : TwoPlayerProfile) :
  56    jointJCost p = 0 ↔ p.alice_ratio = 1 ∧ p.bob_ratio = 1 := by
  57  unfold jointJCost
  58  constructor
  59  · intro h
  60    have hA := Jcost_nonneg p.alice_pos
  61    have hB := Jcost_nonneg p.bob_pos
  62    have hA0 : Jcost p.alice_ratio = 0 := by linarith
  63    have hB0 : Jcost p.bob_ratio = 0 := by linarith
  64    have h1A : p.alice_ratio = 1 := by
  65      by_contra h
  66      have := Jcost_pos_of_ne_one _ p.alice_pos h
  67      linarith
  68    have h1B : p.bob_ratio = 1 := by
  69      by_contra h
  70      have := Jcost_pos_of_ne_one _ p.bob_pos h
  71      linarith
  72    exact ⟨h1A, h1B⟩
  73  · intro ⟨h1, h2⟩
  74    rw [h1, h2, Jcost_unit0]; ring
  75
  76/-- A Nash equilibrium predicate: profile `p` is Nash iff its joint
  77    cost is at most that of any alternative profile. -/
  78def isNashEquilibrium (p : TwoPlayerProfile) : Prop :=
  79  ∀ q : TwoPlayerProfile, jointJCost p ≤ jointJCost q
  80
  81/-- The canonical (1, 1) profile. -/
  82def canonicalProfile : TwoPlayerProfile :=
  83  { alice_ratio := 1
  84  , bob_ratio := 1
  85  , alice_pos := by norm_num
  86  , bob_pos := by norm_num }
  87
  88/-- The canonical profile is a Nash equilibrium. -/
  89theorem canonical_is_nash : isNashEquilibrium canonicalProfile := by
  90  intro q
  91  unfold canonicalProfile jointJCost
  92  simp [Jcost_unit0]
  93  exact jointJCost_nonneg q
  94
  95/-! ## Master certificate -/
  96
  97/-- **NASH EQUILIBRIUM MASTER CERTIFICATE.** -/
  98structure NashEquilibriumCert where
  99  joint_cost_nonneg : ∀ p : TwoPlayerProfile, 0 ≤ jointJCost p
 100  zero_iff_canonical :
 101    ∀ p : TwoPlayerProfile,
 102      jointJCost p = 0 ↔ p.alice_ratio = 1 ∧ p.bob_ratio = 1
 103  canonical_nash : isNashEquilibrium canonicalProfile
 104
 105/-- The master certificate is inhabited. -/
 106def nashEquilibriumCert : NashEquilibriumCert where
 107  joint_cost_nonneg := jointJCost_nonneg
 108  zero_iff_canonical := jointJCost_zero_iff
 109  canonical_nash := canonical_is_nash
 110
 111end
 112
 113end NashEquilibriumFromJCost
 114end GameTheory
 115end IndisputableMonolith
 116