@article{arrow1950,
 author={Arrow, Kenneth J.}, title={A Difficulty in the Concept of Social Welfare},
 journal={Journal of Political Economy}, volume={58}, number={4}, pages={328--346},
 year={1950}, doi={10.1086/256963}, url={https://doi.org/10.1086/256963}
,
 note={\url{https://doi.org/10.1086/256963}}
}
@article{gibbard1973,
 author={Gibbard, Allan}, title={Manipulation of Voting Schemes: A General Result},
 journal={Econometrica}, volume={41}, number={4}, pages={587--601}, year={1973},
 doi={10.2307/1914083}, url={https://doi.org/10.2307/1914083}
,
 note={\url{https://doi.org/10.2307/1914083}}
}
@article{satterthwaite1975,
 author={Satterthwaite, Mark A.},
 title={Strategy-proofness and {Arrow}'s conditions: Existence and correspondence theorems for voting procedures and social welfare functions},
 journal={Journal of Economic Theory}, volume={10}, number={2}, pages={187--217}, year={1975},
 doi={10.1016/0022-0531(75)90050-2}, url={https://doi.org/10.1016/0022-0531(75)90050-2}
,
 note={\url{https://doi.org/10.1016/0022-0531(75)90050-2}}
}
@article{nipkow2009,
 author={Nipkow, Tobias}, title={Social Choice Theory in {HOL}: {Arrow} and {Gibbard--Satterthwaite}},
 journal={Journal of Automated Reasoning}, volume={43}, number={3}, pages={289--304}, year={2009},
 doi={10.1007/s10817-009-9147-4}, url={https://doi.org/10.1007/s10817-009-9147-4}
,
 note={\url{https://doi.org/10.1007/s10817-009-9147-4}}
}
@misc{ramosArrow,
 author={Ramos, Arthur Freitas}, title={{Arrow}'s Impossibility Theorem in {Lean} 4}, year={2026},
 note={Pinned repository snapshot. BSD-3-Clause \url{https://github.com/Arthur742Ramos/arrow-impossibility-lean/tree/4f405d27d0b244574bbee5d3d79bae0c66bda16e}},
 url={https://github.com/Arthur742Ramos/arrow-impossibility-lean/tree/4f405d27d0b244574bbee5d3d79bae0c66bda16e}
}
@misc{ramosGS,
 author={Ramos, Arthur Freitas}, title={{Gibbard--Satterthwaite} Theorem in {Lean} 4}, year={2026},
 note={Pinned repository snapshot. BSD-3-Clause \url{https://github.com/Arthur742Ramos/gibbard-satterthwaite-lean/tree/8398e65a99cd3d5e973c64963c4bab8c0491947c}},
 url={https://github.com/Arthur742Ramos/gibbard-satterthwaite-lean/tree/8398e65a99cd3d5e973c64963c4bab8c0491947c}
}
@misc{palomarArrow,
 author={{Palomar Registry}}, title={{Arrow}'s impossibility theorem (general finite version)}, year={2026},
 note={PALOMAR-2026-09-25-000024, version 1. Registered September 25, 2026 \url{https://palomar-registry.org/entry?id=PALOMAR-2026-09-25-000024&version=1}},
 url={https://palomar-registry.org/entry?id=PALOMAR-2026-09-25-000024&version=1}
}
@misc{palomarGS,
 author={{Palomar Registry}}, title={{Gibbard--Satterthwaite} theorem (strategy-proof social choice)}, year={2026},
 note={PALOMAR-2026-09-25-000028, version 1. Registered September 25, 2026 \url{https://palomar-registry.org/entry?id=PALOMAR-2026-09-25-000028&version=1}},
 url={https://palomar-registry.org/entry?id=PALOMAR-2026-09-25-000028&version=1}
}
@misc{roos2026,
 author={Roos, Joris}, title={{Arrow}'s theorem via {Fourier} analysis}, year={2026},
 note={Palomar record PALOMAR-2026-09-01-000011, version 1 \url{https://palomar-registry.org/entry?id=PALOMAR-2026-09-01-000011&version=1}},
 url={https://palomar-registry.org/entry?id=PALOMAR-2026-09-01-000011&version=1}
}

@misc{peters2026,
 author={Peters, Dominik}, title={{SocialChoiceLean}: {Gibbard--Satterthwaite} in {Lean}}, year={2026},
 note={Public repository snapshot, July 21, 2026. Consulted as source; not rebuilt for this manuscript \url{https://github.com/DominikPeters/SocialChoiceLean/tree/94a4c650b6a3ef14df801a613c3b46169dbd754d}},
 url={https://github.com/DominikPeters/SocialChoiceLean/tree/94a4c650b6a3ef14df801a613c3b46169dbd754d}
}