IndisputableMonolith.Decision.NashEquilibriumFromJCost

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# Nash Equilibrium from J-Cost Minimisation — Tier F Game Theory
   6
   7In RS, every agent minimises its recognition cost J(r) where r is the
   8ratio of its action to the social norm. At Nash equilibrium, no agent
   9can unilaterally reduce its J-cost by deviating.
  10
  11Structural claim: Nash equilibrium = joint J-cost minimum = all agents
  12at r = 1 (recognition cost 0). Any unilateral deviation from r = 1
  13strictly increases J-cost (proved: J is zero only at r = 1, positive
  14elsewhere on ℝ+).
  15
  16This gives a one-paragraph recognition-science proof that Nash equilibria
  17in symmetric games are recognitively stable: the unique zero-cost joint
  18state is the equilibrium.
  19
  20Lean status: 0 sorry, 0 axiom.
  21-/
  22
  23namespace IndisputableMonolith.Decision.NashEquilibriumFromJCost
  24open Cost
  25
  26/-- At joint homeostasis (all agents at r=1), J-cost = 0. -/
  27theorem joint_homeostasis_zero_cost : Jcost 1 = 0 := Jcost_unit0
  28
  29/-- Any unilateral deviation strictly increases J-cost for deviating agent. -/
  30theorem deviation_increases_cost {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
  31    0 < Jcost r := Jcost_pos_of_ne_one r hr hne
  32
  33/-- Nash stability: no agent benefits from unilateral deviation. -/
  34theorem nash_stability_at_homeostasis {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
  35    Jcost 1 < Jcost r := by
  36  rw [Jcost_unit0]; exact Jcost_pos_of_ne_one r hr hne
  37
  38structure NashEquilibriumCert where
  39  homeostasis_optimal : Jcost 1 = 0
  40  deviation_costly : ∀ {r : ℝ}, 0 < r → r ≠ 1 → 0 < Jcost r
  41  stability : ∀ {r : ℝ}, 0 < r → r ≠ 1 → Jcost 1 < Jcost r
  42
  43noncomputable def nashEquilibriumCert : NashEquilibriumCert where
  44  homeostasis_optimal := joint_homeostasis_zero_cost
  45  deviation_costly := deviation_increases_cost
  46  stability := nash_stability_at_homeostasis
  47
  48end IndisputableMonolith.Decision.NashEquilibriumFromJCost
  49