IsArrowAdmissible
plain-language theorem explainer
A definition identifying voting rules that meet all three Arrow conditions simultaneously: unrestricted domain, Pareto efficiency, and independence of irrelevant alternatives. Social choice theorists cite it when embedding Arrow's impossibility into the Recognition Science F₂³ lattice model. The definition is realized as a direct conjunction of the three Boolean fields carried by the VotingRuleSignature structure.
Claim. A voting rule $r$ is Arrow-admissible when it satisfies unrestricted domain, Pareto efficiency, and independence of irrelevant alternatives.
background
The module recasts Arrow's 1951 impossibility theorem using the three binary axes of the vector space F₂³, which corresponds to the D=3 spatial dimensions in the Recognition Science forcing chain. The structure VotingRuleSignature records the satisfaction of each condition as a Boolean: unrestrictedDomain, paretoEfficiency, and iia. IsArrowAdmissible selects the subset of rules for which all three hold.
proof idea
The definition is a one-line wrapper that returns the conjunction of the three Boolean components from the VotingRuleSignature input.
why it matters
It supplies the predicate used by the theorem arrow_dictatorship_only to establish that only the dictatorship satisfies the conditions, and by the VotingParadoxesCert structure to certify the uniqueness result. This fills the Arrow impossibility step in the F10 module, linking the three conditions to the axes of F₂³ and confirming that non-dictatorial rules must violate at least one, consistent with the |F₂³ ∖ {0}| = 7 structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.