Mathematics Game Theory Depth From Rs Solution Concept

The five solution concepts

Game theory asks how rational players settle on strategies. Over decades, theorists produced five canonical answers: Nash equilibrium, subgame perfect equilibrium, correlated equilibrium, Bayesian Nash equilibrium, and evolutionarily stable strategy. Each captures a different idea of stability, from no player wanting to change alone, to credibility in sequential play, to resistance against invading mutants. The Recognition Science framework's library, a machine-checked collection of formal theorems, contains a declaration called SolutionConcept, a discrete record of these five named concepts and nothing else.

The declaration is an inductive type, a formal way of saying these five names are the complete list. The library proves a theorem, solutionConceptCount, that the number of concepts is exactly five. This is not a discovery about game theory; it is a bookkeeping fact. The framework's own contribution is to count what game theory already has. Its certificate structure, GameTheoryDepthCert, packages this count as a single object, and a definition, gameTheoryDepthCert, constructs that object from the theorem. The whole file compiles with zero axioms beyond the standard logical ones and zero unfinished proofs.

In Recognition Science, the framework models a game's equilibrium as a state where the cost of recognition, the forced expense of registering events, is zero in each player's field. The prisoner's dilemma becomes a case where mutual defection carries positive social cost, while the stag hunt shows coordination driving cost toward its minimum. These are interpretive glosses on known games, not new results about them. The declaration itself does not define what equilibrium means in game-theoretic terms, does not prove that any game has one, and does not rank the five concepts by importance.

What the declaration establishes is narrower and precise: a formal enumeration. It gives game theory's five standard solution concepts a stable, machine-readable name each, and it proves the count is five. That count matches the conventional list, which is a useful sanity check for the framework's internal dimension claims, but it is not a theorem about the games themselves. The value is in the clean accounting, not in new game-theoretic insight.

inductive SolutionConcept where
  | nash | subgamePerfect | correlated | bayesianNash | evolutionarilyStable
  deriving DecidableEq, Repr, BEq, Fintype

theorem solutionConceptCount : Fintype.card SolutionConcept = 5 := by decide

def gameTheoryDepthCert : GameTheoryDepthCert where
  five_concepts := solutionConceptCount

inductive SolutionConcept where
  | nash | subgamePerfect | correlated | bayesianNash | evolutionarilyStable
  deriving DecidableEq, Repr, BEq, Fintype

What this page does not claim

This declaration does not define the game-theoretic content of any of the five concepts. This declaration does not prove existence or uniqueness of equilibria for any game. This declaration does not rank the five concepts or claim one is more fundamental.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Mathematics/GameTheoryDepthFromRS.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: