Best responses and checkers

The rational RPS and one-step games have executable best responses and equilibrium checkers connected to correctness proofs. Their verification statements quantify over all admissible rational mixed strategies.

General finite-horizon solvers

The finite-horizon numerical layer implements Fictitious Play, Online Mirror Descent, Prior Descent, MFOMO, and Occupation Measure Inclusion in LeanMFG/Computational/Algorithms/. It supports general finite state and action shapes, time-indexed policies, and population-dependent transition probabilities. These solvers have numerical reference checks; their correctness and convergence proofs are deferred.

Three-action static game

bestResponse compares the three pure-action rewards and chooses a maximum. Ties are resolved Rock, then Paper, then Scissors. exploitability subtracts the population strategy's own reward from the best pure-action reward. checkEpsilonEquilibrium checks nonnegative ε and exploitability at most ε.

One-step finite-state game

bestAction selects a maximizing action at each state. bestResponse assembles these selections into a deterministic policy. The executable exploitability and ε-equilibrium checker evaluate a unilateral policy deviation against the population induced by the candidate policy.

This rational finite-state update is executable and defined in Model. The general numerical iteration solvers are documented above. No convergence or discretization error theorem is claimed for those numerical algorithms.