three_conditions_match_D
plain-language theorem explainer
The declaration establishes that Arrow's three conditions form a set of exact cardinality three, matching the three binary axes of the F₂³ lattice in the D=3 structure. Voting theorists and sociologists working in the Recognition Science framework cite this to anchor classical impossibility results in the spatial dimension count. The proof is a direct one-line reduction to the decidable cardinality computation on the enumerated inductive type.
Claim. The set of Arrow conditions has cardinality three: $|A| = 3$, where $A$ consists of unrestricted domain, Pareto efficiency, and independence of irrelevant alternatives.
background
The module recasts Arrow's 1951 impossibility result, Condorcet's paradox, and Gibbard-Satterthwaite manipulation as consequences of sigma conservation on the D=3 lattice. ArrowCondition is the inductive type whose three constructors label the independent binary axes of F₂³ = {0,1}³. The upstream arrowConditionCount theorem computes the cardinality of this type via the decide tactic on its derived Fintype instance.
proof idea
One-line wrapper that invokes arrowConditionCount, which itself reduces to a decidable equality check on the finite enumeration of the three constructors.
why it matters
This cardinality anchors the RS claim that Arrow's conditions correspond to the three axes of F₂³, with the dictatorship baseline as the sole element satisfying all three simultaneously. It supports the module's derivation that any non-dictatorial rule violates at least one condition, leaving the seven nonzero elements of the lattice. The result sits inside the T8 step fixing D=3 and feeds the broader voting paradoxes certification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.