% Copyright 2026 Arthur Freitas Ramos, David Barros Hulak,
% and Ruy J. G. B. de Queiroz. Manuscript source licensed CC BY 4.0.
\documentclass[11pt]{amsart}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage[a4paper,margin=29mm]{geometry}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{microtype}
\usepackage{xurl}
\usepackage[hidelinks]{hyperref}
\hypersetup{pdftitle={Finite Nash Equilibria and Dependent Mixed Strategies in Lean},pdfauthor={Arthur Freitas Ramos; David Barros Hulak; Ruy J. G. B. de Queiroz},pdfsubject={Source-grounded exposition of finite potential games and common-action and dependent-action mixed Nash equilibrium},pdfkeywords={Nash equilibrium, potential games, dependent action types, Brouwer fixed point, Lean 4, Mathlib}}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\newcommand{\R}{\mathbb R}
\newcommand{\NE}{\operatorname{NE}}
\newcommand{\decl}[1]{{\small\nolinkurl{#1}}}
\newcommand{\native}[2]{\href{https://github.com/Arthur742Ramos/nash-equilibrium-lean/blob/6dd83f3b004c0318e52f4c3cb272d909efca321d/#1}{#2}}
\newcommand{\dependent}[2]{\href{https://github.com/Arthur742Ramos/dependent-nash-equilibrium-lean/blob/2f65710af26a24a26660dd1e92d09adf1697a527/#1}{#2}}
\title[Finite Nash equilibria in Lean]{Finite Nash Equilibria and Dependent Mixed Strategies in Lean}
\author{Arthur Freitas Ramos}
\author{David Barros Hulak}
\author{Ruy J. G. B. de Queiroz}
\thanks{Author ORCID identifiers: Arthur Freitas Ramos,
\href{https://orcid.org/0009-0003-3568-0325}{0009-0003-3568-0325}; David Barros Hulak,
\href{https://orcid.org/0009-0002-8056-1774}{0009-0002-8056-1774}; Ruy J. G. B. de Queiroz,
\href{https://orcid.org/0000-0003-1482-0977}{0000-0003-1482-0977}.}
\thanks{Copyright 2026 the authors. Licensed under \href{https://creativecommons.org/licenses/by/4.0/}{Creative Commons Attribution 4.0 International (CC BY 4.0)}.}
\date{October 1, 2026}
\subjclass[2020]{91A10, 91A11, 68V20}
\keywords{finite games, Nash equilibrium, ordinal potential, better-response paths, mixed strategies, dependent types, Brouwer fixed point, Lean 4}
\begin{document}
\begin{abstract}
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.
\end{abstract}
\maketitle
\raggedbottom

\section{The mathematical result and the two artifacts}

Nash's finite-game existence theorem states that every game with finitely
many players, finitely many nonempty action sets, and real payoffs admits
a mixed equilibrium \cite{Nash1950,Nash1951}. A different, more elementary
existence argument applies to finite potential games: maximize a scalar
potential and rule out profitable unilateral deviations. The two arguments
share the equilibrium concept but use different hypotheses and proof tools.

This article gives a consolidated account of two Lean-native artifacts.
The native artifact, \native{README.md}{\texttt{nash-equilibrium-lean}}, is inspected at
commit \nolinkurl{6dd83f3b004c0318e52f4c3cb272d909efca321d}
\cite{NativeArtifact}. It contains the pure potential-game interface and
a common-action mixed layer. The dependent artifact,
\dependent{README.md}{\texttt{dependent-nash-equilibrium-lean}}, is inspected at
commit \nolinkurl{2f65710af26a24a26660dd1e92d09adf1697a527}
\cite{DependentArtifact}. It gives each player its own action type.
All source links in this paper refer to these commits.

The formalization contribution is an explicit game API, a careful separation
of potential predicates, a finite improvement-path interface, and native
mixed-game adapters to fixed-point infrastructure. The mathematics is
classical \cite{PotentialGames}. Earlier formalizations include the
Isabelle/HOL AFP development by the present manuscript's authors
\cite{AFPNash}, and a Ssreflect/Coq library for potential games and
best-response dynamics \cite{Bagnall2017}. The reused Lean development of Lyu and Li already addresses
Scarf, Brouwer, and Nash \cite{LyuLi2026}; its fixed-point proofs are attributed
dependencies here. We do not claim the first formalization of Nash's theorem,
a cross-prover translation, or a machine-checked equivalence with AFP.

The artifacts use Lean 4 and Mathlib \cite{Lean4,Mathlib2020}.
Finite spaces are supplied through \texttt{Fintype} instances, with
\texttt{DecidableEq} on players and on each relevant action type. The mathematical
statements below are readable independently of Lean. Source names identify
where the encoded definitions and proofs can be found; the distinction
between selected registry declarations and additional repository results
is maintained throughout.

\section{Pure games and the order on utilities}

Let $P$ and $A$ be finite types. For each $i\in P$, let $L_i\subseteq A$
be a nonempty finite legal action set. A profile is a function $s:P\to A$;
it is legal if $s_i\in L_i$ for every $i$. Write $s[i\leftarrow a]$ for
the profile changing only player $i$ to $a$. Payoffs are functions
$u_i:A^P\to U$, where $U$ is an ordered utility type.

These data form \decl{NashEquilibrium.Game} in
\native{NashEquilibrium/Basic.lean}{\texttt{Basic.lean}}.
The structure stores payoffs even on illegal profiles, but all equilibrium
comparisons below start from a legal profile and use legal deviations.
The field \decl{nonempty_strategies} supplies a legal action for each player.
No nonemptiness assumption on $P$ is made. If $P$ is empty, its unique
profile is legal and all playerwise comparisons are vacuous.

\begin{definition}\label{def:pure}
For a utility preorder, a pure Nash equilibrium is a legal profile $s$ such
that
\begin{equation}\label{eq:pure}
 \forall i\in P\ \forall a\in L_i,\qquad
 \neg\bigl(u_i(s)<u_i(s[i\leftarrow a])\bigr).
\end{equation}
\end{definition}

This is exactly \decl{IsNash}. For a general preorder, an incomparable
utility is not a strict improvement. Consequently~\eqref{eq:pure} must not
be silently replaced by
$u_i(s[i\leftarrow a])\leq u_i(s)$. The repository defines a best response
using these weak comparisons and proves \decl{isNash_iff_bestResponse}
under a \emph{linear} order on $U$. It also defines dominant actions and
proves that a profile of dominant actions is Nash under a preorder.
The selected potential theorems impose linear orders on both utilities
and potential values, as required by their formal statements.

\section{Potential certificates and finite improvement paths}

Assume $U$ and $V$ are linearly ordered, and let $\Phi:A^P\to V$. The repository keeps the
following predicates separate.

\begin{definition}\label{def:potential}
A \emph{generalized ordinal potential} satisfies, for every legal $s$ and
$a\in L_i$,
\begin{equation}\label{eq:gen}
 u_i(s)<u_i(s[i\leftarrow a])
 \quad\Longrightarrow\quad
 \Phi(s)<\Phi(s[i\leftarrow a]).
\end{equation}
An \emph{ordinal potential} satisfies the same statement with
$\Longleftrightarrow$ in place of $\Longrightarrow$.
\end{definition}

These are \decl{IsGeneralizedOrdinalPotential} and
\decl{IsOrdinalPotential}. The bidirectional condition is the usual strict
sign agreement. In particular, applying it to a deviation and its reverse
rules out a strict potential change along a payoff-neutral deviation.
The one-way condition permits such a change.

\begin{theorem}\label{thm:potential}
Assume that utilities and potential values are linearly ordered.
\begin{enumerate}
\item If $\Phi$ is a generalized ordinal potential, there is a legal profile
$s$ maximizing $\Phi$ over all legal profiles, and this $s$ is Nash.
\item If $\Phi$ is an ordinal potential, a profile is Nash if and only if
it is legal and
$\Phi(s[i\leftarrow a])\leq\Phi(s)$ for all $i$ and $a\in L_i$.
\item For a generalized ordinal potential, there is no nonempty finite
cycle of strict better responses. From every legal starting profile there
is a finite better-response path to a Nash equilibrium, allowing a
zero-step path if the starting profile is already Nash.
\end{enumerate}
\end{theorem}

For the first assertion, the finite set of legal profiles is nonempty:
choose one legal action for each player. A maximum of $\Phi$ exists in
any linear order because the set is finite. A legal strict improvement
would produce a legal profile with larger potential by~\eqref{eq:gen},
contradicting maximality. No real-valued potential is needed.
The proof uses \decl{Finset.exists_max_image}.

The implementation proves this generalized maximizer certificate as
\decl{exists_nash_maximizing_generalized_ordinal_potential}.
The \emph{selected} registry theorem is its standard-ordinal specialization,
\decl{NashEquilibrium.Palomar.exists_nash_maximizing_ordinal_potential},
which returns both equilibrium and global potential maximality.
The selected local-maximum equivalence is
\decl{isNash_iff_potential_local_maximum} in the same namespace.
Its forward implication uses the reverse direction of the ordinal
condition; its backward implication uses~\eqref{eq:gen}.

The stronger hypothesis for the equivalence is necessary. Consider one
player with two actions, constant payoff, and potentials $0$ and $1$.
Every profile is Nash and every potential is generalized, but the action
with potential $0$ is not a local potential maximum. The repository's
\texttt{Examples.lean} contains checked counterexamples illustrating the
potential distinction, alongside Prisoner's Dilemma, coordination,
matching-pennies, and rock-paper-scissors examples.

A better-response edge $s\to t$ consists of legal profiles and a legal
unilateral deviation strictly improving the deviator's utility.
\decl{BetterResponsePath} is inductively generated by one edge and
prefixing an edge to a nonempty path. Each edge strictly increases
$\Phi$; induction and transitivity give $\Phi(s)<\Phi(t)$ along every
such path. A cycle would imply $\Phi(s)<\Phi(s)$.

For reachability, \decl{IsWeaklyAcyclic} explicitly permits either
$t=s$ or a nonempty path from $s$ to a Nash profile $t$.
The proof makes the reversed path relation well founded using finiteness,
transitivity, and irreflexivity. Well-founded induction then chooses a
strictly profitable deviation whenever the current legal profile is not
Nash and concatenates it with the induction hypothesis. The selected
\decl{no_betterResponse_cycle_of_generalized_ordinal_potential} and
\decl{weaklyAcyclic_of_generalized_ordinal_potential} certify these
properties. They specify no scheduling rule, numerical convergence rate,
or equilibrium-computation complexity.

\section{Finite mixed profiles and expected payoffs}\label{sec:mixed}

We now use real payoffs. Let $A_i$ be a finite nonempty action type for
each player $i\in P$, and put $S=\prod_{i\in P}A_i$. The payoff table
is now $u_i:S\to\R$. A mixed profile is
an independent distribution for each player:
\begin{equation}\label{eq:simplex}
 x_i:A_i\to\R,\qquad x_i(a)\geq0,\qquad
 \sum_{a\in A_i}x_i(a)=1.
\end{equation}
Write $K=\prod_i\Delta(A_i)$ for the feasible set.

The native mixed layer takes a \emph{common} type $A$ and represents
profiles as functions $P\to(A\to\R)$. Unlike the native pure \decl{Game}, its
\decl{MixedGame} has no legal-set field: every player may choose every
$a\in A$. The dependent layer represents a profile as
$(i:P)\to(A_i\to\R)$, using a family of action types indexed by players.
The definitions that follow have the same finite-sum form in both layers.

For a pure profile $s\in S$, define the opponents' weight
\[
 W_i(x,s)=\prod_{j\in P\setminus\{i\}}x_j(s_j).
\]
The source enumerates full pure profiles while fixing the deviator's
coordinate:
\begin{align}
 D_i(x,a)&=\sum_{s\in S}\mathbf 1_{\{s_i=a\}}\,
                         W_i(x,s)\,u_i(s),\label{eq:deviation}\\
 U_i(x)&=\sum_{a\in A_i}x_i(a)D_i(x,a).\label{eq:payoff}
\end{align}
These are \decl{opponentWeight}, \decl{pureDeviationPayoff}, and
\decl{mixedPayoff} in the native
\native{NashEquilibrium/Mixed.lean}{\texttt{Mixed.lean}} and dependent
\dependent{DependentNash/Basic.lean}{\texttt{Basic.lean}} modules.
The indicator in~\eqref{eq:deviation} ensures each opponents' profile is
counted once, rather than once per action of player $i$.

\begin{definition}\label{def:mixed}
A mixed Nash equilibrium is $x\in K$ such that
\begin{equation}\label{eq:mixed}
 \forall i\in P\ \forall a\in A_i,\qquad D_i(x,a)\leq U_i(x).
\end{equation}
\end{definition}

The predicate \decl{IsMixedNash} includes feasibility as well as these
inequalities. This finite pure-deviation formulation excludes an improving
mixed deviation as well: for any distribution $y_i$,
$\sum_a y_i(a)D_i(x,a)\leq\sum_a y_i(a)U_i(x)=U_i(x)$.
This is an elementary explanation of the definition; it is not a separate
selected arbitrary-mixed-deviation equivalence theorem.

\begin{theorem}\label{thm:support}
If $x$ is a mixed Nash equilibrium and $x_i(a)>0$, then
$D_i(x,a)=U_i(x)$. In particular, if $D_i(x,a)<U_i(x)$, then $x_i(a)=0$.
\end{theorem}

\begin{proof}
Each summand $x_i(b)(U_i(x)-D_i(x,b))$ is nonnegative by
\eqref{eq:simplex} and~\eqref{eq:mixed}, and
\[
 \sum_b x_i(b)(U_i(x)-D_i(x,b))
 =U_i(x)\sum_bx_i(b)-U_i(x)=0.
\]
Every summand is therefore zero. For $b=a$, the positive factor $x_i(a)$
can be cancelled. The second assertion follows by contradiction from
the first and nonnegativity of probabilities.
\end{proof}

Both selected \decl{mixedNash_support_payoff_eq} theorems implement this
argument. They need no additional global nonemptiness assumption on
action types: the equilibrium hypothesis already supplies the relevant
normalization. Equalization applies only to positive-probability actions;
an unused action may tie the equilibrium payoff or have a lower payoff.

For a pure profile $s$, its Dirac embedding assigns probability one to
$s_i$ and zero to every other action. The source proves
\[
 D_i(\delta_s,a)=u_i(s[i\leftarrow a]),\qquad U_i(\delta_s)=u_i(s).
\]
Products of Dirac weights eliminate all opponents' profiles except the
one agreeing with $s$, and the finite sum reduces to a single term.
Thus the condition of no profitable pure deviation yields a mixed
Dirac equilibrium. These identities are additional library lemmas,
not separately selected registry declarations. For the common-action
mixed game they compare against \emph{every} common action; a restricted
pure-game equilibrium is not automatically an equilibrium of that game.

\section{The normalized payoff-excess map}

For an arbitrary real coordinate profile $x$, define
\begin{equation}\label{eq:excess}
 e_i(x,a)=\max\{0,D_i(x,a)-U_i(x)\},\qquad
 E_i(x)=\sum_{a\in A_i}e_i(x,a),
\end{equation}
and
\begin{equation}\label{eq:map}
 F(x)_i(a)=\frac{x_i(a)+e_i(x,a)}{1+E_i(x)}.
\end{equation}
The source names are \decl{excess}, \decl{excessSum}, and \decl{nashMap}.
Because $E_i(x)\geq0$ for every $x$, the denominator is strictly positive
on the entire ambient space, not just on $K$.

If $x\in K$, the numerator is nonnegative and
\[
 \sum_a F(x)_i(a)
 =\frac{\sum_a x_i(a)+\sum_a e_i(x,a)}{1+E_i(x)}=1.
\]
Hence $F(K)\subseteq K$, as proved by \decl{nashMap_isMixedProfile}.
The decisive algebraic step is the following.

\begin{lemma}\label{lem:fixed}
If $x\in K$ and $F(x)=x$, then all excesses are zero, and $x$ is a
mixed Nash equilibrium.
\end{lemma}

\begin{proof}
Fix a player $i$ and abbreviate $T=E_i(x)$. Multiplying a fixed-point
coordinate identity by $1+T$ yields
\begin{equation}\label{eq:fp}
 e_i(x,a)=x_i(a)T\qquad\text{for every }a\in A_i.
\end{equation}
If $T=0$, every excess is zero. Suppose instead $T>0$.
Whenever $x_i(a)>0$, equation~\eqref{eq:fp} makes the excess positive,
so the maximum in~\eqref{eq:excess} is its second argument and
\[
 D_i(x,a)=U_i(x)+x_i(a)T.
\]
For zero-probability actions, multiplying by $x_i(a)$ makes the
corresponding identity hold as well. Summing therefore gives
\[
 U_i(x)=\sum_a x_i(a)D_i(x,a)
       =U_i(x)\sum_a x_i(a)+T\sum_a x_i(a)^2,
\]
so $T\sum_a x_i(a)^2=0$. Normalization ensures some $x_i(a)>0$;
thus $\sum_a x_i(a)^2>0$, contradicting $T>0$.
It follows that $T=0$ and each $D_i(x,a)-U_i(x)\leq0$.
Applying this to every player gives~\eqref{eq:mixed}.
\end{proof}

This sum-of-squares proof follows \decl{fixedPoint_excess_zero}, followed
by \decl{mixedNash_of_nashMap_fixedPoint}, in both mixed modules.
It does not infer equilibrium merely from nonnegativity of total excess,
nor cancel a probability that might be zero. Conversely, an equilibrium
has zero excess by definition and hence is fixed by~\eqref{eq:map}; the
existence proof uses the forward implication of Lemma~\ref{lem:fixed}.

\section{Geometry and the proved fixed-point dependency}

\subsection{Finite-dimensional topology}

The feasible set $K$ is closed: it is the intersection of coordinate
half-spaces $x_i(a)\geq0$ and normalization hyperplanes
$\sum_a x_i(a)=1$. Every feasible coordinate is at most one, since it
is a nonnegative summand of a sum equal to one. Hence
\[
 K\subseteq\prod_{i\in P}\prod_{a\in A_i}[0,1].
\]
The finite product box is compact, and the closed subset $K$ is compact.
Convexity follows directly from~\eqref{eq:simplex}: a convex combination
preserves nonnegativity and normalization. Nonemptiness is witnessed by
the uniform distributions $x_i(a)=1/|A_i|$ when each $A_i$ is nonempty.

These facts are proved as \decl{mixedProfiles_closed},
\decl{mixedProfiles_compact}, \decl{mixedProfiles_convex}, and
\decl{mixedProfiles_nonempty} in the native \texttt{MixedTopology.lean}
and dependent \texttt{Topology.lean}. Their proofs use finite sums,
coordinate evaluations, compact interval products, and closedness.
Payoffs are arbitrary lookup values on a finite pure-profile space;
no continuity assumption on the payoff table is necessary.

Each $D_i(x,a)$ is a finite sum of finite products of coordinates with
fixed real coefficients. The functions $D_i$, $U_i$, $e_i$, and $E_i$
are therefore continuous. Division in~\eqref{eq:map} is continuous
because the denominator never vanishes. The two modules prove
\decl{continuous_nashMap} on the full ambient real coordinate space.
Their conditional fixed-point reduction accepts a supplied fixed point;
it does not postulate that such a point exists.

\subsection{The Brouwer bridge}

\begin{theorem}\label{thm:existence}
Every finite real-payoff game with a nonempty action type for each player
has a mixed Nash equilibrium. The common-action version assumes one
finite nonempty type available to every player. Neither version requires
the player type to be nonempty.
\end{theorem}

The existence modules use the theorem \decl{Brouwer_Product} from
\nolinkurl{Gametheory/Brouwer_product.lean}. Its interface concerns a
continuous self-map of
\[
 \prod_{k\in\operatorname{Fin}(n)}\Delta(\operatorname{Fin}(c_k)),
 \qquad c_k\in\mathbb N_{>0}.
\]
For this interface the finite player index type is inhabited, so $n>0$.
It returns a fixed point. The imported Scarf-to-Brouwer development is
\emph{proved source}, not a new fixed-point axiom introduced by either
Nash library. The four included \texttt{Gametheory} files are attributed
to the MIT-licensed \texttt{math-xmum/Brouwer} development at commit
\nolinkurl{09941e849a81e520cc0cc53220f10f8e5f4768e0}
\cite{BrouwerSource,LyuLi2026}. The native copies are unchanged from that pin; the dependent copy of
\texttt{Scarf.lean} narrows its opening imports while retaining the proof
body. This paper does not rederive or claim those upstream fixed-point proofs.

For nonempty $P$, choose a finite equivalence
$\pi:P\simeq\operatorname{Fin}(|P|)$. In the common-action bridge,
choose $A\simeq\operatorname{Fin}(|A|)$ and set $c_k=|A|$ for every
$k$. In the dependent bridge, set
\[
 c_k=|A_{\pi^{-1}(k)}|,\qquad
 \eta_k:A_{\pi^{-1}(k)}\simeq\operatorname{Fin}(c_k).
\]
Nonempty action types ensure $c_k>0$. Reindexing the probability
coordinates identifies feasible game profiles with this product of
standard simplices. The normalized map transports to a continuous
self-map of the product using the feasibility and continuity lemmas.
The theorem \decl{Brouwer_Product} supplies a fixed point, which is
transported back and converted into equilibrium by
Lemma~\ref{lem:fixed}.

The dependent implementation must also transport actions along
$\pi^{-1}(\pi(i))=i$. These casts appear in its playerwise equivalence
\decl{eMPlayer}; the fixed-point calculation uses heterogeneous equality
to reconcile coordinates whose action types have propositionally equal
indices. This is a type-correct reindexing issue, not an additional
mathematical assumption or the addition of dummy actions.

If $P$ is empty, the existence modules construct the unique empty
profile directly; feasibility and fixed-point equality are vacuous.
They do not invoke a product theorem requiring an inhabited finite
index type in that branch. The native theorem nevertheless retains its
stated \decl{Nonempty Move} hypothesis. The dependent assumption
$\forall i,\ A_i\ne\varnothing$ is vacuous for empty $P$.

The direct existence proofs in
\native{NashEquilibrium/MixedBrouwer.lean}{\texttt{MixedBrouwer.lean}} and
\dependent{DependentNash/Existence.lean}{\texttt{Existence.lean}}
use the simplex-product bridge, continuity, and preservation. The
separate compactness and convexity lemmas document the expected geometry;
the final proof does not apply an abstract compact-convex fixed-point
axiom to them.

\section{An additional restricted-action interface}\label{sec:restricted}

The dependent repository also contains
\dependent{DependentNash/Restricted.lean}{\texttt{Restricted.lean}}.
Given an ambient finite type $A$, legal finite sets $L_i\subseteq A$,
and an ambient payoff table, it defines
\[
 A_i=\{a:A\mid a\in L_i\}
\]
and restricts payoffs by forgetting each subtype membership proof.
Nonempty legal sets make these dependent types nonempty, so
\decl{exists_mixedNash_restricted} applies
Theorem~\ref{thm:existence} to the restricted game. No padding with
unavailable or dummy actions is used.

For a dependent pure profile $s$, let $\bar s$ be its ambient image.
The file proves that forgetting subtype proofs commutes with unilateral
deviation, then establishes
\begin{equation}\label{eq:restricted}
 \delta_s\text{ is mixed Nash in the restricted game}
 \quad\Longleftrightarrow\quad
 \forall i\ \forall a\in L_i,\quad
 u_i(\bar s[i\leftarrow a])\leq u_i(\bar s).
\end{equation}
This is \decl{restricted_dirac_mixed_nash_iff}. Its proof uses the Dirac
payoff identities from the mixed layer of Section~\ref{sec:mixed}.

The exact scope matters: equation~\eqref{eq:restricted} is a
Dirac-profile and pure-deviation correspondence. The file does not
construct an equivalence between arbitrary ambient mixed profiles and
dependent mixed profiles. These restricted-action results are additional
repository results, are not imported by the selected
\texttt{Solution.lean}, and are not selected by the dependent entry's
comparator. Their exposition here must not be read as expanding that
entry's verified comparison surface.

\section{Selected declarations and historical verification}

The native registration is
\href{https://palomar-registry.org/entry?id=PALOMAR-2026-09-07-000009\&version=1}{PALOMAR-2026-09-07-000009, version 1}
\cite{PalomarNative}. In the namespace \decl{NashEquilibrium.Palomar},
its six selected theorems are:
\begin{itemize}
\item \decl{exists_nash_maximizing_ordinal_potential};
\item \decl{isNash_iff_potential_local_maximum};
\item \decl{no_betterResponse_cycle_of_generalized_ordinal_potential};
\item \decl{weaklyAcyclic_of_generalized_ordinal_potential};
\item \decl{mixedNash_support_payoff_eq};
\item \decl{exists_mixedNash}.
\end{itemize}
The dependent registration is
\href{https://palomar-registry.org/entry?id=PALOMAR-2026-09-07-000014\&version=1}{PALOMAR-2026-09-07-000014, version 1}
\cite{PalomarDependent}. Its selected namespace is
\decl{DependentNash.Palomar}, and its two theorems are
\decl{exists_mixedNash} and \decl{mixedNash_support_payoff_eq}.
The wrappers in each \texttt{Solution.lean} delegate to implementation
theorems; \texttt{comparator.json} identifies the statement-side and
solution-side declarations and the selected definitions.

The two records report the same Lean toolchain,
\texttt{leanprover/lean4:v4.33.0}, and Mathlib revision
\nolinkurl{db584cd6d46c92f209a44c0f1c829460d327499d}.
For the native entry, the recorded verification time is September 7,
2026, at 13:45:01 UTC, with
\href{https://github.com/PalomarRegistry/PalomarSubmission/actions/runs/34128531761}{workflow run 34128531761}.
For the dependent entry, it is September 7, 2026, at 20:52:40 UTC, with
\href{https://github.com/PalomarRegistry/PalomarSubmission/actions/runs/34160743338}{workflow run 34160743338}.
Both permit only \texttt{propext}, \texttt{Quot.sound}, and
\texttt{Classical.choice} in the selected theorem axiom audit.
The records include an external \texttt{nanoda} checker revision.
These dated records are evidence about the configured declarations;
registration is not a claim of journal peer review.

The native \texttt{Challenge.lean} contains two deliberate statement-side
\texttt{sorry} holes, for weak acyclicity and mixed existence; the other
selected targets, including support equalization, are proved there directly. The dependent
challenge has two deliberate holes. The corresponding proofs are in the
implementation and \texttt{Solution.lean}; the challenge files are not
being presented as complete proof implementations. The inspected
implementation modules and solution files contain no \texttt{sorry} or
\texttt{admit} placeholders. Textual inspection alone is not a fresh
kernel verification of the complete import closure.

Preparation of this manuscript included inspecting the pinned definitions,
proof bodies, comparator configurations, and dependency metadata. The
retrieved source files match their pinned Git blob identifiers, and the
\texttt{Challenge.lean} and \texttt{Solution.lean} SHA-256 hashes match
both immutable registry records. No new Lean build or rerun of the
external checker was performed for this manuscript. Its mechanical
verification claims refer to the dated records; its explanatory claims
are grounded in source inspection. The dependent record's warning about
restricted-action scope is addressed by the explicit separation in
Section~\ref{sec:restricted}.

\section{Authorship disclosure and limitations}

This manuscript was primarily drafted with GPT 6.1 under the authors'
direction. The submitting author reports understanding some parts of the
work. This disclosure does not claim a complete independent human
reconstruction or line-by-line human validation of every formal proof.
Both pinned \texttt{formalization.yaml} files separately record
\texttt{GPT-5 Codex} assistance with historical proof engineering.
The manuscript model is not inferred to be the historical proof model,
and model identity is not verification evidence.

The manuscript and its source are licensed CC BY 4.0. Both Lean projects
declare BSD-3-Clause; the included fixed-point source retains its MIT
notice. The manuscript license does not relicense those artifacts.
The two registry entries list Arthur Freitas Ramos as formalization
author and responsible maintainer. The present three-author manuscript
byline does not alter that attribution or assert undocumented individual
contributions.

The results concern finite strategic-form games, pure potential games,
and independently mixed real-payoff games under the stated action
hypotheses. They do not establish an equilibrium-selection procedure,
uniqueness, computable approximation bounds, infinite-game existence,
correlated-equilibrium results, or an economic interpretation beyond
the encoded payoff model. The artifact's value is its explicit separation
of hypotheses, source-traceable proof interfaces, and reusable bridge
between native game definitions and proved fixed-point infrastructure.

\bibliographystyle{plain}
{\raggedright\bibliography{references}}
\end{document}