\documentclass[11pt]{amsart}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{microtype}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{booktabs,array}
\usepackage[margin=1in]{geometry}
\usepackage{xurl}
\usepackage[colorlinks=true,linkcolor=blue,citecolor=blue,urlcolor=blue]{hyperref}
\hypersetup{pdftitle={Arrow and Gibbard Satterthwaite Theorems in Lean},pdfauthor={Arthur Freitas Ramos; David Barros Hulak; Ruy J. G. B. de Queiroz},pdfsubject={Finite strict-ranking social choice impossibility formalizations},pdfkeywords={Arrow theorem, Gibbard Satterthwaite, Lean 4, social choice}}
\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{\Nat}{\mathbb N}
\newcommand{\Ballot}{\mathcal B}
\newcommand{\Profiles}{\mathcal P}
\newcommand{\pref}{\succ}
\newcommand{\code}[1]{\texttt{\small #1}}
\setlength{\emergencystretch}{1em}
\newcommand{\Pred}{\operatorname{Pred}}
\title[Arrow and Gibbard Satterthwaite in Lean]{Arrow and Gibbard Satterthwaite Theorems in Lean}
\author{Arthur Freitas Ramos}
\author{David Barros Hulak}
\author{Ruy J. G. B. de Queiroz}
\date{October 1, 2026}
\subjclass[2020]{91B14, 68V20}
\keywords{social choice, Arrow theorem, Gibbard--Satterthwaite theorem, decisive coalition, strategy-proofness, Lean 4, formal verification}
\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. This manuscript is licensed under \href{https://creativecommons.org/licenses/by/4.0/}{Creative Commons Attribution 4.0 International}. The cited Lean repositories have their separate BSD-3-Clause licenses.}
\begin{document}
\begin{abstract}
We give a source-aligned account of two Lean 4 formalizations of classical finite social-choice impossibility theorems. For a finite nonempty electorate and a finite alternative set containing three distinct alternatives, Arrow's theorem derives dictatorship from unanimity and independence of irrelevant alternatives. Its proof expands a weakly decisive coalition from one ordered pair to all pairs, then contracts decisive coalitions to a singleton. The Gibbard--Satterthwaite development proves that every onto strategy-proof choice function on the unrestricted strict-ranking domain is dictatorial by constructing a social welfare function and applying that Arrow implementation. We explain the essential construction in full: top-two profiles define pairwise comparisons; strategy-proof monotonicity and three-top profiles establish a strict total order; predecessor counts provide injective natural-number ranks. Exact hypotheses, vendored dependencies, pinned source identities, prior formalizations, and the distinction between historical registry verification and the present source audit are recorded. The contribution is an exposition and audit of reusable formalization artifacts, not a new social-choice theorem or a claim of first formalization.
\end{abstract}
\maketitle

\section{Introduction}
Arrow's theorem and the Gibbard--Satterthwaite theorem expose two different limits of collective decision making. Arrow studies the aggregation of individual rankings into a social ranking. Gibbard--Satterthwaite studies the selection of one alternative when each voter may misreport a ranking. Their classical sources are Arrow's 1950 paper \cite{arrow1950}, Gibbard's 1973 paper \cite{gibbard1973}, and Satterthwaite's 1975 paper \cite{satterthwaite1975}.

The artifacts examined here are Arthur Freitas Ramos's finite Arrow development \cite{ramosArrow} and its Gibbard--Satterthwaite extension \cite{ramosGS}, registered separately in Palomar \cite{palomarArrow,palomarGS}. Their mathematical dependence makes a combined exposition natural. The second repository contains a byte-identical copy of the first repository's four substantive Arrow modules, and its main theorem invokes the copied Arrow theorem. The manuscript's subject is therefore one proof chain: decisive coalitions establish Arrow; strategy-proof choice is converted into a valid strict social ranking; Arrow's dictator is transferred back to the original choice rule.

The source pins used throughout are
\begin{center}\small
\begin{tabular}{ll}
\toprule
Arrow & \texttt{4f405d27d0b244574bbee5d3d79bae0c66bda16e}\\
Gibbard--Satterthwaite & \texttt{8398e65a99cd3d5e973c64963c4bab8c0491947c}\\
\bottomrule
\end{tabular}
\end{center}
These identify repository snapshots, not merely branch names. Both use Lean \code{v4.\allowbreak{}35.\allowbreak{}0-rc2} and the same Mathlib manifest revision, recorded in Section~\ref{sec:verification}.

Our main expository task is to make the intermediate social welfare function explicit. Choosing winners on two-alternative tests does not by itself produce a ballot: the resulting pairwise relation might have cycles or tied numerical scores. The formalization proves the order laws before using predecessor counts to construct an injective ranking. This step is essential to the reduction, and was specifically absent from the optional proof sketch noted in the Gibbard--Satterthwaite registry review \cite{palomarGS}.

The mathematical route is established. Satterthwaite describes Gibbard's construction of a social welfare function from strategy-proof voting, the verification of Pareto and independence conditions, the use of Arrow, and the transfer of dictatorship \cite[pp.~205--207]{satterthwaite1975}. Formal proofs of both theorems also predate these Lean repositories; Nipkow formalized them in Isabelle/HOL \cite{nipkow2009}. Peters's earlier public Lean development proves a resolute unanimous strategy-proof choice correspondence dictatorial using voter cloning and strong induction \cite{peters2026}; we consulted its pinned source, without rebuilding it. The Arrow metadata separately acknowledges Joris Roos's independent three-candidate Fourier-analytic Lean formalization \cite{roos2026}. We claim neither a new reduction nor priority among formalizations. The present contribution is a readable explanation of the precise finite strict-ranking implementations, their interfaces, and their verification boundary.

\section{The strict ranking domain and exact statements}\label{sec:domain}
Let $V$ be a finite nonempty electorate and $A$ a finite set of alternatives. The main results take explicit witnesses $x,y,z\in A$ satisfying
\begin{equation}\label{eq:three}
x\ne y,\qquad x\ne z,\qquad y\ne z.
\end{equation}
Thus the alternative-set hypothesis is at least three alternatives, without fixing a particular cardinality. The Lean interfaces use \code{Fintype V}, \code{Fintype A}, \code{DecidableEq V}, \code{DecidableEq A}, and \code{Nonempty V}. The Gibbard--Satterthwaite interface also supplies \code{Nonempty A}; condition~\eqref{eq:three} already entails it mathematically. No assumption of two or more voters is made. A one-voter electorate is included.

\subsection{Ballots as injective natural ranks}
The common representation is
\begin{equation}\label{eq:ballot}
\Ballot(A)=\{s:A\longrightarrow\Nat\mid s\text{ is injective}\},
\qquad a\pref_s b\quad\Longleftrightarrow\quad s(a)<s(b).
\end{equation}
Lower numbers mean higher preference. Injectivity makes $\pref_s$ irreflexive, asymmetric, transitive, and total on distinct alternatives. Rankings need not be consecutive integers or bounded by $|A|-1$. Conversely, every strict linear order on a finite set can be represented by counting predecessors in that order. This elementary mathematical observation explains the domain; the pinned Arrow library does not separately state a general representation theorem. Thus~\eqref{eq:ballot} supplies the full strict-ranking domain. It excludes indifference and partial orders.

A profile is $P\in\Profiles(V,A)=V\to\Ballot(A)$. We write $a\pref_{P_v}b$ for voter $v$'s comparison. Both a social welfare function and a social choice function are defined on every profile:
\[
F:\Profiles(V,A)\longrightarrow\Ballot(A),
\qquad f:\Profiles(V,A)\longrightarrow A.
\]
Unrestricted domain is built into these function types. The implementations do not begin with a quotient that identifies different numerical encodings of the same ranking. Their axioms and conclusions concern the induced comparisons; equality of complete natural-number score functions is not Arrow's dictatorship conclusion.

\subsection{Arrow's axioms}
A social welfare function $F$ is \emph{unanimous} if
\begin{equation}\label{eq:unanimous}
\forall P,a,b,\quad (\forall v\in V,\ a\pref_{P_v}b)
\ \Longrightarrow\ a\pref_{F(P)}b.
\end{equation}
It satisfies \emph{independence of irrelevant alternatives} (IIA) if
\begin{equation}\label{eq:iia}
\left[\forall v,\ a\pref_{P_v}b\ \Longleftrightarrow\ a\pref_{Q_v}b\right]
\ \Longrightarrow\
\left[a\pref_{F(P)}b\ \Longleftrightarrow\ a\pref_{F(Q)}b\right]
\end{equation}
for all profiles and alternatives. A voter $d$ is a dictator of $F$ precisely when
\begin{equation}\label{eq:arrowdictator}
\forall P,a,b,\qquad a\pref_{P_d}b\ \Longleftrightarrow\ a\pref_{F(P)}b.
\end{equation}
There is no anonymity or neutrality hypothesis. Social transitivity and completeness come from the codomain $\Ballot(A)$.

\begin{theorem}[Finite strict-ranking Arrow theorem]\label{thm:arrow}
Under the finite-domain hypotheses above and~\eqref{eq:three}, every unanimous social welfare function satisfying IIA has a dictator in the sense of~\eqref{eq:arrowdictator}.
\end{theorem}
The selected declaration is \code{Arrow.\allowbreak{}Palomar.\allowbreak{}arrowImpossibility}; the substantive theorem is \code{Arrow.\allowbreak{}arrowImpossibility} in \code{Arrow/\allowbreak{}ArrowTheorem.\allowbreak{}lean}.

\subsection{Strategy proof choice}
For a profile $P$, voter $v$, and ballot $b$, let $P[v\leftarrow b]$ replace only $v$'s report. Strategy-proofness means
\begin{equation}\label{eq:sp}
\forall P,v,b,\qquad
\neg\bigl(f(P[v\leftarrow b])\pref_{P_v} f(P)\bigr).
\end{equation}
The comparison uses the true ballot $P_v$ on both outcomes. Onto means $f$ is surjective: for every $a\in A$, some profile selects $a$. Dictatorship of a choice function is the existence of $d\in V$ such that
\begin{equation}\label{eq:gsdictator}
\forall P,a,\qquad a\ne f(P)\ \Longrightarrow\ f(P)\pref_{P_d}a.
\end{equation}
Equivalently, the chosen alternative is always $d$'s unique top choice. A finite nonempty ballot has such a unique top alternative.

\begin{theorem}[Finite strict-ranking Gibbard--Satterthwaite theorem]\label{thm:gs}
Under the finite-domain hypotheses above and~\eqref{eq:three}, every onto strategy-proof social choice function is dictatorial in the sense of~\eqref{eq:gsdictator}.
\end{theorem}
This is \code{GibbardSatterthwaite.\allowbreak{}gibbardSatterthwaite}, proved in \code{GS/\allowbreak{}Main.\allowbreak{}lean}. It concerns deterministic single-valued choice without transfers on the full strict-ranking domain. It does not assert an impossibility for restricted domains, randomized rules, weak preferences, or infinite electorates.

\section{Arrow through decisive coalitions}\label{sec:arrowproof}
For a coalition $G\subseteq V$ and distinct $a,b$, the implementation distinguishes two properties. \emph{Weak decisiveness} for $(a,b)$ requires $F(P)$ to rank $a$ above $b$ whenever every member of $G$ ranks $a$ above $b$ and every outsider ranks $b$ above $a$. \emph{Decisiveness for the pair} requires the same social comparison whenever the members agree on $a\pref b$, with no condition on outsiders. A coalition is \emph{decisive} if it is decisive for every ordered pair of distinct alternatives. These are \code{WeakDecisive}, \code{DecisivePair}, and \code{Decisive} in \code{Arrow/\allowbreak{}Basic.\allowbreak{}lean}.

The whole electorate is decisive by unanimity. The selected theorem \code{Arrow.\allowbreak{}Palomar.\allowbreak{}decisiveUniv} exposes this first step. The remaining argument uses field expansion and group contraction.

\subsection{Realizing auxiliary profiles}
The proof must produce full ballots, not just diagrams involving three alternatives. Given any injective baseline $s_0:A\to\Nat$ and three distinct alternatives $a,b,c$, \code{chainFun} assigns scores $0,1,2$ to $a,b,c$ respectively, and $3s_0(w)+3$ to every other $w$. The resulting function is injective: the designated scores are distinct and less than every residual score, while injectivity on the residual alternatives follows from that of $s_0$. A baseline is obtained from an equivalence with a finite initial segment of $\Nat$. The theorem \code{exists\_\allowbreak{}chain} consequently realizes $a\pref b\pref c$ as a ballot over all of $A$.

\subsection{Field expansion}
\begin{lemma}[Field expansion]\label{lem:expansion}
If $F$ is unanimous and satisfies IIA, and $G$ is weakly decisive for one ordered pair $(a,b)$, then, given a third distinct alternative, $G$ is decisive for every ordered pair.
\end{lemma}
\begin{proof}
We describe the first expansion in the source, which is representative of the construction. To prove decisiveness for $(a,c)$, take an arbitrary profile $Q$ at which every member of $G$ ranks $a$ above $c$. Construct $P$ with these three-alternative restrictions:
\begin{center}
\begin{tabular}{ll}
\toprule
Voters & Restriction of $P$\\
\midrule
$v\in G$ & $a\pref b\pref c$\\
$v\notin G$, $a\pref_{Q_v}c$ & $b\pref a\pref c$\\
$v\notin G$, $c\pref_{Q_v}a$ & $b\pref c\pref a$\\
\bottomrule
\end{tabular}
\end{center}
Weak decisiveness gives $a\pref_{F(P)}b$. Unanimity gives $b\pref_{F(P)}c$, so transitivity gives $a\pref_{F(P)}c$. Every voter has the same $a,c$ comparison at $P$ and $Q$; IIA transfers the result to $Q$. Crucially, the outsiders' rankings were selected according to $Q$. The conclusion is strong pair decisiveness, not merely decisiveness on another polarized profile.

The dual right-expansion construction gives decisiveness for $(c,b)$, keeping the second alternative fixed. Once these two pairs are decisive, replace the coalition members' ballots by $a\pref c\pref b$ while retaining outsiders' ballots. Transitivity and IIA give strong decisiveness for the original pair $(a,b)$ as well. The source then repeatedly applies these left and right expansion lemmas, with case distinctions when a target alternative coincides with one of the designated alternatives, to reach every ordered pair. No neutrality assumption is introduced.
\end{proof}
The implementation separates \code{weak\_\allowbreak{}expand\_\allowbreak{}left}, \code{weak\_\allowbreak{}expand\_\allowbreak{}right}, and \code{weak\_\allowbreak{}expand\_\allowbreak{}same}, then packages the result as \code{Arrow.\allowbreak{}Palomar.\allowbreak{}fieldExpansion}.

\subsection{Group contraction}
\begin{lemma}[Group contraction]\label{lem:contraction}
A decisive coalition with at least two members contains a strictly smaller nonempty decisive coalition.
\end{lemma}
\begin{proof}
Choose $v_1\in G$ and put $G_1=\{v_1\}$ and $G_2=G\setminus\{v_1\}$. Both are nonempty proper subsets of $G$. Using three distinct alternatives, construct the profile
\begin{center}
\begin{tabular}{ll}
\toprule
Voters & Restriction of $P$\\
\midrule
$G_1$ & $a\pref b\pref c$\\
$G_2$ & $c\pref a\pref b$\\
$V\setminus G$ & $b\pref c\pref a$\\
\bottomrule
\end{tabular}
\end{center}
All members of $G$ rank $a$ above $b$, hence $a\pref_{F(P)}b$. If $b\pref_{F(P)}c$, transitivity yields $a\pref_{F(P)}c$. At $P$, precisely the members of $G_1$ favor $a$ over $c$, while all outsiders favor $c$ over $a$. IIA extends this social comparison to every profile with that polarized comparison pattern. Thus $G_1$ is weakly decisive for $(a,c)$ and is fully decisive by Lemma~\ref{lem:expansion}.

In the other case, $c\pref_{F(P)}b$. At $P$, the members of $G_2$ favor $c$ over $b$ and all outsiders favor $b$ over $c$. IIA makes $G_2$ weakly decisive for $(c,b)$; field expansion again makes it decisive. Completeness of the social ballot supplies the exhaustive case split.
\end{proof}
The selected declaration \code{Arrow.\allowbreak{}Palomar.\allowbreak{}groupContraction} returns $G'\subsetneq G$, a proof that $G'$ is nonempty, and a proof that $G'$ is decisive. Strict containment is used to obtain the strict cardinality decrease.

\subsection{From contraction to a dictator}
Theorem~\ref{thm:arrow} uses strong induction on coalition cardinality, starting with $V$. Nonemptiness excludes the zero case. A coalition of cardinality one already gives a decisive singleton; a larger one contracts and invokes the induction hypothesis on a smaller cardinality.

If $\{d\}$ is decisive, $a\pref_{P_d}b$ implies $a\pref_{F(P)}b$. Conversely, if the social ballot ranks $a$ above $b$ but $d$ does not, strict completeness of $d$'s ballot gives $b\pref_{P_d}a$. Decisiveness would then give $b\pref_{F(P)}a$, contradicting asymmetry. Equal alternatives have neither comparison. This proves the full equivalence~\eqref{eq:arrowdictator}, not just a one-way implication.

\section{Strategy proofness and monotonicity}\label{sec:monotonicity}
The reduction begins with a consequence of strategy-proofness. For an alternative $a$, its lower contour in ballot $s$ is the set of alternatives ranked below $a$.

\begin{lemma}[Outcome monotonicity]\label{lem:monotone}
Let $f$ satisfy~\eqref{eq:sp}. Suppose $f(P)=a$ and
\begin{equation}\label{eq:lowercontour}
\forall v,b,\qquad a\pref_{P_v}b\ \Longrightarrow\ a\pref_{Q_v}b.
\end{equation}
Then $f(Q)=a$.
\end{lemma}
\begin{proof}
First suppose only voter $v$ changes ballot. If the new outcome is $b\ne a$, strategy-proofness at $P$ excludes $b\pref_{P_v}a$. Therefore $a\pref_{P_v}b$, and~\eqref{eq:lowercontour} gives $a\pref_{Q_v}b$. At the true profile $Q$, reporting the old ballot would obtain $a$ instead of $b$, contradicting strategy-proofness at $Q$.

For the general case, change voters' ballots one at a time. The electorate is finite, so this sequence reaches $Q$. At each intermediate profile, a voter's ballot is either its original or target ballot, and the same lower-contour preservation holds for the next update. The one-voter argument preserves the outcome throughout.
\end{proof}
These steps are \code{monotone\_\allowbreak{}one\_\allowbreak{}step} and \code{monotone} in \code{GS/\allowbreak{}Reduction.\allowbreak{}lean}. The finite update construction uses a list containing all voters.

\begin{lemma}[Unanimous top choice]\label{lem:topunanimity}
If $f$ is strategy-proof and onto, and $a$ is every voter's top alternative at $P$, then $f(P)=a$.
\end{lemma}
\begin{proof}
Onto supplies a profile $Q$ with $f(Q)=a$. Since $a$ is top at $P$, moving from $Q$ to $P$ preserves every comparison in which $a$ is above another alternative. Apply Lemma~\ref{lem:monotone}.
\end{proof}
This is \code{unanimous\_\allowbreak{}of\_\allowbreak{}sp\_\allowbreak{}onto}. Onto is used to obtain the starting profile; strategy-proofness transports its choice. It is not an additional unanimity hypothesis in Theorem~\ref{thm:gs}.

\section{From pair tests to a strict social order}\label{sec:order}
\subsection{The top two transformation}
For distinct $a,b$, let $T_{ab}(P)$ put $a$ and $b$ in the first two positions of every ballot, preserving that voter's original comparison between them. Its numerical construction assigns the preferred member score $0$, the other score $1$, and every other alternative $c$ score $P_v(c)+2$. Thus
\begin{align}
 a\pref_{T_{ab}(P)_v}b&\ \Longleftrightarrow\ a\pref_{P_v}b,\label{eq:tpair}\\
 a\pref_{T_{ab}(P)_v}c\text{ and }b\pref_{T_{ab}(P)_v}c
 &\quad(c\notin\{a,b\}).\label{eq:trest}
\end{align}
The score assignment is injective. The source defines \code{topTwoProfile} and proves these properties as \code{topTwo\_\allowbreak{}preserves} and \code{topTwo\_\allowbreak{}above\_\allowbreak{}rest}. It also proves $T_{ab}(P)=T_{ba}(P)$; writing the pair in the opposite order does not change the ballot transformation.

\begin{lemma}[Range of a top two test]\label{lem:toprange}
For a strategy-proof onto rule, $f(T_{ab}(P))\in\{a,b\}$.
\end{lemma}
\begin{proof}
Suppose instead it selects $c\notin\{a,b\}$. Promote $a$ alone to the top of every ballot while keeping the order among other alternatives. Every voter already ranks $a$ above $c$, so this promotion cannot remove any alternative from $c$'s lower contour. Monotonicity therefore preserves outcome $c$. But the new profile has unanimous top choice $a$, forcing outcome $a$ by Lemma~\ref{lem:topunanimity}, a contradiction.
\end{proof}
The analogous construction with three designated alternatives gives a three-top profile whose outcome lies among those three. The proof has the same lower-contour argument. Both range claims use onto through unanimous-top choice.

\subsection{Pairwise comparison and independence}
Define
\begin{equation}\label{eq:beats}
a\triangleright_P b\quad\Longleftrightarrow\quad
 a\ne b\ \text{ and }\ f(T_{ab}(P))=a.
\end{equation}
This is \code{beats f P a b}. It is irreflexive by definition. Symmetry of the top-two transformation and single-valued choice imply asymmetry. Lemma~\ref{lem:toprange} supplies totality: for distinct $a,b$, exactly one of $a\triangleright_P b$ and $b\triangleright_P a$ holds.

\begin{lemma}[Pairwise independence]\label{lem:pairiia}
If every voter has the same comparison of $a,b$ at $P$ and $Q$, then
$a\triangleright_P b\Longleftrightarrow a\triangleright_Q b$.
\end{lemma}
\begin{proof}
Suppose $f(T_{ab}(P))=a$. In the move from $T_{ab}(P)$ to $T_{ab}(Q)$, $a$ remains above all alternatives outside the pair. Its comparison with $b$ is also unchanged by hypothesis and~\eqref{eq:tpair}. Thus its lower contour is preserved, and monotonicity gives $f(T_{ab}(Q))=a$. Interchange $P$ and $Q$ for the reverse implication.
\end{proof}
This is \code{pairwise\_\allowbreak{}IIA}. The residual ballots need not be identical: monotonicity makes their differences irrelevant to this pair test. Onto is not needed for this lemma itself.

\subsection{Why there are no cycles}
Totality and asymmetry alone allow a tournament with cycles. The source establishes transitivity by using one profile that puts three alternatives jointly above the rest.

For distinct $a,b,c$, the three-top profile $U_{abc}(P)$ preserves all original comparisons among them. The score of a designated alternative is the number of the other two ranked above it; these scores are $0,1,2$ in some order. Every other alternative $w$ receives $P_v(w)+3$. This is an injective ballot, and it preserves each designated pair comparison. The auxiliary lemma \code{predCount\_\allowbreak{}lt} verifies the elementary three-score comparison used in the construction.

\begin{lemma}[Transitivity]\label{lem:beatstrans}
If $a\triangleright_P b$ and $b\triangleright_P c$, then $a\triangleright_P c$.
\end{lemma}
\begin{proof}
The hypotheses imply $a\ne b$ and $b\ne c$; asymmetry rules out $a=c$. Put $Q=U_{abc}(P)$. Pairwise independence transfers the two hypotheses to $Q$. The three-top range lemma gives $f(Q)\in\{a,b,c\}$.

If $f(Q)=b$, move to $T_{ab}(Q)$. This move preserves $b$'s lower contour: its relation to $a$ is unchanged and all alternatives outside the pair are now below it. Monotonicity would give $f(T_{ab}(Q))=b$, contrary to $a\triangleright_Q b$. Similarly $f(Q)=c$ would force $f(T_{bc}(Q))=c$, contrary to $b\triangleright_Q c$. Therefore $f(Q)=a$.

Moving from $Q$ to $T_{ac}(Q)$ preserves $a$'s lower contour, so the latter profile selects $a$. Hence $a\triangleright_Q c$. Pairwise independence, using the preserved $a,c$ comparisons, transfers this conclusion back to $P$.
\end{proof}
This is \code{beats\_\allowbreak{}trans} in \code{GS/\allowbreak{}SWF.\allowbreak{}lean}. Its explicit distinctness binders are sufficient because repeated alternatives are excluded by irreflexivity and asymmetry. Consequently $\triangleright_P$ is a strict total order for every profile. This order property is proved before numerical social ranks are introduced.

\section{Predecessor counts and the application of Arrow}\label{sec:counts}
\subsection{Encoding the order as a ballot}
For each alternative define
\begin{equation}\label{eq:score}
\Pred_P(a)=\{c\in A:c\triangleright_P a\},
\qquad r_P(a)=|\Pred_P(a)|.
\end{equation}
The implementation calls $r_P$ \code{copelandScore}, but here it counts predecessors in the already proved strict total order. It does not aggregate voters by a Copeland voting rule, and it does not repair a cyclic relation by scoring it.

\begin{proposition}[Order representation]\label{prop:count}
For distinct $a,b$,
\begin{equation}\label{eq:countspec}
a\triangleright_P b\quad\Longleftrightarrow\quad r_P(a)<r_P(b).
\end{equation}
In particular, $r_P:A\to\Nat$ is injective.
\end{proposition}
\begin{proof}
If $a\triangleright_P b$, transitivity implies $\Pred_P(a)\subseteq\Pred_P(b)$. The containment is strict because $a\in\Pred_P(b)$ but $a\notin\Pred_P(a)$. Finiteness gives $r_P(a)<r_P(b)$. Conversely, if this inequality holds, totality excludes $b\triangleright_P a$, which would give the opposite strict inequality. Hence $a\triangleright_P b$. For injectivity, any two distinct alternatives are ordered one way or the other and so have distinct predecessor counts.
\end{proof}
The strict inequality is proved as \code{copeland\_\allowbreak{}lt\_\allowbreak{}of\_\allowbreak{}beats}. The injectivity theorem is \code{copelandScore\_\allowbreak{}injective}. The source then defines
\begin{equation}\label{eq:swf}
F_f(P)=\langle r_P,\text{ proof of injectivity}\rangle\in\Ballot(A).
\end{equation}
This is \code{swfOfSCF f hSP hO}. The characterization \code{swfOfSCF\_\allowbreak{}spec} states exactly that the social ballot ranks $a$ above $b$ if and only if $a\triangleright_P b$. At this point, and only at this point, the construction has the required social-welfare codomain.

\subsection{The two Arrow axioms}
Unanimity of $F_f$ follows directly from a unanimous pair comparison. If every voter ranks $a$ above $b$ at $P$, then $a$ is top in every ballot of $T_{ab}(P)$. Lemma~\ref{lem:topunanimity} gives $f(T_{ab}(P))=a$, hence $a\triangleright_P b$ and therefore $a\pref_{F_f(P)}b$ by~\eqref{eq:countspec}. The code supplies this through \code{beats\_\allowbreak{}of\_\allowbreak{}unanimous} and \code{swfOfSCF\_\allowbreak{}unanimous}. Its proof uses an intermediate unanimous-top profile and monotonicity to reach the top-two profile, with the same conclusion.

IIA of $F_f$ is Lemma~\ref{lem:pairiia} translated through~\eqref{eq:countspec}, and is proved as \code{swfOfSCF\_\allowbreak{}IIA}. Equal alternatives are handled separately using irreflexivity. Therefore Theorem~\ref{thm:arrow} applies to the actual injective ballot-valued function~\eqref{eq:swf} and yields a voter $d$ whose pairwise ranking agrees with $F_f$ at every profile.

\subsection{Transferring the dictator back to choice}
Fix $P$ and put $a=f(P)$. Suppose some $b\ne a$ is ranked above $a$ by $d$. Arrow dictatorship and the social-ranking characterization imply $b\triangleright_P a$, so
\[
f(T_{ba}(P))=b.
\]
On the other hand, moving from $P$ to $T_{ba}(P)$ preserves $a$'s lower contour. Its comparison with $b$ is retained, and all other alternatives are below $a$ in the new profile. Monotonicity, starting from $f(P)=a$, therefore gives
\[
f(T_{ba}(P))=a,
\]
a contradiction. Thus no alternative is above $f(P)$ in $d$'s ballot. Strict completeness gives~\eqref{eq:gsdictator} for every other alternative. This proves Theorem~\ref{thm:gs}. No extra onto assumption is imposed on the constructed welfare function, and no restriction to top-two profiles is imposed on the final dictatorship conclusion.

\section{Source structure and verification boundary}\label{sec:verification}
\subsection{Modules and dependency identity}
The Arrow proof is organized into \code{Arrow/\allowbreak{}Basic.\allowbreak{}lean}, \code{Arrow/\allowbreak{}FieldExpansion.\allowbreak{}lean}, \code{Arrow/\allowbreak{}GroupContraction.\allowbreak{}lean}, and \code{Arrow/\allowbreak{}ArrowTheorem.\allowbreak{}lean}. The Gibbard--Satterthwaite repository vendors those same four files. A byte comparison at the two stated pins finds them identical. Its Lake file declares a local \code{Arrow} library alongside the \code{GibbardSatterthwaite} library; Arrow is not a separate fetched Lake package.

The extension's dependency chain is \code{GS/\allowbreak{}Basic.\allowbreak{}lean}, \code{GS/\allowbreak{}Reduction.\allowbreak{}lean}, \code{GS/\allowbreak{}SWF.\allowbreak{}lean}, and \code{GS/\allowbreak{}Main.\allowbreak{}lean}. The first reuses \code{Arrow.\allowbreak{}Basic}; the last imports both \code{GS.\allowbreak{}SWF} and \code{Arrow.\allowbreak{}ArrowTheorem}. Although the README broadly locates the reduction in \code{GS/\allowbreak{}Reduction.\allowbreak{}lean}, that file proves monotonicity and unanimous-top choice. The social order and rank construction are in \code{GS/\allowbreak{}SWF.\allowbreak{}lean}; the Arrow axioms, invocation, and dictatorship transfer are in \code{GS/\allowbreak{}Main.\allowbreak{}lean}. This division follows the source files, not the abbreviated README description.

Both manifests pin Mathlib to
\begin{center}\small
\texttt{065356127b1dc0016f66b7283ce0ce2c4055aa55}.
\end{center}
The remaining manifest packages are Mathlib's supporting Lean packages. The vendored Arrow copy and the Mathlib dependency have different roles: the former is substantive source developed by the same maintainer; the latter supplies the general finite-set, order, equivalence, and tactic infrastructure.

\subsection{Challenge and solution separation}
Each \code{Challenge.\allowbreak{}lean} is a self-contained statement module importing only \code{Mathlib.\allowbreak{}Data.\allowbreak{}Finset.\allowbreak{}Basic} and \code{Mathlib.\allowbreak{}Data.\allowbreak{}Fintype.\allowbreak{}EquivFin}. Arrow's Challenge contains four deliberate statement holes, one per selected theorem; Gibbard--Satterthwaite's contains one. These are the problems to be compared with the implementations, not proofs of the results.

The GS Challenge defines its own support vocabulary for ballots and profiles, while the implementation reuses \code{Arrow.\allowbreak{}Basic}. Its comparator selects the four choice concepts and the final theorem; it does not separately select every support definition. Arrow's comparator selects nine definitions and four theorems; \code{WeakDecisive} occurs in its statement but is not a separately selected definition.

Each \code{Solution.\allowbreak{}lean} imports the final implementation module. Neither solution imports its Challenge. The selected proved declarations are reached through that implementation import closure. At the inspected pins, a lexical scan of the substantive Arrow and GS modules and both solution wrappers finds no proof placeholders, custom \code{axiom} declarations, or \code{unsafe} declarations. This scan is a source observation, not a substitute for elaboration or a transitive axiom audit.

The registry configurations permit \code{propext}, \code{Quot.\allowbreak{}sound}, and \code{Classical.\allowbreak{}choice}. The source uses classical selection, including choosing a finite enumeration and top alternatives. The paper therefore makes no claim of a constructive or executable decision algorithm extracted from these proofs. The repositories contain axiom-audit scripts, but their presence alone does not establish that a new audit has been run.

\subsection{Historical checks and present checks}
Palomar records historical verification on September 25, 2026, under the stated Lean toolchain. The Arrow record reports verification at 18:26:09 UTC and registration at 19:02:37 UTC, with workflow run \href{https://github.com/PalomarRegistry/PalomarSubmission/actions/runs/36171797049}{36171797049}. The Gibbard--Satterthwaite record reports verification at 20:43:00 UTC and registration at 21:11:21 UTC, with workflow run \href{https://github.com/PalomarRegistry/PalomarSubmission/actions/runs/36187074973}{36187074973}. Both records include comparator configuration, permitted axioms, dependency pins, file hashes, preservation receipts, and independent-kernel tool identities \cite{palomarArrow,palomarGS}.

For this manuscript we retrieved both exact repository snapshots, read the substantive proofs and theorem interfaces, compared the vendored Arrow files, checked manifest and toolchain identities, and matched both Challenge and both Solution SHA-256 hashes against the immutable registry records. We also reviewed the mathematical exposition and bibliographic references independently of the initial drafting pass. We did not execute a fresh Lean build or a fresh kernel/axiom audit in this preparation environment, where Lean and Lake were unavailable. The September 25 verification is historical evidence associated with the pinned artifacts. Compilation of the present \LaTeX{} manuscript, source comparison, and mathematical source review are distinct checks and are not described as fresh formal verification or human peer review.

\section{Attribution and limitations}\label{sec:provenance}
The source mathematics belongs to Arrow, Gibbard, and Satterthwaite \cite{arrow1950,gibbard1973,satterthwaite1975}. Earlier machine-checked work includes Nipkow's Isabelle/HOL development of both theorems \cite{nipkow2009}. The independent Roos record concerns a three-candidate Fourier-analytic Arrow proof, whereas the inspected Arrow artifact follows decisive coalitions for any finite alternative set with three distinct members \cite{roos2026,palomarArrow}. These are differences in proof route and formal statement, not a claim that the current development originated the general theorem.

The pinned repository and registry metadata credit Arthur Freitas Ramos as the author and responsible maintainer of the Lean developments. That source attribution is separate from the three-author byline of this manuscript. Both repositories are BSD-3-Clause; Mathlib is a dependency with its own Apache-2.0 license. The manuscript's CC BY 4.0 license does not relicense those source artifacts. The bibliography cites and links the existing work; the prose and displayed proofs here are a newly prepared exposition rather than a republication of a supplied journal manuscript.

One source-metadata correction is recorded explicitly. The pinned Gibbard--Satterthwaite metadata cites Satterthwaite's intended 1975 title with DOI \code{10.\allowbreak{}1016/\allowbreak{}0022-0531(75)90002-6}. The publisher identifies that title as \code{10.\allowbreak{}1016/\allowbreak{}0022-0531(75)90050-2}, which is the DOI used in our bibliography \cite{satterthwaite1975}. This bibliographic correction changes neither the pinned code nor its theorem statements. Likewise, a dated search that found no earlier Gibbard--Satterthwaite entry in Palomar would not establish absence of earlier formalizations elsewhere; we make no such inference.

\paragraph{AI assistance.}
This manuscript was prepared with GPT-6.1 assistance for exposition, source alignment, and review. The formalization metadata separately records proof-engineering assistance by \code{gpt-6-luna} via the Codex CLI. These are distinct provenance claims: the manuscript-generation model is not substituted for the model recorded by the source repositories. AI-assisted review and mechanical proof checking do not establish comprehensive human understanding, source-author endorsement, or independent human peer review.

The verified scope is finite strict-ranking social choice. Broader variants with weak preferences or infinite electorates require different statements and are not supplied by these artifacts. The value of the present development is its explicit proof interface: auxiliary ballots satisfy the domain, coalition contraction terminates by finite cardinality, the strategy-proof reduction really constructs an injective social ballot, and the final conclusions match the declared pairwise and top-choice notions of dictatorship.

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