Discrete Game Theory🔗

This is a formalization of game theory fundamentals in Lean 4, without real numbers, probability, or fixed-point theorems. Nash equilibria are computed by a terminating descent algorithm on finite face lattices.

The key ideas:

• Games record ordinal preferences — which action is better, not by how much.

• The probabilistic simplex of strategies is replaced by a discrete version. A face of the simplex (nonempty subset of vertices) replaces probability distributions as the notion of mixed strategy.

• Instead of using expected utility, preferences between faces are defined conservatively: A dominates B only when every action in A beats every action in B against every consistent opponent play. This produces a partial preference order on mixed strategies for each player.

• Nash equilibrium existence follows from a terminating descent algorithm that starts considering the mixture of all actions and eliminates dominated actions.

• The algorithm is not only provably terminating but directly executable: a computable findNash runs the descent and returns a concrete Nash profile on any finite game, ready for #eval.