% 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={Nash Bargaining Characterization in Lean},pdfauthor={Arthur Freitas Ramos; David Barros Hulak; Ruy J. G. B. de Queiroz},pdfsubject={A source-grounded account of the two-person Nash bargaining characterization},pdfkeywords={Nash bargaining, axiomatic characterization, Lean 4, Mathlib, formal verification}}
\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{\IR}{\operatorname{IR}}
\newcommand{\NP}{\operatorname{NP}}
\newcommand{\swap}{\operatorname{swap}}
\newcommand{\decl}[1]{\mbox{\small\nolinkurl{#1}}}
\newcommand{\source}[2]{\href{https://github.com/Arthur742Ramos/nash-bargaining-lean/blob/0ddaa4bb858fa6fdf78074459eafada5e7938727/#1}{#2}}
\title[Nash bargaining in Lean]{Nash Bargaining Characterization 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]{91A12, 68V20}
\keywords{Nash bargaining, two-person bargaining, compact convex feasible sets, individual rationality, axiomatic characterization, Lean 4, Mathlib}
\begin{document}
\begin{abstract}
We describe a Lean 4 formalization of the classical two-person Nash
bargaining characterization. A bargaining problem consists of a compact
convex subset of the real plane, a feasible disagreement point, and a
feasible outcome strictly improving both utilities. The Nash product is
maximized over the individually rational part of that set. The development
proves existence and uniqueness of the maximizer, verifies Pareto
optimality, symmetry, positive affine invariance, and independence of
irrelevant alternatives, and proves that these four axioms characterize
the maximizer among feasible selection rules. We explain the algebraic
midpoint proof of uniqueness and the normalization argument, including
an explicit small-step tangent bound and a compact symmetric enlargement.
The exposition is tied to an immutable repository snapshot and four
declarations registered in Palomar. Historical registry verification is
distinguished from the source inspection used to prepare this manuscript.
The contribution is a documented formalization of established mathematics;
no new bargaining theorem or formalization-priority claim is made.
\end{abstract}
\maketitle
\raggedbottom

\section{The result and its scope}

Nash's bargaining solution selects a cooperative outcome by maximizing
the product of the players' utility gains above disagreement. His 1950
paper gives an axiomatic justification for this choice \cite{Nash1950}.
The mathematical question is distinct from the existence of a Nash
equilibrium in a noncooperative game: here the input is a feasible utility
set and a disagreement point, and the output is one utility pair.

This article explains the development
\texttt{Arthur742Ramos/nash-bargaining-lean} at commit
\nolinkurl{0ddaa4bb858fa6fdf78074459eafada5e7938727}
\cite{BargainingArtifact}. The selected declarations are registered as
\href{https://palomar-registry.org/entry?id=PALOMAR-2026-09-25-000013\&version=1}{PALOMAR-2026-09-25-000013, version 1}
\cite{PalomarBargaining}. The formalization uses Lean 4 and Mathlib
\cite{Lean4,Mathlib2020}. References to source files below always mean
this pinned snapshot, rather than a moving branch.

The scope is precisely two players with real-valued utilities. Feasible
sets are compact and convex, disagreement is feasible, and a strictly
mutually beneficial outcome exists. No comprehensiveness or downward
closure of the feasible set is assumed. The feasible set may contain
outcomes below disagreement. The theorem concerns a utility-space
selection rule; it does not construct a bargaining protocol, prove
strategic implementation, or supply an executable optimization algorithm.

The formalization's useful content lies in making this domain explicit
and carrying it through both directions of the characterization. Its
proof separates compactness-based attainment from algebraic uniqueness,
and gives a direct real-arithmetic version of the normalization argument.
These are implementation and exposition contributions for a classical
result, not claims of a new solution concept.

\section{Bargaining problems and individual rationality}

\begin{definition}\label{def:problem}
A problem is a pair $P=(S,d)$ such that $S\subseteq\R^2$ is nonempty,
compact, and convex, $d\in S$, and
\begin{equation}\label{eq:strict}
  \exists z\in S,\qquad d_1<z_1\quad\hbox{and}\quad d_2<z_2.
\end{equation}
Write $\mathcal B$ for this class of problems. Its individually rational
part is
\[
  \IR(P)=\{u\in S:d_1\leq u_1,\ d_2\leq u_2\}.
\]
The Nash product and maximizer predicate are
\[
  \NP_d(u)=(u_1-d_1)(u_2-d_2),
\]
\[
  \operatorname{Max}(P,x)\quad\Longleftrightarrow\quad
  x\in\IR(P)\ \hbox{and}\
  \forall y\in\IR(P),\ \NP_d(y)\leq\NP_d(x).
\]
\end{definition}

These definitions translate \decl{NashBargaining.Problem},
\decl{nashProduct}, and \decl{IsNashMaximizer} in
\source{NashBargaining/Basic.lean}{\texttt{Basic.lean}}. The Lean type
bundles the set and point with proofs of all five conditions in
Definition~\ref{def:problem}. The nonempty condition is retained explicitly
although it follows from $d\in S$.

The restriction to $\IR(P)$ is essential. For example, take
$d=(0,0)$ and
$S=\{(t,t):-2\leq t\leq1\}$. The raw product is $t^2$, whose maximum
on $S$ is attained at $(-2,-2)$, whereas its maximum on $\IR(P)$ is
attained at $(1,1)$. Thus a statement about maximization over all of $S$
would misdescribe the formal theorem, even for a compact convex problem
satisfying~\eqref{eq:strict}.

Strict simultaneous improvement ensures that the maximum product is
positive. It excludes the flat zero-product case: on
$S=[0,1]\times\{0\}$ with $d=(0,0)$, every individually rational point
has product zero, so uniqueness fails. A strictly improving point need
not be an interior point of $S$ in the plane. The admissible diagonal
segment in the preceding example already has empty planar interior.

\begin{definition}\label{def:solution}
A solution is a function $F:\mathcal B\to\R^2$ satisfying
$F(S,d)\in S$ for every problem. No individual-rationality condition is
included in the definition of a solution.
\end{definition}

The corresponding Lean type \decl{NashBargaining.Solution} is a subtype
of functions with a feasibility proof. This matters for the converse:
the characterization starts with any feasible rule satisfying the four
axioms, rather than assuming in advance that it selects an individually
rational point.

\section{The four axioms}

The predicates in \texttt{Basic.lean} have the following mathematical
content. Every quantified problem below belongs to $\mathcal B$.

\begin{enumerate}
\item \emph{Pareto optimality.} If $y\in S$ and
$F(P)_1\leq y_1$, $F(P)_2\leq y_2$, then $y=F(P)$.
This rules out weak domination with at least one strict utility gain.

\item \emph{Symmetry.} Define $\swap(u_1,u_2)=(u_2,u_1)$.
If $\swap(S)=S$ and $d_1=d_2$, then $F(P)_1=F(P)_2$.
This is a condition on symmetric problems, not a separately assumed
equivariance law for every permutation of an arbitrary problem.

\item \emph{Positive affine invariance.} For
\[
  A(u)=(a_1u_1+b_1,a_2u_2+b_2),\qquad a_1,a_2>0,
\]
if $Q=(A(S),A(d))$, then $F(Q)=A(F(P))$.
Both the feasible set and disagreement point transform together;
the two scales and translations may be different.

\item \emph{Independence of irrelevant alternatives (IIA).}
If $P=(S,d)$, $Q=(T,d)$, $S\subseteq T$, and $F(Q)\in S$, then
$F(P)=F(Q)$. The smaller problem must remain in $\mathcal B$.
\end{enumerate}

Their conjunction is \decl{NashBargaining.NashAxioms}. In particular,
IIA compares sets at the same disagreement point. It does not assert
invariance under arbitrary changes to disagreement or contraction to
sets outside the specified domain.

\section{The formal theorem interface}

\begin{theorem}\label{thm:main}
For every $P\in\mathcal B$ there exists exactly one $x\in\R^2$ such
that $\operatorname{Max}(P,x)$. If a function $N$ selects a maximizer
for every problem, its induced feasible solution satisfies the four
axioms. Conversely, for every feasible solution $F$ satisfying the
axioms, every $P\in\mathcal B$, and every $x$ with
$\operatorname{Max}(P,x)$, one has $F(P)=x$.
\end{theorem}

The registered namespace is \decl{NashBargaining.Palomar}.
Its four declarations are:
\begin{itemize}
\item \decl{nashMaximizerExists}: $\forall P,\ \exists x,\operatorname{Max}(P,x)$;
\item \decl{nashMaximizerUnique}: any two maximizers for one problem agree;
\item \decl{nashSatisfiesAxioms}: any pointwise maximizer selector satisfies the axioms;
\item \decl{axiomsCharacterizeNash}: an axiomatic feasible rule agrees with any given maximizer.
\end{itemize}
The registered declarations in \source{Solution.lean}{\texttt{Solution.lean}}
are wrappers around implementation theorems in the main namespace.
The existence and uniqueness assertions do not themselves define a
particular selector. Classically, existence permits choosing one for
each problem, and uniqueness makes all such selections extensionally
equal. The axiom-verification theorem is deliberately expressed for an
arbitrary function together with its pointwise maximizer proofs.

\section{Attainment and algebraic uniqueness}

\subsection{Compactness gives a maximum}

For $P=(S,d)$, let
\[
  K=S\cap\{u:d_1\leq u_1\}\cap\{u:d_2\leq u_2\}.
\]
The coordinate half-spaces are closed, so $K$ is compact. It is nonempty
by~\eqref{eq:strict}. The map $u\mapsto\NP_d(u)$ is continuous as a
product of two continuous coordinate differences. The extreme-value
theorem therefore supplies a point of maximum on $K$.

In \source{NashBargaining/Existence.lean}{\texttt{Existence.lean}}, attainment follows
from Mathlib's \decl{IsCompact.exists_isMaxOn} theorem.
The proof then unpacks membership in $K$
into feasibility and the two individual-rationality inequalities.
Convexity is not used in this attainment step, although it remains part
of the input type and is needed for uniqueness and characterization.

\subsection{Positive product and a midpoint identity}

Suppose $x,y$ both maximize. Put
\[
  a=x_1-d_1,\quad b=x_2-d_2,\quad
  c=y_1-d_1,\quad e=y_2-d_2.
\]
The gains are initially nonnegative. Comparing each maximizer with the
other gives $ab=ce=M$. Comparing with the strictly improving witness
gives $M>0$, hence $a,b,c,e>0$.

If $a=c$, cancellation in $ab=ce$ gives $b=e$, so $x=y$. Otherwise,
convexity places $z=(x+y)/2$ in $S$. It is individually rational, with
gains $u=(a+c)/2$, $v=(b+e)/2$. The crucial equality is
\begin{equation}\label{eq:midpoint}
  4c(uv-M)=b(a-c)^2.
\end{equation}
It follows by expanding and substituting $ce=ab$. Its right side is
strictly positive when $a\ne c$, while $4c>0$. Therefore $uv>M$,
contradicting maximality of $x$.

This is the proof in
\source{NashBargaining/Uniqueness.lean}{\texttt{Uniqueness.lean}}.
It expresses strictness through a polynomial identity and positivity,
without introducing logarithms, derivatives, or a strict-concavity
library. The product function is not concave on the entire nonnegative
quadrant; the equal-product relation is a substantive ingredient in
\eqref{eq:midpoint}.

\section{Why maximizer selection satisfies the axioms}

The first theorem of
\source{NashBargaining/Characterization.lean}{\texttt{Characterization.lean}}
proves each conjunct for an arbitrary maximizer selector $N$.
Uniqueness is the common final step.

For Pareto optimality, if $y$ weakly dominates $N(P)$, it is individually
rational and its product is at least that of $N(P)$ by monotonicity of
multiplication on nonnegative gains. Thus $y$ is also a maximizer;
uniqueness gives $y=N(P)$. This argument checks domination by all
feasible points, not merely by an externally restricted Pareto frontier.

On a symmetric problem, swapping $N(P)$ preserves feasibility,
individual rationality, and the product. Swapping every comparison
point shows that the swapped point is again a maximizer. Uniqueness
then forces the two coordinates of $N(P)$ to coincide.

For a positive affine map $A$, direct expansion gives
\begin{equation}\label{eq:scale}
  \NP_{A(d)}(A(u))=a_1a_2\NP_d(u).
\end{equation}
The positive factor preserves the ordering of products, and positive
scales preserve the individual-rationality inequalities. Every point
of $A(S)$ has a preimage in $S$, so $A(N(P))$ is a maximizer for the
transformed problem. Uniqueness identifies it with $N(Q)$.

Finally, in the IIA situation, $N(Q)\in S$ and disagreement is unchanged.
Its larger-set maximality restricts to every individually rational
point in $S$, making it a maximizer for $P$. Uniqueness again proves the
required equality. Neither this argument nor the axiom grants a
contraction that loses the selected point.

\section{The converse via normalization and a bounded enlargement}

We now explain the second theorem of \texttt{Characterization.lean}.
Let $F$ satisfy the four axioms, and fix a maximizer $x$ for $P=(S,d)$.
The positivity argument above yields $x_i-d_i>0$. Define
\begin{equation}\label{eq:normalize}
  \phi(u)=\left(\frac{u_1-d_1}{x_1-d_1},
                   \frac{u_2-d_2}{x_2-d_2}\right),
  \qquad U=\phi(S).
\end{equation}
This positive affine map sends $d$ to $(0,0)$ and $x$ to $(1,1)$.
It preserves compactness and convexity, and the transformed problem
$Q=(U,(0,0))$ remains admissible. By~\eqref{eq:scale}, $(1,1)$ is a
Nash maximizer of $Q$.

\subsection{A tangent bound for every feasible point}

\begin{lemma}\label{lem:tangent}
Every $z\in U$ satisfies $z_1+z_2\leq2$.
\end{lemma}

\begin{proof}
Assume $c=z_1+z_2-2>0$. Set
\[
 K=|(z_1-1)(z_2-1)|,\qquad K_i=|z_i-1|,
\]
and choose the explicit positive number
\begin{equation}\label{eq:small}
 t=\min\left\{\frac12,\frac{c}{2(K+1)},
                 \frac1{2(K_1+1)},\frac1{2(K_2+1)}\right\}.
\end{equation}
The point $w=(1-t)(1,1)+tz$ belongs to $U$ by convexity. The bounds
$tK_i\leq1/2$ show $w_i=1+t(z_i-1)\geq1/2$, so $w$ is
individually rational even if $z$ itself is not. Expanding the product,
\[
  w_1w_2-1=tc+t^2(z_1-1)(z_2-1).
\]
Since $tK\leq c/2$, the right side is at least $tc/2>0$.
This contradicts maximality of $(1,1)$ on the individually rational
part of $U$.
\end{proof}

The source uses nested binary minima to realize~\eqref{eq:small}.
This quantitative argument proves a supporting-line inequality for
\emph{all} of $U$. It is important not to infer the inequality directly
from $z_1z_2\leq1$: that comparison is available only for individually
rational $z$, and even there requires convexity near $(1,1)$ to obtain
the linear bound. The proof avoids a differentiability premise.

\subsection{Constructing an admissible symmetric comparison problem}

The half-space $H=\{u:u_1+u_2\leq2\}$ contains $U$, but is not compact
and is therefore not itself an admissible bargaining set. The source
repairs this by a bounded enlargement. The compact set
\[
  V=U\cup\swap(U)
\]
has upper and lower bounds for both coordinate projections. From any
such bounds $M_1,m_1,M_2,m_2$, set
\[
  B=|M_1|+|m_1|+|M_2|+|m_2|+1\geq1,
  \qquad W=[-B,B]^2\cap H.
\]
The bounds imply $V\subseteq[-B,B]^2$, while
Lemma~\ref{lem:tangent} and its swapped version give $V\subseteq H$.
Consequently $U\subseteq W$.

The set $W$ is compact, convex, and invariant under swapping. It
contains both $(0,0)$ and $(1,1)$, so $R=(W,(0,0))$ is an admissible
problem. Symmetry gives $F(R)=(r,r)$. Feasibility gives $2r\leq2$.
If $r<1$, the point $(1,1)\in W$ would dominate $F(R)$ and Pareto
optimality would force equality, a contradiction. Thus $r=1$ and
\[
  F(R)=(1,1).
\]
Because $U\subseteq W$ and $(1,1)\in U$, IIA gives
$F(Q)=F(R)=(1,1)$. Positive affine invariance then yields
$\phi(F(P))=F(Q)=\phi(x)$. The positive scales make $\phi$ injective,
so $F(P)=x$, completing the converse.

This use of a symmetric box intersected with a half-space is the actual
formal construction. The proof does not require a compact convex hull
of $U\cup\swap(U)$, nor an application of the axioms to an unbounded
half-space. It also explains why individual rationality need not be
postulated for $F$: the axioms determine its output through the
comparison problem.

\section{Source organization and verification evidence}

The implementation is small enough to inspect by module. Definitions
and axiom predicates are in \texttt{NashBargaining/Basic.lean};
attainment is in \texttt{Existence.lean}; midpoint uniqueness is in
\texttt{Uniqueness.lean}; both axiom directions are in
\texttt{Characterization.lean}; and the four registered wrappers are
in \texttt{Solution.lean}. The proof bodies use Mathlib's topology and
convexity interfaces together with real-arithmetic tactics, including
\texttt{ring}, \texttt{linarith}, \texttt{nlinarith},
\texttt{positivity}, and \texttt{field\_simp}.

\texttt{Challenge.lean} repeats the public definitions and the four
target theorem statements, with four deliberate \texttt{sorry} holes.
It is the statement-side challenge, not the implementation proof.
The comparator configuration maps those declarations to
\texttt{Solution.lean}. The inspected implementation files contain
no \texttt{sorry} or \texttt{admit} proof placeholders; this textual
observation is distinct from a kernel check of their complete dependency
closure.

The immutable Palomar record reports the following historical evidence
\cite{PalomarBargaining}:
\begin{itemize}
\item Lean toolchain \texttt{leanprover/lean4:v4.35.0-rc2} and Mathlib
revision \nolinkurl{065356127b1dc0016f66b7283ce0ce2c4055aa55};
\item verification on September 24, 2026, at 20:19:45 UTC, with
\href{https://github.com/PalomarRegistry/PalomarSubmission/actions/runs/36053394619}{workflow run 36053394619};
\item permitted axioms \texttt{propext}, \texttt{Quot.sound}, and
\texttt{Classical.choice}, with external checker entries for
\texttt{nanoda} and \texttt{con-ron};
\item registration on September 25, 2026, and preserved source at
the commit identified in Section 1.
\end{itemize}
The record also reports a neutral editorial outcome with no warnings.
That status is not a claim of journal peer review or an endorsement by
Nash's original publisher.

Preparation of this manuscript involved retrieving and inspecting the
pinned definitions, proof files, comparator configuration, and dependency
metadata, and checking the statement-side and solution-side file hashes
against the registry record. We did not perform a fresh Lean build or
rerun the registry's external checkers for this manuscript. The verification
claim therefore rests on the dated registry evidence, while the present
explanation rests on source inspection. Mathematical validity is relative
to the encoded hypotheses and Lean's foundational assumptions; neither
compilation nor registration certifies a broader economic interpretation.

\section{Authorship disclosure and limitations}

The 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. The pinned
\texttt{formalization.yaml} separately records AI-assisted proof engineering
using \texttt{gpt-6-luna (Codex CLI)}. These are distinct disclosures:
the manuscript-drafting model is not inferred to be the historical
proof-engineering model, and model identity is not verification evidence.

The manuscript and its source are licensed CC BY 4.0. The referenced
Lean repository declares BSD-3-Clause; the manuscript license does not
relicense that code. The registry lists Arthur Freitas Ramos as the
formalization's author and responsible maintainer. The present manuscript's
three-author byline should not be read as an altered registry attribution
or as a statement of undocumented individual contributions.

The development covers neither degenerate problems lacking strictly
positive mutual gains nor bargaining among more than two players.
It establishes no convergence rates, numerical method, equilibrium
implementation, or empirical fairness claim. Its mathematical value is
the explicit, source-traceable verification of the classical characterization
within the stated compact convex two-person model.

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