Read-back: gibbard_satterthwaite

Setting

Let $A$ and $\iota$ be arbitrary types, both assumed finite (each carries a Fintype instance), with equality on $\iota$ decidable. Elements of $A$ play the role of alternatives; elements of $\iota$ play the role of voters. There is one explicit cardinality hypothesis:

$$2 < |A|,$$

i.e. $A$ has at least three elements. No cardinality assumption is made on $\iota$: the statement's hypotheses admit $\iota$ empty, a single voter, or any finite number of voters.

A ballot is any binary relation $r$ on $A$ (a function $A \to A \to \mathrm{Prop}$, i.e. an arbitrary relation — not a priori an order of any kind). A profile is any function $P$ assigning to each voter $i$ a relation $P_i$ on $A$. Write $P_i(a,b)$ for the statement that the relation $P_i$ holds of the pair $(a,b)$; the code attaches no intrinsic meaning ("prefers", "above") to this — it is just a binary relation.

The predicate "$P$ is a preference profile" (IsPrefProfile P) unfolds to: for every voter $i$, the relation $P_i$ is a strict total order on $A$, where "strict total order" is Mathlib's IsStrictTotalOrder: $P_i$ is irreflexive ($\neg P_i(a,a)$ for all $a$), transitive, and trichotomous (for all $a, b$: $P_i(a,b)$ or $a = b$ or $P_i(b,a)$).

The object under study is a function

$$f : (\text{profiles}) \to A,$$

defined on all functions $\iota \to (A \to A \to \mathrm{Prop})$ — including profiles whose component relations are not strict total orders, or are not orders at all. The hypotheses below constrain $f$ only on (or via) profiles built from strict total orders; on arbitrary relation-profiles $f$ may take any value.

For a profile $P$, a voter $i$, and a relation $r'$, write $P[i \mapsto r']$ for the profile that agrees with $P$ at every voter except $i$, where it is $r'$ (this is Function.update). When $P$ is a preference profile and $r'$ is a strict total order, $P[i \mapsto r']$ is again a preference profile, though the statement never needs to say so explicitly.

Hypotheses on $f$

Hypothesis 1 — IncentiveCompatible f, unfolded: for every profile $P$ such that every $P_i$ is a strict total order, for every voter $i$, and for every relation $r'$ on $A$ that is itself a strict total order,

$$\neg\, P_i\bigl(\, f(P[i \mapsto r']),\; f(P) \,\bigr).$$

In words: the relation $P_i$ (voter $i$'s relation in the original profile) does not hold of the pair whose first component is the outcome of $f$ on the deviated profile $P[i \mapsto r']$ and whose second component is the outcome of $f$ on the original profile $P$. Note the precise shape: this is a plain negation, quantified only over deviations $r'$ that are strict total orders (deviations to non-order relations are unconstrained), and it constrains the pair in one direction only — nothing is asserted about $P_i\bigl(f(P), f(P[i \mapsto r'])\bigr)$ beyond what trichotomy of $P_i$ would give. In particular, taking $r' = P_i$ the hypothesis yields $\neg P_i(f(P), f(P))$, which is automatic from irreflexivity.

Hypothesis 2 — SCFOnto f, unfolded: for every alternative $a \in A$ there exists a profile $P$ such that every $P_i$ is a strict total order and $f(P) = a$. That is, $f$ attains every element of $A$ already on preference profiles (attaining values on non-order profiles does not count toward this hypothesis).

Conclusion

There exists a voter $i \in \iota$ such that SCFDictator f i holds, which unfolds to: for every profile $P$ in which every voter's relation is a strict total order, and for every alternative $a$,

$$\Bigl(\forall\, b \neq a,\; P_i(a, b)\Bigr) \;\Longrightarrow\; f(P) = a.$$

In words: whenever alternative $a$ is $P_i$-related to every other alternative — i.e. $a$ is the (necessarily unique, by irreflexivity) element that relation $P_i$ places above all others, which for a strict total order on a nonempty finite $A$ always exists — the outcome is $a$. Note this dictatorship notion says nothing directly about pairwise comparisons or about profiles that are not preference profiles; it is stated purely as an implication, one profile at a time, from "$a$ dominates everything else under $P_i$" to "$f$ selects $a$". The existential is a plain $\exists$, not unique existence: nothing asserts the dictator is unique.

Edge cases the quantifiers silently include

• Zero voters. Fintype ι permits $\iota = \emptyset$. Then there is exactly one profile (the empty function), it is vacuously a preference profile, and incentive compatibility is vacuously true. But ontoness then demands that a single value $f(P)$ equal every one of the $\geq 3$ alternatives, which is impossible; so with zero voters the hypotheses are contradictory and the conclusion $\exists i \in \emptyset, \ldots$ (which would otherwise be false) holds vacuously. The theorem therefore implicitly asserts that its hypotheses force $\iota$ to be nonempty.
• One voter. $|\iota| = 1$ is allowed and non-degenerate: the claim then says that single voter is a dictator.
• $|A| = 3$ exactly is allowed ($2 < |A|$ is strict); $|A| \le 2$ is excluded by hypothesis, and $A$ empty or a singleton is likewise excluded.
• Totality of $f$. Since $f$ is total on all relation-profiles, its values on "junk" inputs (non-order relations) exist but are never constrained or consulted by any hypothesis or by the conclusion.
• All three properties — incentive compatibility, ontoness, dictatorship — quantify only over profiles of strict total orders; ties/indifference are not representable within the constrained inputs, and no hypothesis mentions them.