% Copyright (c) 2026 Arthur Freitas Ramos, David Barros Hulak,
% and Ruy J. G. B. de Queiroz.
% Manuscript and source licensed CC BY 4.0:
% https://creativecommons.org/licenses/by/4.0/
\documentclass[11pt]{amsart}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage[a4paper,margin=26mm]{geometry}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{microtype}
\usepackage{xurl}
\usepackage[hidelinks]{hyperref}
\hypersetup{pdftitle={Finite VCG and Groves Payments in Lean},
 pdfauthor={Arthur Freitas Ramos; David Barros Hulak; Ruy J. G. B. de Queiroz},
 pdfsubject={An exposition of finite Clarke pivot mechanisms and a Groves payment characterization},
 pdfkeywords={VCG, Clarke pivot, Groves payments, Green-Laffont, Lean 4, formalization}}
\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{\V}{\mathcal{V}}
\newcommand{\decl}[1]{\texttt{\detokenize{#1}}}
\newcommand{\source}[2]{\href{https://github.com/Arthur742Ramos/vcg-mechanism-lean/blob/aad0c41b99053cf4657d91f7446279557f87ae18/#1}{#2}}
\title[Finite VCG and Groves payments]{Finite VCG and Groves Payments 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{September 30, 2026}
\subjclass[2020]{91B26, 68V20}
\keywords{VCG mechanism, Clarke pivot payments, Groves characterization,
dominant strategies, Lean 4, formal verification}
\begin{document}
\begin{abstract}
We describe a Lean 4 development of finite direct mechanisms with
quasi-linear utility and unrestricted real-valued valuations. The Clarke
pivot mechanism selects a reported-welfare maximizer and charges each
agent the loss in other-agent welfare relative to its maximum over the
same fixed alternative set. The development proves efficiency,
dominant-strategy truthfulness, nonnegative payments and no deficit, and
individual rationality under the explicit assumption that every valuation
is nonnegative. It also proves that every efficient, dominant-strategy
incentive-compatible mechanism on the full valuation domain has Groves-form
payments, with a term independent of the paying agent's report. We explain
the finite-maximization interface, the report-update invariants, and the
characterization argument using outcome-forcing reports and positive
perturbations. The exposition is tied to a specific source revision and
separates proved implementations from statement-only comparator
placeholders. These are classical mechanism-design results; no new
mathematical theorem or formalization-priority claim is made.
\end{abstract}
\maketitle
\raggedbottom
\emergencystretch=2em

\section{Scope and context}

The Vickrey--Clarke--Groves tradition connects efficient allocation to
truthful reporting through quasi-linear payments. Vickrey's auction
analysis, Clarke's public-goods pivot rule, and Groves' more general payment
scheme provide the classical context \cite{Vickrey1961,Clarke1971,Groves1973}.
Characterization results associated with Green and Laffont and with
Holmstr\"om explain when efficient, strategy-proof mechanisms must have
Groves form \cite{GreenLaffont1977,Holmstrom1979}. This paper explains one
finite, unrestricted-domain Lean development of these ideas. It does not
claim to reproduce every domain or participation assumption in those
original papers.

All implementation descriptions refer to revision
\nolinkurl{aad0c41b99053cf4657d91f7446279557f87ae18} of
\emph{vcg-mechanism-lean} \cite{VCGArtifact}. The repository's public interface
contains four results about its Clarke pivot mechanism and a general
Groves-payment necessity theorem. The latter is named
\decl{VCG.vcg_greenLaffont}. Our presentation states its exact finite-domain
meaning before explaining the proof. The source fixes Lean
\texttt{v4.35.0-rc2}; the Mathlib dependency uses the same release tag and
resolves to revision
\nolinkurl{065356127b1dc0016f66b7283ce0ce2c4055aa55}.
Mathlib supplies real arithmetic, finite sums, finite maximization, and
supporting tactics \cite{Mathlib2020}.

The contribution of this note is an inspectable correspondence between the
mathematics and the artifact: the sign convention for payments, the exact
individual-rationality hypothesis, the full report domain used in the
characterization, and the separation between a proof implementation and a
statement-only challenge. The mathematical arguments are classical. We
make no assertion that this is the first formalization of any result.

There is prior machine-checked VCG work. The Isabelle Archive of Formal
Proofs entry by Caminati, Kerber, Lange, and Rowat formalizes combinatorial
VCG auctions, including well-defined allocation and pricing and
nonnegative prices \cite{AFP2015}. Barthe and coauthors verify generic VCG
truthfulness using relational refinement types \cite{Barthe2016}. These
developments use different formal systems and models. They provide
relevant context for the supporting VCG properties; we do not claim that
they prove the particular Groves-form necessity theorem discussed here.

\section{The finite direct-mechanism model}

Let $N$ be a finite nonempty set of agents and $A$ a finite nonempty set of
alternatives. We work under \decl{Fintype}, \decl{Nonempty}, and
\decl{DecidableEq} assumptions for both types, as explicitly stated in
the comparator theorems of \decl{Challenge.lean}. A profile is a function
\[
  v\in\V:=\R^{N\times A},\qquad v_i(a)=v(i,a).
\]
Every real-valued report is allowed by \decl{VCG.Valuation}. There is no
sign restriction in this profile type. Nonnegative valuations enter only
as an additional hypothesis of the individual-rationality theorem.

For $a\in A$, define total and other-agent welfare by
\begin{equation}\label{eq:welfare}
  W(v,a)=\sum_{j\in N}v_j(a),\qquad
  S_i(v,a)=\sum_{j\in N\setminus\{i\}}v_j(a).
\end{equation}
Thus $W(v,a)=v_i(a)+S_i(v,a)$. The definitions
\decl{VCG.welfare} and \decl{VCG.othersWelfare} use sums over
\decl{Finset.univ} and \decl{Finset.univ.erase i}, respectively. The finite
sum identity is the bridge between an individual utility expression and
an objective involving all agents.

A deterministic direct mechanism is a pair
\[
  x:\V\longrightarrow A,\qquad p:\V\longrightarrow\R^N.
\]
The quantity $p_i(v)$ is a charge paid by agent $i$ to the mechanism. Under
true valuation $t_i$ and submitted profile $w$, that agent's quasi-linear
utility is
\begin{equation}\label{eq:trueutility}
  U_i(t_i;w)=t_i(x(w))-p_i(w).
\end{equation}
No income constraint, nonlinear money preference, implementation cost, or
outside option is represented.

Write $v[i\leftarrow r]$ for the profile obtained by replacing only agent
$i$'s report with $r:A\to\R$. This is \decl{Function.update v i r} in the
source. The general mechanism is \emph{efficient} if
\begin{equation}\label{eq:eff}
  W(v,a)\le W(v,x(v))\qquad(v\in\V,\ a\in A),
\end{equation}
and \emph{dominant-strategy incentive compatible} (DSIC) if
\begin{equation}\label{eq:dsic}
  v_i\bigl(x(v[i\leftarrow r])\bigr)-p_i(v[i\leftarrow r])
    \le v_i(x(v))-p_i(v)
\end{equation}
for every $v,i,r$. In this inequality, $v_i$ is the true valuation of the
agent whose report changes. The components $v_j$ for $j\ne i$ may be any
fixed reports. Their numerical values enter the mechanism, but the
agent's true utility uses only its own true valuation.

\section{Clarke pivot allocation and payments}

Because $A$ is finite and nonempty, a maximum of $W(v,\cdot)$ exists. The
artifact chooses an alternative $x^*(v)$ with
\[
  W(v,a)\le W(v,x^*(v))\quad\hbox{for every }a\in A.
\]
It also defines the attained maximum
\begin{equation}\label{eq:pivot}
  H_i(v)=\max_{a\in A} S_i(v,a).
\end{equation}
Both constructions use \decl{Finset.exists_max_image}; selected maximizers
are obtained through \decl{Classical.choice}. Consequently
\decl{VCG.xstar} and \decl{VCG.pivotTerm} are noncomputable definitions,
rather than an executable optimization algorithm. Ties are allowed, and
none of the proofs needs a specified tie-breaking order.

\begin{definition}[Clarke pivot charge]\label{def:pivot}
For each profile $v$, allocate $x^*(v)$ and charge agent $i$
\begin{equation}\label{eq:payment}
  p_i^*(v)=H_i(v)-S_i(v,x^*(v)).
\end{equation}
At truthful reporting its utility is
\begin{equation}\label{eq:utilityidentity}
  u_i(v)=v_i(x^*(v))-p_i^*(v)=W(v,x^*(v))-H_i(v).
\end{equation}
\end{definition}

The definition \decl{VCG.clarkePayment} gives the charges in
\eqref{eq:payment}. Utilities are recorded by \decl{VCG.utility}, with
identity \eqref{eq:utilityidentity} proved by \decl{VCG.utility_eq}.
The baseline in \eqref{eq:pivot} maximizes the
other agents' welfare over the \emph{same} $A$ as the original mechanism.
Removing agent $i$ from the sum does not create a new feasible-alternative
set. This detail is material when comparing the model to allocation
problems in which feasible outcomes change with participation.

\begin{theorem}[Pivot mechanism properties]\label{thm:pivot}
The allocation and charges in Definition~\ref{def:pivot} have the
following properties.
\begin{enumerate}
\item For all $v,a$, $W(v,a)\le W(v,x^*(v))$.
\item For all $v,i,r$, $U_i(v_i;v[i\leftarrow r])\le U_i(v_i;v)$,
where $U_i$ uses $x^*$ and $p^*$.
\item For all $v,i$, $0\le p_i^*(v)$, and hence
$0\le\sum_{i\in N}p_i^*(v)$.
\item If $v_j(a)\ge0$ for every $j\in N$ and $a\in A$, then
$u_i(v)\ge0$ for every $i\in N$.
\end{enumerate}
\end{theorem}

The first two results are \decl{VCG.vcg_efficient} and
\decl{VCG.vcg_truthful}. Nonnegative charges are established by
\decl{VCG.clarkePayment_nonneg}, then summed in \decl{VCG.vcg_noDeficit}.
The last theorem is \decl{VCG.vcg_individualRational}; its hypothesis,
named \decl{hnn}, is exactly $\forall j\,a,\ 0\le v_j(a)$.

\subsection{The truthfulness invariant}

Other-agent welfare does not change when only agent $i$ changes its report:
\begin{equation}\label{eq:update}
  S_i(v[i\leftarrow r],a)=S_i(v,a),\qquad
  H_i(v[i\leftarrow r])=H_i(v).
\end{equation}
The first identity follows term by term in the sum excluding $i$. For the
second, the artifact uses attainment on each side and the maximum bound
on the other side, then applies antisymmetry. This avoids requiring the
chosen maximizing \emph{alternatives} to agree: only the maximum
\emph{values} must agree. The lemmas are
\decl{VCG.othersWelfare_update} and \decl{VCG.pivotTerm_update}.

Put $w=v[i\leftarrow r]$. Expanding the charge and using
\eqref{eq:update} gives
\[
  U_i(v_i;w)=W(v,x^*(w))-H_i(v).
\]
Since $x^*(v)$ maximizes welfare computed using $v$,
\[
  W(v,x^*(w))-H_i(v)
    \le W(v,x^*(v))-H_i(v)=U_i(v_i;v).
\]
This proves item~2. In Lean, \decl{VCG.trueUtility_eq_of_agree} first proves
the welfare expression under agreement outside $i$, and
\decl{VCG.vcg_truthful} then applies it to an update.

The formal theorem compares a truthful profile with a one-agent deviation.
Its universal quantification gives dominant-strategy truthfulness against
arbitrary reports by the other agents: given their reports $w_{-i}$ and
agent $i$'s true valuation $t_i$, apply the theorem to the hybrid profile
$(t_i,w_{-i})$. There is no assumption that the other agents' submitted
reports match their true valuations.

\subsection{Payments and utility}

Equation~\eqref{eq:pivot} bounds $S_i(v,x^*(v))$, so
\eqref{eq:payment} is nonnegative for arbitrary real valuations.
Summing this inequality proves item~3. No deficit here means
nonnegative aggregate charges; the model contains no separate cost term.

For item~4, choose $a_i$ attaining $H_i(v)$. Then
\[
  H_i(v)=S_i(v,a_i)\le v_i(a_i)+S_i(v,a_i)
     =W(v,a_i)\le W(v,x^*(v)).
\]
Subtracting $H_i(v)$ and using \eqref{eq:utilityidentity} proves the claim.
Although this proof uses only $v_i(a_i)\ge0$ for the chosen agent, the
exported theorem assumes nonnegativity of \emph{all} entries. A weaker
hypothesis should not be attributed to that theorem merely because its
proof would support a refinement.

\section{The Groves payment characterization}

The pivot rule is one member of a larger family. A Groves-form payment has
an agent-specific term depending only on other agents' reports and
subtracts their welfare at the selected outcome.

\begin{theorem}[Finite unrestricted-domain necessity]\label{thm:groves}
Let $x:\V\to A$ and $p:\V\to\R^N$ satisfy efficiency
\eqref{eq:eff} and DSIC \eqref{eq:dsic} on the full domain
$\V=\R^{N\times A}$. There is a function
$h:N\times\V\to\R$ such that
\begin{align}
 v_{-i}=w_{-i}&\ \Longrightarrow\ h_i(v)=h_i(w),\label{eq:independent}\\
 p_i(v)&=h_i(v)-S_i(v,x(v))\qquad(v\in\V,\ i\in N).
 \label{eq:groves}
\end{align}
Here $v_{-i}=w_{-i}$ means $v_j=w_j$ as functions on $A$ for every $j\ne i$.
\end{theorem}

This is the conclusion of \decl{VCG.vcg_greenLaffont}. The source represents
$h_i$ as a function of a full profile and separately proves
\eqref{eq:independent}. It does not define a quotient type of other-agent
profiles. The theorem identifies the payment \emph{form}; it neither
fixes $h_i$ to the pivot maximum nor imposes individual rationality or
budget conditions on arbitrary $h_i$.

\subsection{Equal outcomes imply equal payments}

Fix $i$ and other reports, and abbreviate their welfare by $S(a)$.
Consider two reports $r,s$ by agent $i$ that select the same outcome $c$.
Apply DSIC with $r$ as the true report and $s$ as the deviation:
\[
  r(c)-p_i(s)\le r(c)-p_i(r).
\]
Here $p_i(r)$ abbreviates the payment at the full profile with these fixed
other reports. Reversing $r$ and $s$ proves the opposite payment
inequality, so $p_i(r)=p_i(s)$. The source uses this fact as a local lemma
inside \decl{VCG.groves_key}. It requires no continuity of the payment
rule.

\subsection{Forcing an alternative}

For any $c\in A$ and $\varepsilon>0$, the unrestricted report domain permits
\begin{equation}\label{eq:forced}
  r^{c,\varepsilon}(d)=-S(d)+
     \begin{cases}\varepsilon,&d=c,\\0,&d\ne c.\end{cases}
\end{equation}
Total welfare at $d$ becomes $\varepsilon$ when $d=c$ and $0$ otherwise.
Efficiency therefore forces $x=c$, even if the mechanism has arbitrary
tie-breaking at other profiles. By the preceding argument, every
positive $\varepsilon$ forcing $c$ has the same payment as the report
$r^{c,1}$. Any original report that selects $c$ also has that payment.
This step explains why restricting all reports to nonnegative valuations
would change the characterization argument: \eqref{eq:forced} need not
belong to such a restricted domain.

\subsection{Squeezing the payment difference}

Let two original profiles $v,w$ agree outside $i$, and put
$a=x(v)$, $b=x(w)$. If $a=b$, equal payments and equality of the relevant
other-agent welfare already give
\begin{equation}\label{eq:key}
  p_i(w)+S_i(w,x(w))=p_i(v)+S_i(v,x(v)).
\end{equation}
Suppose $a\ne b$. Apply DSIC to the forced report
$r^{a,\varepsilon}$ with deviation $r^{b,\varepsilon}$. Since payments at
these reports equal the original payments at $v$ and $w$, respectively,
\[
  S(a)-S(b)\le p_i(w)-p_i(v)+\varepsilon.
\]
Applying DSIC in the reverse direction gives
\[
  p_i(w)-p_i(v)\le S(a)-S(b)+\varepsilon.
\]
Both inequalities hold for every positive $\varepsilon$. The real order
lemma \decl{le_of_forall_pos_le_add} removes the perturbation on each side,
yielding
\[
  p_i(w)-p_i(v)=S(a)-S(b).
\]
Because the other reports agree, this is \eqref{eq:key}. Thus
\decl{VCG.groves_key} proves that $p_i(v)+S_i(v,x(v))$ is invariant under
changes to $i$'s report. The proof uses finite welfare sums, efficiency,
and real order;
no differentiability, continuity, integration, or limiting sequence is
introduced.

\subsection{Choosing an independent term}

Let $v^0=v[i\leftarrow0]$, where $0$ is the identically zero report. The
artifact defines
\[
  h_i(v)=p_i(v^0)+S_i(v^0,x(v^0)).
\]
If $v,w$ agree outside $i$, their zeroed profiles are equal, so
$h_i(v)=h_i(w)$. Applying \eqref{eq:key} to $v$ and $v^0$ and rearranging
establishes \eqref{eq:groves}. This completes the necessity theorem.

For context, the usual sufficiency argument is the same welfare
comparison as in the pivot proof: for an efficient $x$ and any term
satisfying \eqref{eq:independent}, a unilateral deviation changes utility
to $W(v,x(v[i\leftarrow r]))-h_i(v)$, which cannot exceed
$W(v,x(v))-h_i(v)$. The exported general theorem in this artifact is the
\emph{necessity} direction. We do not attribute a separately exported
general sufficiency theorem to the source.

\section{Proof organization and trust boundary}

The artifact divides its implementation into four substantive modules.
\source{VCG/Basic.lean}{\decl{VCG.Basic}} defines valuations, finite welfare
maximizers, pivot terms, charges, and truthful utility.
\source{VCG/Truthful.lean}{\decl{VCG.Truthful}} defines true utility at a
reported profile and proves update invariance, truthfulness, and
efficiency. \source{VCG/Properties.lean}{\decl{VCG.Properties}} proves
nonnegative charges, no deficit, and individual rationality.
\source{VCG/GreenLaffont.lean}{\decl{VCG.GreenLaffont}} proves the invariant
\eqref{eq:key} and the general payment characterization.
\decl{VCG.Main} publicly imports all four; \decl{Solution.lean} publicly
imports \decl{VCG.Main}.

The separate \decl{Challenge.lean} repeats public definitions and theorem
statements with twelve intentional \decl{sorry} placeholders: seven
nontrivial definition bodies and five theorem proofs. Its valuation
abbreviation is explicit. This statement-only comparator input is not a
proof of the results. It imports Mathlib rather than the implementation
modules. The implementation route is \decl{Solution}, whose
source and imported \decl{VCG} modules contain no \decl{sorry},
\decl{admit}, custom \decl{axiom}, or \decl{unsafe} declaration tokens at
the pinned revision.

The comparator configuration lists eight definition names and five theorem
names and permits \decl{propext}, \decl{Classical.choice}, and
\decl{Quot.sound}. The repository's verification script requests a build,
standalone challenge compilation, declaration-kind checks, placeholder
scanning, an axiom audit, and comparator checks. These are different
checks: matching interfaces does not make a placeholder proof valid, and
source-token scanning does not replace kernel checking. The script and
metadata describe the intended reproducibility procedure; this paper
makes no claim to have executed a fresh Lean build in the manuscript
preparation environment.

The version pins determine the Lean and dependency environment. They do
not establish that the prose matches every source theorem or that an
historical attribution is correct. Those are source-review obligations.
Likewise, a kernel-checked mathematical result does not supply a runtime
auction system, a verified optimizer, or economic guarantees outside the
formal hypotheses.

\section{Examples and limitations}

The pivot model does not imply exact budget balance. For two agents and
two alternatives $a,b$, take
\[
  (v_1(a),v_1(b))=(10,0),\qquad
  (v_2(a),v_2(b))=(0,6).
\]
The welfare-maximizing alternative is $a$, with total welfare $10$.
The pivot terms are $H_1=6$ and $H_2=10$, so the charges are $p_1^*=6$ and
$p_2^*=0$. Aggregate revenue is $6$, whereas budget balance in the
zero-cost model would require revenue $0$. Utilities are $4$ and $0$.
This example is explanatory arithmetic, not an additional named theorem
in the artifact.

Individual rationality cannot be read as unconditional on the full real
valuation domain. With one agent and one alternative valued at $-1$, the
other-agent welfare and pivot payment are $0$, and utility is $-1$.
The exported nonnegativity assumption rules out this example. There is
also no participation decision in the formal model, so the theorem's
``individual rationality'' means utility at least zero under its stated
hypothesis rather than comparison to a separately modeled reservation
utility.

The characterization does not single out Clarke pivot charges. Replacing
$H_i(v)$ by an arbitrary other-report-dependent $h_i(v)$ retains Groves
form and truthful incentives for efficient allocation, but may produce
negative charges or negative utility. Conversely, the necessity proof
uses the full unrestricted real report domain throughout; the result
should not be transferred unchanged to a restricted type space, a
randomized allocation rule, or an infinite alternative set.

No welfare-maximization complexity bound is formalized. Classical choice
provides selected maximizers for finite nonempty $A$ and yields a
mathematical mechanism, while executable optimization and deterministic
tie-breaking algorithms remain separate implementation questions.
Coalition resistance, Bayesian incentive constraints, approximate
efficiency, externalities in valuations, and feasibility changes upon
agent removal are outside this development.

\section{Reproducibility and manuscript provenance}

The pinned source repository \cite{VCGArtifact} provides the theorem
implementations, dependency manifest, comparator configuration, and
verification script. Its software license is BSD-3-Clause. This manuscript
and its two-file \LaTeX{} project are licensed CC BY 4.0; the manuscript
license does not change the repository's software license. The submitted
project consists of \decl{main.tex} and \decl{references.bib}. A standard
pdf\LaTeX{}, BibTeX, pdf\LaTeX{}, pdf\LaTeX{} sequence produces the reading
copy without bundling Lean source or prebuilt bibliography files.

The manuscript text was generated primarily with OpenAI GPT-6.1, with
human direction of the scope and some human understanding of the work.
No comprehensive personal, line-by-line human review is claimed.
AI-assisted source comparison and an independent AI mathematical and
bibliographic review were used in manuscript preparation; these are not
represented as human peer review. The repository's own formalization
metadata records a distinct implementation-assistance history involving
GPT-6-Luna. Lean's proof checking applies to the formal implementation,
not to the surrounding exposition, citations, or authorship assertions.

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