arrowConditionCount
plain-language theorem explainer
The declaration establishes that Arrow's impossibility theorem rests on a set of exactly three conditions, matching the three binary axes of the F₂³ lattice in Recognition Science. Voting theorists and social choice researchers working in the RS framework cite this cardinality to ground classical results in the D=3 structure. The proof is a one-line decision procedure that enumerates the inductive definition of ArrowCondition.
Claim. The set consisting of unrestricted domain, Pareto efficiency, and independence of irrelevant alternatives has cardinality three: $|A| = 3$ where $A = $ {unrestricted domain, Pareto efficiency, independence of irrelevant alternatives}.
background
In the Voting Paradoxes from Sigma Conservation module, Arrow's conditions appear as the inductive type ArrowCondition whose three constructors serve as binary axes on the F₂³ lattice. The module derives the classical impossibility results from the fact that only the zero element satisfies all three axis constraints simultaneously while the remaining seven elements each violate at least one. This local setting rests on the Recognition Science claim that the three conditions correspond to the three spatial dimensions forced at T8.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic computes Fintype.card directly from the finite inductive type ArrowCondition, whose three constructors are listed explicitly in the definition.
why it matters
This supplies the cardinality fact consumed by three_conditions_match_D and the VotingParadoxesCert definition that certifies the link to sigma conservation. It fills the explicit step in the module that equates the three Arrow conditions with the D=3 lattice from the forcing chain. The result touches the question of how social-choice paradoxes arise from the same phi-ladder structures that fix physical constants such as alpha inverse.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.