dictatorship
plain-language theorem explainer
The dictatorship definition encodes the voting rule satisfying all three Arrow conditions by setting unrestricted domain, Pareto efficiency, and independence of irrelevant alternatives to true. Social choice theorists and Recognition Science modelers cite it when recasting Arrow's impossibility as the sole zero element in the F₂³ lattice. It is a direct structure constructor with all Boolean flags enabled.
Claim. The dictatorial voting rule is the signature element satisfying unrestricted domain, Pareto efficiency, and independence of irrelevant alternatives, written as the structure instance with all three fields true.
background
The module recasts Arrow's 1951 impossibility, Condorcet's paradox, and Gibbard-Satterthwaite as consequences of sigma conservation on the D=3 lattice F₂³. A VotingRuleSignature is the structure with three Boolean fields recording satisfaction of unrestricted domain, Pareto efficiency, and independence of irrelevant alternatives. The dictatorship is defined as the rule meeting every field, corresponding to the zero baseline element.
proof idea
This is a one-line wrapper that applies the VotingRuleSignature structure constructor with all three fields set to true.
why it matters
This definition supplies the baseline for the theorem arrow_dictatorship_only proving only the dictatorship satisfies all three conditions, which is the formal statement of Arrow's theorem. It fills the F10 step by exhibiting the |F₂³ minus zero| = 7 structure that forces at least one violation for any non-dictatorial rule. It is referenced in VotingParadoxesCert to certify the three conditions and the uniqueness claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.