VotingRuleSignature
plain-language theorem explainer
A structure that encodes any voting rule by the subset of Arrow's three conditions it satisfies, represented as booleans for unrestricted domain, Pareto efficiency, and independence of irrelevant alternatives. Social choice theorists working inside the Recognition Science lattice model cite it to formalize the F₂³ derivation of Arrow's impossibility. The declaration is a direct structure definition with three fields and deriving clauses for decidability and finiteness.
Claim. A voting rule is a triple $(u,p,i)∈{0,1}^3$ where $u$ records satisfaction of unrestricted domain, $p$ records Pareto efficiency, and $i$ records independence of irrelevant alternatives.
background
The module recasts Arrow's 1951 theorem inside the Recognition Science framework by identifying the three conditions with the coordinate axes of the vector space F₂³, whose dimension equals the spatial dimension D=3. Only the zero vector satisfies all three axis constraints at once; the remaining seven vectors each violate at least one constraint, reproducing the classical impossibility. Upstream sibling modules supply seven-element enumerations (plot families, kinship systems, ore classes, musical modes) that mirror the seven non-zero elements of F₂³.
proof idea
The declaration is a structure definition that introduces the three boolean fields and attaches deriving instances for DecidableEq, BEq, Repr, and Fintype.
why it matters
It supplies the carrier type for the downstream theorems arrow_dictatorship_only and VotingParadoxesCert, which state that only the dictatorship satisfies all three conditions. The definition thereby realizes the module claim that Arrow's impossibility is the statement that no non-zero element of F₂³ meets every boundary condition, directly linking the result to the D=3 lattice and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.