arrow_dictatorship_only
plain-language theorem explainer
Arrow's impossibility theorem is formalized as the claim that the only voting rule meeting unrestricted domain, Pareto efficiency, and independence of irrelevant alternatives is the dictatorship. Social choice theorists and formal verification researchers cite this when embedding Arrow's result inside the sigma-conservation lattice. The proof is a direct structural decomposition that matches the three condition flags to the dictatorship definition.
Claim. Let $r$ be a voting rule with Boolean fields for unrestricted domain, Pareto efficiency, and independence of irrelevant alternatives. If all three fields are true, then $r$ equals the dictatorial rule whose fields are all true.
background
A VotingRuleSignature records the three Boolean flags for the Arrow conditions. IsArrowAdmissible holds exactly when the conjunction of those flags is true. The dictatorship is the concrete signature with every flag set to true. This sits inside the module on voting paradoxes from sigma conservation, which maps the three conditions to the three binary axes of the F₂³ lattice and identifies the impossibility with the fact that only the zero element satisfies all boundary constraints simultaneously.
proof idea
The term proof introduces the three components of the rule and the three conjuncts of the admissibility hypothesis. Simplification against the definitions of dictatorship and IsArrowAdmissible reduces both sides to the identical triple of true values. Exact matching of the components then yields equality.
why it matters
The result supplies the uniqueness half of the votingParadoxesCert certificate, which packages the three conditions together with dictatorship uniqueness. It realizes the module claim that Arrow's impossibility follows from the |F₂³ minus zero| = 7 structure on the D=3 lattice. Within Recognition Science it closes the formalization that every non-dictatorial rule violates at least one axis constraint.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.