math.LO — Logic
Finite Nash Equilibria and Dependent Mixed Strategies in Lean
We present two complementary Lean 4 developments of finite Nash equilibrium. The pure-game layer uses player-specific legal action sets, distinguishes one-way generalized ordinal potentials from bidirectional ordinal potentials, and proves potential-maximizer certificates, a local-maximum characterization, absence of strict-improvement cycles, and weak acyclicity. The mixed-game layers use either a common finite action type or a dependent finite action type for each player. They prove payoff equalization on equilibrium supports, Dirac payoff identities, continuity of the normalized payoff-excess map, and mixed equilibrium existence. We explain the finite-sum and sum-of-squares arguments and the reindexing bridge to an attributed, proved product-of-simplices Brouwer theorem. An additional legal-subtype interface is separated from the declarations selected by the registry comparator. The account is tied to two immutable source snapshots and dated verification records. It documents established mathematics and its formal interfaces, without claiming a new equilibrium theorem or formalization priority.