% Copyright 2026 Arthur Freitas Ramos, David Barros Hulak,
% and Ruy J. G. B. de Queiroz. Manuscript source licensed CC BY 4.0.
% https://creativecommons.org/licenses/by/4.0/
\documentclass[11pt]{amsart}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage[a4paper,margin=29mm]{geometry}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{microtype}
\usepackage{needspace}
\usepackage{xurl}
\usepackage[hidelinks]{hyperref}
\hypersetup{pdftitle={A Lean Formalization of the Shapley Value Characterization for Finite Cooperative Games},
pdfauthor={Arthur Freitas Ramos; David Barros Hulak; Ruy J. G. B. de Queiroz},
pdfsubject={Finite cooperative games and the four-axiom Shapley characterization},
pdfkeywords={Shapley value, cooperative games, unanimity games, Mobius inversion, Lean 4, formal verification}}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\newcommand{\R}{\mathbb{R}}
\newcommand{\G}{\mathcal{G}}
\newcommand{\decl}[1]{{\small\nolinkurl{#1}}}
\title[The Shapley characterization in Lean]{A Lean Formalization of the Shapley Value Characterization for Finite Cooperative Games}
\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]{Primary 91A12; Secondary 68V20}
\keywords{Shapley value, transferable utility, cooperative games, axiomatic characterization, unanimity games, M\"obius inversion, Lean 4, Mathlib}
\begin{document}
\begin{abstract}
We describe a Lean 4 formalization of the standard four-axiom characterization
of the Shapley value for finite transferable-utility cooperative games.
Games are arbitrary real-valued characteristic functions normalized at the
empty coalition; the player type may itself be empty. The factorial
coalition formula is proved efficient, symmetric for interchangeable
players, null-player respecting, and additive. Uniqueness follows from
the values of arbitrarily scaled unanimity games and an explicit Boolean-lattice
M\"obius decomposition. The proof requires neither a real-homogeneity axiom
nor a continuity assumption on competing allocation rules. We explain the
finite-sum arguments, the precise Lean statements, the separation between
the registry's challenge and implemented solution, and the historical
verification evidence for the pinned source revision. The contribution is
an auditable exposition of an existing formalization of classical mathematics,
with no claim of new mathematics or formalization priority.
\end{abstract}
\maketitle
\raggedbottom

\section{Context and contribution}

The Shapley value assigns a payoff to each player of a cooperative game
by weighting that player's marginal contributions to coalitions.
Shapley's classical work introduced a value characterized axiomatically
\cite{shapley1953}; subsequent developments and applications are collected
in Roth's edited volume \cite{roth1988}. This paper concerns the standard
modern formulation using efficiency, symmetry, the null-player property,
and additivity. It does not present that quartet as a literal transcription
of the original paper's axiom list.

The subject here is the Lean 4 and Mathlib development
\cite{lean4,mathlib2020,ramos2026} registered as
\href{https://palomar-registry.org/entry?id=PALOMAR-2026-09-25-000008&version=1}{PALOMAR-2026-09-25-000008, version 1}
\cite{palomar2026}. Every source claim refers to commit
\decl{ee15891fecdf294363791c61a5ec018109fe423a}. The registered source
credits Arthur Freitas Ramos as its author and responsible maintainer.
The three-author byline above is the byline of this explanatory manuscript;
it does not change the registered source attribution.

The development has two mathematically substantive parts. First, direct
finite-sum manipulations show that the factorial formula satisfies all four
axioms. In particular, efficiency is established by cancellation of
coalition coefficients, rather than by a formal permutation-average
representation. Second, unanimity games and a Boolean-lattice inversion
formula show that any rule satisfying the axioms has a prescribed value
on every game. The uniqueness proof is careful about the difference
between additivity and real linearity: it determines arbitrary real multiples
of unanimity games directly from the other three axioms.

Our contribution is to make the formal artifact's exact scope, proof
architecture, and evidence boundary accessible without requiring the
reader to infer them from Lean syntax. The mathematical characterization
and inversion method are classical. Neither registration nor the present
exposition establishes a priority claim, independent human review of every
proof term, or an endorsement by the authors of the mathematical sources.

\section{Games and the exact axioms}

Let $N$ be a finite player type with decidable equality, and write $n=|N|$.
Lean expresses these assumptions as \decl{[Fintype N]} and
\decl{[DecidableEq N]}. Coalitions are finite sets of players, represented
by \decl{Finset N}. The grand coalition is \decl{Finset.univ}.

\begin{definition}
A game is a function $v:\mathcal{P}(N)\to\R$ satisfying $v(\varnothing)=0$.
Write $\G(N)$ for the set of these games. Addition and real scalar
multiplication are pointwise.
\end{definition}

The source definition \decl{ShapleyValue.Game} bundles the function with
its normalization proof as a subtype. It does not impose positivity,
monotonicity, superadditivity, convexity, or an assumption that $N$ is
nonempty. Although the game type itself can be defined without a finite
player assumption, the Shapley formula and the characterization use finite
players throughout.

An allocation rule is an arbitrary function
$\psi:\G(N)\to(N\to\R)$. It need not initially be continuous, measurable,
computable, or linear. Its four properties are as follows.

\begin{definition}\label{def:axioms}
The rule $\psi$ is:
\begin{enumerate}
\item \emph{efficient} if $\sum_{i\in N}\psi_i(v)=v(N)$ for every game $v$;
\item \emph{symmetric} if, for every $v$ and $i,j\in N$,
\[
 \bigl[\forall S\subseteq N,\ i,j\notin S\Longrightarrow
 v(S\cup\{i\})=v(S\cup\{j\})\bigr]
 \Longrightarrow \psi_i(v)=\psi_j(v);
\]
\item \emph{null-player respecting} if, for every $v$ and $i$,
\[
 \bigl[\forall S\subseteq N,\ i\notin S\Longrightarrow
 v(S\cup\{i\})=v(S)\bigr]\Longrightarrow \psi_i(v)=0;
\]
\item \emph{additive} if $\psi_i(v+w)=\psi_i(v)+\psi_i(w)$ for all $v,w,i$.
\end{enumerate}
\end{definition}

These are exactly the predicates \decl{Efficient}, \decl{Symmetric},
\decl{NullPlayer}, and \decl{Additive} in the \decl{ShapleyValue} namespace.
Symmetry is a within-game condition on interchangeable players; the
interface does not posit a separate cross-game relabeling axiom.
The null-player property is the zero-marginal condition stated above,
not a separately assumed general dummy-player payment formula.

For $1\leq k\leq n$, define
\begin{equation}\label{eq:weight}
 w_n(k)=\frac{(k-1)!\,(n-k)!}{n!}.
\end{equation}
The Shapley formula implemented in \decl{shapleyValue} is
\begin{equation}\label{eq:shapley}
 \phi_i(v)=\sum_{\substack{S\subseteq N\\i\in S}}
 w_n(|S|)\bigl(v(S)-v(S\setminus\{i\})\bigr).
\end{equation}
Factorials are natural numbers cast to $\R$. The implementation defines
\decl{weight} for every natural $k$ using truncated natural subtraction,
but only $1\leq k\leq n$ occurs in \eqref{eq:shapley}.
The denominator $n!$ is nonzero even when $n=0$.
In the coefficient identities below, $w_n$ denotes this total extension,
including $k=0$ and $k=n+1$.

\begin{theorem}[Registered characterization]\label{thm:main}
For every finite player type $N$ and allocation rule $\psi$,
\[
 \psi\text{ satisfies the four properties in Definition~\ref{def:axioms}}
 \quad\Longleftrightarrow\quad \psi=\phi.
\]
\end{theorem}

The public declaration is
\decl{ShapleyValue.Palomar.shapley_characterization}.
Equality is equality of functions on every game and every player, not
agreement only on a restricted class of games. If $N=\varnothing$, every
payoff vector is the unique empty function, efficiency is $0=v(\varnothing)$,
and the remaining player-indexed conditions are vacuous. The source retains
this case instead of imposing a nonempty-player hypothesis.

\section{The factorial formula satisfies the axioms}

\subsection{Null players and additivity}
If $i$ is null and $i\in S$, apply the null hypothesis to
$S\setminus\{i\}$ to obtain $v(S)=v(S\setminus\{i\})$.
Every summand in \eqref{eq:shapley} is therefore zero.
For additivity, pointwise game addition gives
\[
 (v+w)(S)-(v+w)(S\setminus\{i\})
 =\bigl(v(S)-v(S\setminus\{i\})\bigr)
  +\bigl(w(S)-w(S\setminus\{i\})\bigr).
\]
Distributivity and finite-sum additivity finish the argument.
These are \decl{shapleyValue_nullPlayer} and
\decl{shapleyValue_additive} in \decl{ShapleyValue/Existence.lean}.

\subsection{Symmetry by coalition reindexing}
The insertion--erasure bijection rewrites the formula as
\begin{equation}\label{eq:without}
 \phi_i(v)=\sum_{R\subseteq N\setminus\{i\}}
 w_n(|R|+1)\bigl(v(R\cup\{i\})-v(R)\bigr).
\end{equation}
Suppose $i\ne j$ are interchangeable. Split each sum according to whether
the other player belongs to $R$. Coalitions excluding both players give
equal contributions by the symmetry hypothesis. In the other parts,
write the coalitions as $R\cup\{j\}$ and $R\cup\{i\}$, respectively,
where $R$ excludes both. The common upper coalition is
$R\cup\{i,j\}$, the lower worths are equal, and the weights agree because
the cardinalities agree. Thus $\phi_i(v)=\phi_j(v)$.
The case $i=j$ is immediate.

The Lean proof \decl{shapleyValue_symmetric} follows precisely this split.
Its helper lemmas establish the insertion--erasure bijections as finite-sum
reindexings, including their membership and inverse conditions.

\subsection{Efficiency by weight cancellation}
For $1\leq k<n$, the factorial identities give
\begin{equation}\label{eq:balance}
 k\,w_n(k)=(n-k)\,w_n(k+1).
\end{equation}
When $n>0$, they also give $n\,w_n(n)=1$.
These are the source lemmas \decl{weight_balance} and \decl{weight_top}.

Sum \eqref{eq:shapley} over players and interchange the finite sums.
Each $v(S)$ occurs $|S|$ times as an upper-coalition worth.
For lower-coalition occurrences, set $T=S\setminus\{i\}$, so that
$i\notin T$ and $S=T\cup\{i\}$. There are $n-|T|$ choices of such $i$.
Consequently,
\begin{equation}\label{eq:efficient-sum}
 \sum_{i\in N}\phi_i(v)=
 \sum_{T\subseteq N}
 \bigl[|T|w_n(|T|)-(n-|T|)w_n(|T|+1)\bigr]v(T).
\end{equation}
Every nonempty proper-coalition coefficient vanishes by
\eqref{eq:balance}. The empty-coalition term vanishes by normalization,
regardless of the value of its coefficient. If $n>0$, the grand-coalition
coefficient equals one, giving $v(N)$.
If $n=0$, the only coalition is empty and both sides are zero.

The implementation \decl{shapleyValue_efficient} makes all these boundary
cases explicit. It uses \decl{sum_over_members},
\decl{sum_over_nonmembers}, and \decl{sum_filter_insert} to obtain
\eqref{eq:efficient-sum}, rather than asserting an unproved interchange
or a counting identity. This proves existence of an allocation rule
satisfying the four axioms before uniqueness is invoked.

\section{Unanimity games and uniqueness}

\subsection{Scaled unanimity games without a homogeneity axiom}
For nonempty $T\subseteq N$, the unanimity game $u_T$ is
\[
 u_T(S)=\begin{cases}1,&T\subseteq S,\\0,&T\nsubseteq S.\end{cases}
\]
The Lean definition \decl{unanimityGame} is total on all coalitions:
$u_\varnothing$ is defined to be the zero game, so that normalization
is never violated.

\begin{lemma}\label{lem:unanimity}
If $\psi$ is efficient, symmetric, and null-player respecting, then for
every nonempty $T$, every real $c$, and every player $i$,
\begin{equation}\label{eq:unanimity}
 \psi_i(cu_T)=
 \begin{cases}c/|T|,&i\in T,\\0,&i\notin T.\end{cases}
\end{equation}
\end{lemma}
\begin{proof}
Every player outside $T$ is null in $cu_T$, hence receives zero.
Members of $T$ are interchangeable: for two distinct members and a
coalition excluding both, inserting only one cannot complete $T$.
Their payoffs are therefore equal. Efficiency and $(cu_T)(N)=c$
give $|T|$ times the common payoff equal to $c$. Since $T$ is nonempty,
division by $|T|$ is valid. The argument also covers $c=0$ and $c<0$.
\end{proof}

This is \decl{valueOn_unanimity}. Notably, its assumptions do not include
additivity. It does not infer $\psi(cu_T)=c\psi(u_T)$ from additivity:
such an inference for arbitrary real $c$ would require justification.
Instead, \eqref{eq:unanimity} is established directly for each scaled game.
The later uniqueness proof needs only additivity over a finite sum.

\subsection{Boolean-lattice inversion}
Define the coefficient
\begin{equation}\label{eq:mobius}
 m_v(T)=\sum_{S\subseteq T}(-1)^{|T|-|S|}v(S),
\end{equation}
implemented as \decl{mobiusCoeff}. This is the Boolean-lattice
M\"obius transform; incidence-algebra inversion is treated generally
by Rota \cite{rota1964}.

\begin{lemma}\label{lem:inversion}
For every normalized game $v$ and coalition $Q$,
\begin{equation}\label{eq:pointwise}
 v(Q)=\sum_{\varnothing\ne T\subseteq Q}m_v(T).
\end{equation}
Consequently, as games,
\begin{equation}\label{eq:decomposition}
 v=\sum_{\varnothing\ne T\subseteq N}m_v(T)u_T.
\end{equation}
\end{lemma}
\begin{proof}
Expand the right side of \eqref{eq:pointwise} using \eqref{eq:mobius}
and interchange the two finite sums. For a nonempty $S\subseteq Q$,
its worth $v(S)$ has coefficient
\[
 \sum_{S\subseteq T\subseteq Q}(-1)^{|T|-|S|}
 =\sum_{U\subseteq Q\setminus S}(-1)^{|U|},
\]
using the bijection $T\mapsto T\setminus S$, with inverse
$U\mapsto S\cup U$. This alternating sum is one if $S=Q$ and
zero otherwise. In the latter case $Q\setminus S$ is nonempty,
and the sum vanishes by the binomial identity $(1-1)^{|Q\setminus S|}=0$.
The $S=\varnothing$ term vanishes because $v(\varnothing)=0$.
If $Q$ is empty, the sum in \eqref{eq:pointwise} is empty and the
identity again follows from normalization. Evaluating the right side of
\eqref{eq:decomposition} at $Q$ selects exactly its nonempty subsets,
so \eqref{eq:pointwise} proves equality of games.
\end{proof}

The source isolates the alternating cancellation in \decl{alt_sum_powerset}
and \decl{inner_mobius}. The latter assumes a nonempty $S$, $S\subseteq Q$,
and $S\ne Q$; empty $S$ is handled separately by normalization.
The resulting pointwise and game-level theorems are
\decl{mobius_pointwise} and \decl{mobius_decomposition}.
Thus no coefficient is silently divided by a zero coalition size.

\subsection{Determination of every allocation}
Additivity first implies $\psi_i(0)=0$, since
$\psi_i(0)=\psi_i(0)+\psi_i(0)$. Induction then extends it to any finite
sum; this is \decl{additive_sum}. Apply it to \eqref{eq:decomposition}
and use Lemma~\ref{lem:unanimity} for each summand to obtain
\begin{equation}\label{eq:dividends}
 \psi_i(v)=\sum_{\substack{\varnothing\ne T\subseteq N\\i\in T}}
 \frac{m_v(T)}{|T|}.
\end{equation}
The theorem \decl{value_eq_of_axioms} proves this formula for every
rule satisfying the four properties.

The rule $\phi$ satisfies those properties by Section~3, so it has the
same expression \eqref{eq:dividends}. Any other such $\psi$ therefore
agrees with $\phi$ at every game and player. Function extensionality
gives \decl{shapleyValue_unique}. Its converse, substituting $\psi=\phi$
and collecting the four existence results, proves Theorem~\ref{thm:main}.
This proof uses no continuity axiom and does not assume a real-linear
structure on the competing rule.

\begin{remark}[An illustrative three-player calculation]
Let $N=\{a,b,c\}$ and write $v_{ab}=v(\{a,b\})$, and similarly for
other coalitions. For player $a$, formula \eqref{eq:shapley} reads
\[
 \phi_a(v)=\tfrac{1}{3}v_a+\tfrac{1}{6}(v_{ab}-v_b)
 +\tfrac{1}{6}(v_{ac}-v_c)+\tfrac{1}{3}(v_{abc}-v_{bc}).
\]
Meanwhile \eqref{eq:mobius} gives $m_v(\{a\})=v_a$,
$m_v(\{a,b\})=v_{ab}-v_a-v_b$, and
$m_v(N)=v_{abc}-v_{ab}-v_{ac}-v_{bc}+v_a+v_b+v_c$.
Substitution into \eqref{eq:dividends} gives the same expression.
This calculation illustrates the two representations; it is explanatory
algebra, not an additional registered theorem or source benchmark.
\end{remark}

\section{The formal interface and its evidence boundary}

\subsection{Implementation and challenge}
The substantive source modules have distinct roles:
\begin{itemize}
\item \decl{ShapleyValue/Basic.lean}: games, operations, factorial weight,
the Shapley formula, and the four predicates;
\item \decl{ShapleyValue/Existence.lean}: finite-sum reindexing, weight
cancellation, and the four properties of the formula;
\item \decl{ShapleyValue/Uniqueness.lean}: the additive game structure,
unanimity games, inversion, determination of values, and characterization;
\item \decl{Solution.lean}: the six public wrapper theorems in the
\decl{ShapleyValue.Palomar} namespace.
\end{itemize}
Besides the characterization and uniqueness theorems, the exported wrappers
are \decl{shapleyValue_efficient}, \decl{shapleyValue_symmetric},
\decl{shapleyValue_nullPlayer}, and \decl{shapleyValue_additive}, all
under that namespace.

\decl{Challenge.lean} is a separate specification module. It repeats the
seven compared definitions and six theorem statements, each theorem ending
in an intentional \decl{sorry}. The solution imports the substantive
uniqueness module, not the challenge. Compiling the challenge alone cannot
establish the six results, and its six statement holes must not be
mistaken for holes in the solution proof dependency chain.
The comparator configuration fixes the compared definitions and theorems
and permits only \decl{propext}, \decl{Quot.sound}, and
\decl{Classical.choice} as axioms.

\subsection{Pinned environment and historical verification}
The authoritative \decl{lean-toolchain} selects
\decl{leanprover/lean4:v4.35.0-rc2}, and \decl{lake-manifest.json}
pins Mathlib to \decl{065356127b1dc0016f66b7283ce0ce2c4055aa55},
together with eight transitive packages. Reproduction should preserve
the complete manifest. The README's older reference to Lean 4.33.0 is
inconsistent with this pin and is not the environment used for the
registered verification. The separate local comparator script also has
older-toolchain comments and pins; its compatibility should be checked
before using it for a new replay.

The registry records successful verification on September 24, 2026,
followed by registration on September 25. The official mechanical report
from workflow run \decl{36005001365} was retrieved during manuscript
preparation \cite{verification2026}. It identifies the exact source commit,
challenge and solution hashes, toolchain, dependencies, and permitted
axioms. It reports a successful solution build and acceptance by Lean's
default kernel and by the con-ron and NanoDa kernels. Its status is
\decl{pass}, with no listed errors or warnings. The comparator's
kernel-acceptance statement concerns the solution checked against that
configured challenge surface; it is historical machine-checking evidence,
not a fresh run performed for this manuscript.

The three permitted foundations are propositional extensionality, quotient
soundness, and classical choice. These are standard classical Lean
foundations, not the four economic axioms, which are explicit hypotheses
on $\psi$. A permitted-axiom list bounds what may occur in the checked
proof dependency closure; by itself it does not say that each theorem
uses all three. The pinned \decl{scripts/AxiomAudit.lean} prints axiom
dependencies for twelve declarations, consisting of the six library
theorems and their six wrappers. Its checker requires exact coverage and
rejects axioms outside the configured set. We inspected this audit's
source, but do not claim a new per-declaration axiom execution.

\subsection{Checks performed for this exposition}
Fresh source retrieval on October 1, 2026 checked all 22 repository blobs
against the Git tree at the registered commit. The implementation modules
and solution contain no visible \decl{sorry}, \decl{admit}, or new axiom
declaration in this static inspection. The challenge contains exactly
the six deliberate statement holes described above. Challenge, solution,
manifest, and configuration hashes agree with the official mechanical
report. A separate AI-based review checked the mathematical exposition
against the pinned declarations and proof organization, and the bibliography
against primary-source publication records.

No fresh Lean build, kernel replay, or executed axiom audit was performed
while preparing this manuscript. Static scans cannot replace elaboration
and transitive proof-term checking. The proofs in Sections~3 and 4 are
mathematical explanations of the source architecture, not an alternative
verification system. Likewise, checking a theorem proves a proposition
in the specified definitions; it does not validate an economic application
whose assumptions differ from those definitions.

\section{Scope and preparation provenance}

The formal artifact covers finite normalized real-valued characteristic
functions and the specified four-axiom characterization. It does not
formalize infinite-player games, nontransferable utility, a general
permutation-average theorem, computational complexity, numerical
approximation, or application-specific guarantees for attribution methods.
The Shapley formula and associated constructions are marked
\decl{noncomputable}; finite mathematical sums are not presented here
as an extracted executable implementation.

The pinned source metadata reports AI-assisted proof engineering with
\decl{gpt-6-luna (Codex CLI)}. That historical disclosure concerns the
formal development. This manuscript was prepared with GPT-6.1 assistance
and its text is primarily AI-generated. The submitting contributor reports
some human understanding of its content. These statements do not assert
that every listed manuscript author personally reviewed every proof term.
The independent source and mathematical review and the document checks
have the limited scope stated above.

The Lean repository remains licensed BSD-3-Clause. The CC BY 4.0 license
of this newly written manuscript is separate and does not relicense the
repository. No source-repository change or new registry verification is
implied by preparation of this exposition.

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