Individual Rationality and Majority Cycles

Abstract

Complete transitive individual rankings can aggregate into a nontransitive majority cycle with no faithful scalar order.

Theorem 1.1 (Individually rational rankings produce a collective cycle).

$$(\forall v\in \mathrm{Fin}\left(3\right),x\in \mathrm{Fin}\left(3\right),y\in \mathrm{Fin}\left(3\right),z\in \mathrm{Fin}\left(3\right),\left(\mathrm{prefers}\left(v,x,y\right)\wedge \mathrm{prefers}\left(v,y,z\right)\right)\Rightarrow \mathrm{prefers}\left(v,x,z\right))\wedge \left((\forall v\in \mathrm{Fin}\left(3\right),x\in \mathrm{Fin}\left(3\right),y\in \mathrm{Fin}\left(3\right),\left(\neg x=y\right)\Rightarrow \left(\mathrm{prefers}\left(v,x,y\right)\vee \mathrm{prefers}\left(v,y,x\right)\right))\wedge \left(\left(\mathrm{majorityPrefers}\left(0,1\right)\wedge \left(\mathrm{majorityPrefers}\left(1,2\right)\wedge \mathrm{majorityPrefers}\left(2,0\right)\right)\right)\wedge \left(\left(\neg \mathrm{Transitive}\left(majorityPrefers\right)\right)\wedge \left(\neg \left(\exists u\in \mathrm{Fin}\left(3\right)\to \mathbb{R},\forall x\in \mathrm{Fin}\left(3\right),y\in \mathrm{Fin}\left(3\right),\mathrm{majorityPrefers}\left(x,y\right)\Rightarrow u\left(x\right)>u\left(y\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Aggregation/IndividualRationalityMajorityCycle.individual_rationality_majority_cycle (✓ std3). ∎

Source. Repository-derived.

Commentary.

The fixed profile ranks the three candidates cyclically across three voters. Every individual strict preference is transitive and complete on distinct candidates.

Pairwise counting makes zero beat one, one beat two, and two beat zero. Those public edges directly contradict transitivity of the majority relation, and the imported cycle obstruction excludes every faithful real-valued ordering.

References

• Truth anchor: D5/S3/ConceptDynamics/Aggregation/IndividualRationalityMajorityCycle.individual_rationality_majority_cycle
• Dependency: D5/S3/ConceptDynamics/Aggregation/MajorityCycleNotScalarOrder