VotingParadoxesCert
plain-language theorem explainer
The structure certifies that Arrow's three conditions match the three binary axes of the D=3 lattice and that the only voting rule satisfying all three simultaneously is the dictatorial rule. Decision theorists and sociologists working inside the Recognition Science framework cite it when deriving classical voting impossibilities from sigma conservation. It is assembled directly as a structure whose two fields record the cardinality of the ArrowCondition inductive type and the uniqueness statement for admissible rules.
Claim. Let $A$ be the set of Arrow conditions with $|A|=3$. A voting rule $r$ satisfies the admissible predicate if its three Boolean flags for unrestricted domain, Pareto efficiency, and independence of irrelevant alternatives are all true. Then the only such rule is the dictatorial rule (all flags true).
background
In this module the three classical voting impossibilities are derived from sigma conservation on the D=3 lattice. ArrowCondition is the inductive type whose three constructors unrestrictedDomain, paretoEfficiency, and iia label the binary axes of F₂³. VotingRuleSignature is the structure carrying the three corresponding Boolean flags, while IsArrowAdmissible asserts that all three flags are true. The dictatorship constant is the rule with every flag set to true. The module doc states that Arrow's conditions are the three independent axis constraints and that the only element satisfying all three is the zero baseline, yielding the |F₂³ minus {0}| = 7 structure.
proof idea
This is a structure definition with an empty proof body. The first field is the direct cardinality statement Fintype.card ArrowCondition = 3, which follows from the inductive type having exactly three constructors. The second field is the universal statement that every rule satisfying IsArrowAdmissible equals dictatorship, which is the encoded form of Arrow's theorem.
why it matters
The certificate supplies the sociology content for the VotingParadoxesCert structure instantiated in both the Decision and Sociology modules, completing the passage from J-cost to sigma conservation for social choice. It realizes the RS claim that Arrow's impossibility is the |F₂³ minus {0}| = 7 structure forced by the three axis constraints in D=3. The module doc identifies this as the formal statement that no non-dictatorial rule satisfies all three conditions. It leaves open the explicit derivation of Condorcet and Gibbard-Satterthwaite results inside the same lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.