% Copyright (c) 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{booktabs,array}
\usepackage{listings}
\usepackage{microtype}
\usepackage{needspace}
\usepackage{xurl}
\usepackage[hidelinks]{hyperref}
\hypersetup{pdftitle={A Lean Formalization of Roberts Theorem on Unrestricted Valuations},
pdfauthor={Arthur Freitas Ramos; David Barros Hulak; Ruy J. G. B. de Queiroz},
pdfsubject={Expository formalization note in mechanism design},
pdfkeywords={Roberts theorem, mechanism design, Lean, affine maximizer, truthfulness}}
\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{\Sc}{S_{w,k}}
\newcommand{\upd}[3]{#1[#2\leftarrow #3]}
\newcommand{\decl}[1]{\nolinkurl{#1}}
\newcommand{\source}[2]{\href{https://github.com/Arthur742Ramos/roberts-theorem-lean/blob/0c176c66d2afa62301297f443b1e40eda2387ca2/#1}{#2}}
\lstset{basicstyle=\ttfamily\small,columns=fullflexible,keepspaces=true,
breaklines=true,breakatwhitespace=false,showstringspaces=false,
aboveskip=9pt,belowskip=9pt,frame=none}
\title[Roberts theorem in Lean]{A Lean Formalization of Roberts Theorem on Unrestricted Valuations}
\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]{91B14, 68V20}
\keywords{Roberts theorem, mechanism design, dominant strategies, affine maximizers, Lean 4, Mathlib}
\begin{document}
\begin{abstract}
We describe a Lean 4 formalization of the finite unrestricted-domain
version of Roberts theorem. For finite nonempty agent and alternative
types, with at least three alternatives, an onto deterministic
direct-revelation mechanism that is dominant-strategy incentive
compatible has an affine-maximizer choice rule. Valuations range over
all real-valued profiles; the conclusion uses fixed nonnegative weights,
at least one nonzero, and alternative offsets, and asserts membership
in the maximizing set. The development follows the modular proof route:
taxation and weak monotonicity, perturbation-based tie-breaking to strong
monotonicity, no-veto range analysis, affine prices for two agents, and
induction through fixed-report slices. We explain the proved tie-set
transport lemma, the construction of fresh payments for the tie-broken
rule, and the transfer back to arbitrary ties. A version-pinned account
distinguishes the proved library from statement-only comparator
placeholders and separates source inspection from executable checks.
This is an exposition of a classical result and its formal artifact,
with no claim of mathematical novelty or formalization priority.
\end{abstract}
\maketitle
\raggedbottom

\section{Scope and mathematical context}

Roberts theorem characterizes deterministic implementable choice rules
on an unrestricted quasilinear domain \cite{Roberts1979}. Its force
comes from allowing every agent to assign arbitrary real values to
every alternative. With an onto rule and at least three alternatives,
dominant-strategy incentive compatibility forces the rule to maximize
a fixed weighted sum of those values plus an alternative-dependent
constant. This is a characterization of the choice rule; it is not a
claim that every payment rule has one particular formula.

The artifact explained here follows the modular approach of Dobzinski
and Nisan \cite{DobzinskiNisan2009}. Its weak-to-strong monotonicity
reduction is attributed in the source to Lavi, Mu'alem, and Nisan
\cite{LaviMualemNisan2003}. The contribution of this note is to make the
formal model, the proof interfaces, and the verification boundary
readable. The mathematical theorem and proof strategy are classical.
We do not claim the first formalization of Roberts theorem or a new
mechanism-design result.

Implementation claims refer throughout to commit
\nolinkurl{0c176c66d2afa62301297f443b1e40eda2387ca2}
of \emph{roberts-theorem-lean} \cite{RobertsArtifact}. The pinned
toolchain is Lean \texttt{v4.35.0-rc2}; the Mathlib release tag is the
same, with manifest revision
\nolinkurl{065356127b1dc0016f66b7283ce0ce2c4055aa55}.
The September 30, 2026 source snapshot includes the proved transport
lemma and the rebuilt payment construction. In particular, an earlier
description of the transport lemma as a custom axiom does not describe
this snapshot.

\section{The formal economic model}

Let $N$ be a finite nonempty set of agents and $A$ a finite nonempty set
of alternatives. A valuation profile belongs to
\[
  \V=\{v:N\times A\to\R\}.
\]
The implementation uses the curried function type
\texttt{Valuation N A := N -> A -> Real}. There is no restriction to
nonnegative, normalized, integral, additive, monotone, or bounded
valuations. A mechanism $M=(f,p)$ consists of a choice rule
$f:\V\to A$ and payments $p:\V\times N\to\R$. Payments are subtracted
from value, so agent $i$'s utility at truthful profile $v$ is
$v_i(f(v))-p_i(v)$.

Write $\upd{v}{i}{t}$ for the profile obtained by replacing agent $i$'s
valuation with $t:A\to\R$. Dominant-strategy incentive compatibility
(DSIC), as defined by \decl{Roberts.IsDSIC}, is exactly
\begin{equation}\label{eq:dsic}
 v_i(f(v))-p_i(v)\ \geq\
 v_i(f(\upd{v}{i}{t}))-p_i(\upd{v}{i}{t})
 \quad\text{for every }i,v,t.
\end{equation}
The valuation on both sides is the true valuation $v_i$; only the
reported profile and its resulting payment change on the right.
Surjectivity, or \emph{onto}, means that for every $a\in A$ there exists
some profile $v$ with $f(v)=a$.

For fixed $w:N\to\R$ and $k:A\to\R$, define
\begin{equation}\label{eq:score}
 \Sc(v,a)=\sum_{i\in N}w_i v_i(a)+k(a).
\end{equation}
The source definition \decl{Roberts.IsAffineMaximizer} requires
$w_i\geq0$ for every $i$, some $w_i\ne0$, and
\begin{equation}\label{eq:am}
 \Sc(v,f(v))\geq\Sc(v,a)\qquad(v\in\V,\ a\in A).
\end{equation}
Weights and offsets are chosen once and work for every profile. Some
agents may have zero weight. Neither normalization of the weights nor
uniqueness of the weights, offsets, or selected alternative is part of
the conclusion. In particular, \eqref{eq:am} allows an arbitrary
selection among tied affine-score maximizers.

\begin{theorem}[Formalized Roberts theorem]\label{thm:main}
Suppose $N$ and $A$ are finite and nonempty and $|A|\geq3$. If
$M=(f,p)$ is DSIC and $f$ is onto, then $f$ is an affine maximizer in
the sense of \eqref{eq:score}--\eqref{eq:am}.
\end{theorem}

The declaration \decl{Roberts.roberts_theorem} appears in
\source{Roberts/Induction.lean}{Roberts/Induction.lean}. Its explicit
economic hypotheses are DSIC and onto, together with the cardinality
condition. The surrounding Lean context supplies \texttt{Fintype},
\texttt{DecidableEq}, and \texttt{Nonempty} instances for both types.
Decidable equality is part of this implementation interface; it is
not an additional restriction on preferences. Its conclusion concerns
$M$'s choice function and makes no assertion about budget balance,
individual rationality, participation constraints, or computation time.

\section{Taxation and weak monotonicity}

Fix agent $i$ and the reports of everyone else. The attainable menu is
\[
 B_i(v)=\{a\in A:\exists t, f(\upd{v}{i}{t})=a\}.
\]
The source calls this predicate \decl{Achievable}. Two reports that
produce the same alternative must produce the same payment for $i$:
apply DSIC in each direction and cancel the common true value at that
alternative. Thus a real menu price $P_i(v,a)$ is well defined on
$B_i(v)$ and independent of agent $i$'s report. The implementation
chooses one witnessing report for an attainable alternative; it assigns
zero to unattainable alternatives simply to make \decl{price} a total
real-valued function. The taxation inequality is used only with an
attainability hypothesis.

For every attainable $a$, the chosen alternative maximizes utility
relative to the menu:
\begin{equation}\label{eq:tax}
 t(f(\upd{v}{i}{t}))-P_i(v,f(\upd{v}{i}{t}))
 \ \geq\ t(a)-P_i(v,a).
\end{equation}
These statements are \decl{taxation_payment},
\decl{price_independent}, and \decl{taxation_ineq} in
\source{Roberts/Taxation.lean}{Roberts/Taxation.lean}.

\begin{definition}
A choice rule is \emph{weakly monotone} (W-MON) if, whenever
$a\ne b$, $f(\upd{v}{i}{t})=a$, and $f(\upd{v}{i}{s})=b$,
\begin{equation}\label{eq:wmon}
 t(a)-t(b)\geq s(a)-s(b).
\end{equation}
It is \emph{strongly monotone} (S-MON) if the inequality is strict
under the same hypotheses.
\end{definition}

Applying \eqref{eq:tax} first to report $t$ and alternative $b$, then
to report $s$ and alternative $a$, eliminates the two prices and gives
\eqref{eq:wmon}. This is \decl{wmon_of_dsic}. The strict variant is a
property of changes of outcome; it does not require a strict utility
inequality for every deviation. It will be obtained by a new
tie-broken rule, rather than assumed of the original mechanism.

\section{Tie sets and the strong monotonicity reduction}

For $x\in A$ and $\varepsilon\in\R$, the simultaneous perturbation is
\[
 (v^{x,\varepsilon})_j(a)
   =v_j(a)+\varepsilon\,\mathbf1_{a=x}\quad(j\in N).
\]
For a W-MON rule $f$, define
\begin{equation}\label{eq:tieset}
 T_f(v)=\{x\in A:\exists\delta>0\ 
       \forall\varepsilon\in(0,\delta), f(v^{x,\varepsilon})=x\}.
\end{equation}
This is a perturbational definition, not a reference to weights that
have yet to be proved to exist. Raising only the current winner's
value for one agent preserves that winner by W-MON. Repeating over
the finite agent set shows $f(v)\in T_f(v)$, so the set is nonempty.

Fix a linear order on $A$ and let $g(v)=\max T_f(v)$. The source
obtains an order by transport along \texttt{Fintype.equivFin} and
defines \decl{tieBreak} by \texttt{Finset.max'}. This auxiliary order
does not impose a tie convention on the original rule.

\begin{lemma}[Tie-set transport]\label{lem:transport}
Let $v,v'$ differ only in agent $i$'s report. If
$x\in T_f(v)$, $y\in T_f(v')$, and
\[
 v'_i(x)-v'_i(y)\geq v_i(x)-v_i(y),
\]
then $x\in T_f(v')$.
\end{lemma}

The declaration \decl{key_lemma} in
\source{Roberts/SMon.lean}{Roberts/SMon.lean} proves this statement.
Here is the asymmetric perturbation used in its proof. Assume $x\ne y$,
take a sufficiently small $\varepsilon>0$, and put $t=\varepsilon/5$.
Set
\[
 p=v^{x,t},\qquad s=(v')^{y,t},\qquad
 q_j(a)=v'_j(a)+4t\mathbf1_{a=x}+2t\mathbf1_{a=y},\qquad
 r=\upd{q}{i}{p_i}.
\]
The tie-set hypotheses give $f(p)=x$ and $f(s)=y$.
From $p$ to $r$, unchanged agent $i$ is left alone and every other
agent's $x$-versus-anything-else gap strictly increases. Sequential
W-MON updates imply $f(r)=x$. From $s$ to $q$, every agent's gap
between either element of $\{x,y\}$ and an outside alternative
strictly increases; the same update argument gives $f(q)\in\{x,y\}$.
If $f(q)=y$, the unilateral transition from $r$ to $q$ would require
\[
 (v_i(x)-v_i(y))+t
 \ \geq\ (v'_i(x)-v'_i(y))+2t,
\]
contradicting the hypothesis and $t>0$. Hence $f(q)=x$. Moving from
$q$ to $(v')^{x,5t}$ strictly increases every agent's $x$ gaps again,
so that profile chooses $x$. The allowed range of $\varepsilon$ proves
\eqref{eq:tieset} for $x$ at $v'$.

\Needspace{6\baselineskip}
\begin{proposition}\label{prop:smon}
The tie-broken rule $g$ is S-MON. If $f$ is onto, then $g$ is onto.
\end{proposition}

\begin{proof}
Suppose $g$ chooses distinct $a,b$ under two unilateral reports. If
the gap inequality were not strict, Lemma~\ref{lem:transport} would
place $a$ in the second tie set and, by exchanging the alternatives
and profiles, place $b$ in the first. Maximality then gives $a\leq b$
and $b\leq a$, contradicting distinctness. This is
\decl{tieBreak_isSMon}.

If $f(v)=a$, every positive simultaneous bump of $a$ has tie set
$\{a\}$. Indeed, a further sufficiently small bump of another
alternative still leaves all $a$ gaps strictly above their values at
$v$, so W-MON preserves $a$. Thus $g(v^{a,1})=a$. Starting from an
onto witness for each $a$ proves \decl{tieBreak_onto}.
\end{proof}

\subsection{Fresh payments for the auxiliary rule}

The proof requires a DSIC mechanism with choice function $g$. Strong
monotonicity implies weak monotonicity, but the original mechanism's
prices are not automatically valid for its changed outcomes. The
artifact instead proves \decl{wmon_dsic_payments}: every W-MON rule
on this full valuation domain admits DSIC payments. This construction
is in \source{Roberts/Induction.lean}{Roberts/Induction.lean}.

To see its signs and domain obligations, fix the other reports, write
$h(t)$ for the one-agent choice rule, and let $K=h(0)$. Define
\begin{equation}\label{eq:infmenu}
 d(a)=\inf\{t(K)-t(a):h(t)=K\}.
\end{equation}
The set is nonempty because the zero report selects $K$. For each
attainable $a$, W-MON supplies a lower bound using any report selecting
$a$. Thus the infimum used for attainable alternatives is an ordinary
finite real infimum. W-MON also gives, whenever $h(t)=a$,
$t(K)-t(a)\leq d(a)$, while reports selecting $K$ satisfy
$d(a)\leq t(K)-t(a)$ for attainable $a$. In particular $d(K)=0$.

The remaining argument shows
\[
 t(h(t))+d(h(t))\geq t(h(s))+d(h(s))\quad\text{for all reports }t,s.
\]
The source proves this by contradiction: if an attainable alternative
had higher utility, raise the anchor $K$ to an intermediate utility
level and raise the currently selected alternative slightly.
The anchor inequalities rule out both the anchor and the old outcome;
W-MON then contradicts that slight raise. Setting the payment at a
chosen outcome to $-d(h(t))$ yields DSIC. Values of the total Lean
infimum definition at unattainable alternatives are not used to compare
actual deviations. Applied to $g$, this supplies newly constructed
payments, which are the ones used in the induction theorem.

\section{No veto and affine prices}

For a fixed report $t$ of agent $i$, define the range
\[
 R_i(t)=\{a\in A:\exists v, f(\upd{v}{i}{t})=a\}.
\]
This holds $i$ fixed and allows all other agents to vary. It differs
from the taxation menu, which holds the other agents fixed and varies
$i$. Agent $i$ has \emph{no veto power} if $R_i(t)=A$ for every $t$.
An alternative $a$ is \emph{dictatable} by $i$ if $R_i(t)=\{a\}$ for
some $t$. The latter describes a report that forces one outcome, not
a blanket dictatorship assertion about the entire rule.

\begin{proposition}[No-veto range theorem]\label{prop:noveto}
For an onto S-MON rule with at least three alternatives, there is an
agent $e$ such that every $i\ne e$ has no veto power.
\end{proposition}

This is \decl{all_but_one_no_veto} in
\source{Roberts/NoVeto.lean}{Roberts/NoVeto.lean}. The proof analyzes
single-alternative boosts. Increasing the fixed agent's value of $a$
can add no new range element other than $a$:
\[
 R_i(t+d\mathbf1_a)\subseteq R_i(t)\cup\{a\}\quad(d>0).
\]
If $a$ is not dictatable, sufficiently large boosts make this range
full, with a common finite bound obtained by summing absolute values
of finitely many pairwise gap bounds. It follows that an agent with
no dictatable alternative has no veto power. Two distinct agents
cannot force distinct alternatives simultaneously. If they both
force the same $a$, that alternative belongs to the first agent's
range at every report. An alternative $x\ne a$ is then not dictatable
by that agent; boosting it would make the range full while the subset
inclusion keeps the range inside $\{a,x\}$. A third alternative gives
the contradiction. This accounts for the cardinality assumption in
this range argument without strengthening the statement to universal
no-veto power.

\subsection{The two-agent representation}

Suppose there are exactly two distinct agents $i_1,i_2$, and $i_1$ has
no veto power. Then every alternative is attainable by $i_2$ at every
profile. The taxation prices of $i_2$ therefore apply to all of $A$.
For a DSIC, S-MON mechanism the theorem \decl{price_affine_form} proves
\begin{equation}\label{eq:affprices}
 P_{i_2}(v,a)=H(v)-\alpha v_{i_1}(a)-\beta(a),
 \qquad\alpha\geq0.
\end{equation}
Here $H$ may depend on the profile but is common to all alternatives;
$\alpha$ and $\beta$ are fixed. These are menu prices, not a claimed
classification of every payment to both agents.

The proof in \source{Roberts/TwoAgent.lean}{Roberts/TwoAgent.lean}
first shows that the difference of prices at $a,b$ depends only on
$v_{i_1}(a)-v_{i_1}(b)$ and is nonincreasing in that gap. Normalize
prices at one reference alternative. The response to a coordinate
increase is independent of the alternative and of the base profile;
a third alternative supplies the comparison needed for the latter
step. The response function $\ell:\R\to\R$ is additive and
nonincreasing. The lemma \decl{additive_mono_linear} proves
$\ell(t)=\ell(1)t$, using integer and rational scaling and the
Archimedean order structure of the reals. It does not infer real
linearity from additivity alone.

Substitution of \eqref{eq:affprices} into taxation shows that the
selected alternative maximizes
\[
 \alpha v_{i_1}(a)+v_{i_2}(a)+\beta(a).
\]
Thus \decl{two_agent_affine_maximizer} takes weights $\alpha,1$.
The second weight is positive even if the first is zero. Together
with Proposition~\ref{prop:noveto}, this proves the two-agent base
case of the general induction.

\section{Induction through fixed-report slices}

The declaration \decl{dsic_smon_affine_aux} proves the DSIC, S-MON,
onto theorem by induction on an upper bound for the number of agents.
The zero case is excluded by nonemptiness. With one agent, onto makes
every alternative attainable, and the taxation menu is independent
of the entire profile. Weight one and offsets equal to the negatives
of those prices give an affine maximizer. The offsets may depend on
the alternative; this base case does not assert unweighted value
maximization without offsets.

For $|N|\geq3$, choose a no-veto agent $i_0$ distinct from the
possibly exceptional agent in Proposition~\ref{prop:noveto}. The
implementation fixes this \emph{no-veto} agent's report $t$ and
restricts the remaining agents to the subtype $N\setminus\{i_0\}$.
This choice is important: no veto makes each fixed-report slice onto.
DSIC and S-MON pass to the slice through explicit extension and
restriction identities. The induction hypothesis supplies an affine
representation for every slice.

Normalize the slice's nonnegative, nontrivial weights by their
positive sum and lift them to $N$ with zero at $i_0$. Denote the
normalized weights by $w^t$ and the offsets by $k^t$. They satisfy
$\sum_i w_i^t=1$. The main consistency obligations are:
\begin{enumerate}
\item The normalized weights away from $i_0$ do not depend on $t$.
The proof compares slices after a positive coordinate bump and then
compares any two reports through a common strict coordinatewise upper
report. A finite-dimensional half-space argument shows proportionality
of the relevant vectors; normalization converts it to equality.
\Needspace{5\baselineskip}
\item There is one $\alpha\geq0$ such that
\begin{equation}\label{eq:offset}
 (k^t(a)-\alpha t(a))-(k^t(b)-\alpha t(b))
\end{equation}
is independent of $t$ for every $a,b$.
\end{enumerate}
The source exposes \decl{weights_independent_of_fixed_agent} and
\decl{offsets_consistent_of_fixed_agent}; the induction itself also
uses their private core lemmas. The offset core retains the explicit
nonnegativity of $\alpha$ needed in the final weights.

For offsets, a positive weight on some remaining agent lets that
agent force comparisons between alternatives within a slice.
Strong monotonicity makes an offset difference depend only on the
fixed agent's corresponding value gap. Three-alternative identities
give a common additive response, and monotonicity makes it linear.
This produces \eqref{eq:offset}, allowing a common profile-dependent
additive constant, which is immaterial to maximization.

At a zero reference report define $W_{i_0}=\alpha$,
$W_i=w_i^0$ for $i\ne i_0$, and $K(a)=k^0(a)$.
The difference between global scores at any $a,b$ equals the
difference of the slice scores for $t=v_{i_0}$. That slice chooses
$f(v)$, so its maximizing inequality is the desired global one.
The remaining weights already contain a positive entry; hence the
global weights are nontrivial. This proves
\decl{dsic_smon_affine_maximizer}.

\section{Returning to the original rule}

It remains to recover the W-MON rule $f$, whose ties need not follow
the auxiliary order. The declaration \decl{affine_maximizer_transfer}
uses the same weights and offsets as for $g$. Let $x=f(v)$ and
$y=g(v)$. If $\Sc(v,x)<\Sc(v,y)$, choose a positive bump
$\eta$ small enough both for the stability of $x$ and for
\[
 \eta\sum_i w_i<\Sc(v,y)-\Sc(v,x).
\]
Bumping $x$ raises its score by exactly $\eta\sum_i w_i$ and leaves
$y$'s score unchanged. But a positive bump of a winner makes the
tie-broken rule select that winner, contradicting affine maximization
of $g$ at the bumped profile. Therefore the two scores at $v$ are
equal, and $f(v)$ is a maximizer as well.

The final assembly has the following dependencies:
\begin{enumerate}
\item DSIC of $M$ gives W-MON of $f$ by taxation
\item Tie-set transport gives S-MON, hence W-MON, of $g$
\item W-MON supplies fresh DSIC payments for $g$
\item Onto is preserved by tie-breaking, and induction makes $g$
an affine maximizer
\item The perturbation transfer gives the same affine-maximizer
property for $f$
\end{enumerate}
This is the actual sequence in \decl{Roberts.roberts_theorem}. It
neither assumes strong monotonicity of $f$ nor reuses $M$'s payment
rule after changing its choice rule.

\section{Artifact interfaces and verification boundary}

The library modules form the dependency chain
\decl{Defs}, \decl{Taxation}, \decl{SMon}, \decl{NoVeto},
\decl{TwoAgent}, and \decl{Induction}, all in the \decl{Roberts}
namespace. The package root \texttt{Roberts.lean} and compatibility
module \texttt{Roberts/Basic.lean} import the development;
\texttt{Solution.lean} imports the proved package. The separate
\texttt{Challenge.lean} independently states the model and target for
declaration comparison. Its two predicate definitions and target
theorem contain three intentional \texttt{sorry} placeholders. They
are not part of the solution's import chain.

Source inspection on September 30, 2026 found zero \texttt{sorry},
\texttt{admit}, \texttt{axiom}, or \texttt{unsafe} tokens in
\texttt{Roberts/*.lean} and in \texttt{Solution.lean}. In particular,
\decl{key_lemma} has a proof body, not an axiom declaration. This
syntactic inspection is distinct from elaboration and kernel checking.
The project reports a successful local build and an axiom audit whose
dependency set for the main theorem is
\[
 \{\texttt{propext},\ \texttt{Classical.choice},\ \texttt{Quot.sound}\}.
\]
The September 27, 2026 packaging commit records successful local
declaration, build, placeholder, axiom, comparator, and whitespace
checks \cite{RobertsAuditCommit}. A separate Palomar verification run
for that same September 27 revision completed successfully at
14:55 UTC that day; its workflow logs identify the submitted revision
and the successful comparator and challenge-provenance step
\cite{RobertsMechanicalRun}. Inspection on September 30 confirmed that
the Lean source from that revision to the manuscript pin changes only
module headers, public visibility, and definition exposure annotations:
after removing those annotations and blank lines, every Lean file is
textually identical. The toolchain and dependency manifest are unchanged.
This comparison does not constitute a fresh build of the revised module
packaging. The pinned repository includes a script to repeat the local
checks; its metadata labels review status self-assessed. Neither the
recorded mechanical run nor these source checks establish external
mathematical peer review.

The verification procedure builds the library, elaborates separate
challenge and solution declaration checks, and runs
\texttt{\#print axioms Roberts.roberts\_theorem} against the solution.
It compares the resulting dependencies with an allowed set rather
than treating the allowed list itself as proof of actual dependencies.
The comparator targets \decl{IsDSIC}, \decl{IsAffineMaximizer}, and
\decl{roberts_theorem}; the valuation abbreviation and mechanism
structure remain visible model definitions but are not listed as
predicate comparator targets. A reproducible check must use the
pinned toolchain and dependency manifest, not merely a recent Lean
installation.

The fresh manuscript preparation included source-to-statement
inspection, independent source and mathematical review, and a clean
LaTeX compilation of an extracted source archive with visual inspection
of every PDF page. These are checks on this exposition and its rendering.
A fresh Lean execution was not performed in the manuscript's cloud
typesetting workspace, which had no Lean executable. Lean's kernel
checks the propositions supplied to it; it does not by itself validate
the correspondence of prose to economic interpretation, historical
attribution, or the scope of a repository-status claim.

\section{Limitations and provenance}

The theorem is confined to finite nonempty agent and alternative
types, deterministic direct revelation, unrestricted real valuations,
onto choice, and at least three alternatives. It does not formalize
a generalization to restricted auction or scheduling domains,
randomized mechanisms, infinite sets of agents or alternatives,
Bayesian incentive compatibility, or two-alternative rules. The
artifact proves the necessary affine-maximizer representation of
choice functions; a separate converse characterizing all admissible
tie rules or all original payments is not its headline statement.

The weights, order transport, witness prices, and slice representations
use classical and noncomputable constructions. The development proves
existence and score inequalities; it does not extract an efficient
algorithm to recover weights from an arbitrary mechanism. Allowing
zero weights and arbitrary affine-score ties is essential to the
statement actually encoded.

\paragraph{AI assistance and human understanding.}
This manuscript was drafted primarily with GPT-6.1 assistance,
including exposition, source alignment, and typesetting. The
repository's metadata separately reports GPT-6-Luna assistance for
the formalization and packaging. Some human understanding informed
the work; no claim is made that every listed author independently
understands every formal proof step. The model-assisted review of
this manuscript is not independent human peer review, and acceptance
by an archive would not establish such review.

\Needspace{8\baselineskip}
\paragraph{Attribution and availability.}
Roberts is credited for the characterization; Dobzinski and Nisan
for the modular proof route; Lavi, Mu'alem, and Nisan for the
monotonicity and tie-breaking route; and Lean and Mathlib contributors
for the proof infrastructure. The pinned source repository is
BSD-3-Clause licensed. This manuscript and its TeX source are
separately licensed CC BY 4.0. The TeX archive contains the manuscript
and bibliography, while the Lean implementation and verification
script remain in the referenced repository.

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