Grand Coalition Is Decisive under Unanimity
Theorem. If a social welfare function $F$ ([[social_choice.voting.swf]]) satisfies unanimity ([[social_choice.voting.unanimity]]), then the grand coalition $N \subseteq N$ is decisive for $F$ ([[social_choice.voting.is_decisive]]).
Proof
Unanimity says: if every voter strictly prefers $a$ to $b$, society does too. Specialising the universal quantifier in $\mathrm{IsDecisive}$ to the universal coalition gives exactly that statement. $\square$
In Lean: SocialChoice.Voting.unanimity_univ_isDecisive.
This is the base case of the decisive-coalition proof of Arrow's theorem ([[social_choice.voting.arrow_of_unanimity_iia]]): start from the trivially decisive grand coalition, then shrink it in cardinality using [[social_choice.voting.decisive_contraction]] until you reach a singleton dictator.
References
- [MSZ Chapter 21] Maschler, Solan, and Zamir, Game Theory. Decisive-coalitions proof of Arrow.