ArrowCondition
plain-language theorem explainer
ArrowCondition enumerates the three axioms of Arrow's impossibility theorem as an inductive type with constructors for unrestricted domain, Pareto efficiency, and independence of irrelevant alternatives. Social choice theorists working in the Recognition Science framework cite it to link voting axioms to the F₂³ lattice. The declaration is a direct inductive definition with deriving clauses for decidability and finiteness, requiring no proof steps.
Claim. Let $A$ be the inductive type whose elements are the three conditions of Arrow's theorem: unrestricted domain, Pareto efficiency, and independence of irrelevant alternatives. These correspond to the three binary axes of the vector space $F_2^3$.
background
The module derives classical voting paradoxes from sigma conservation in Recognition Science, identifying Arrow's 1951 impossibility with the structure of the D=3 lattice. The three conditions are treated as independent axis constraints on $F_2^3 = {0,1}^3$, so that the only element satisfying all three simultaneously is the dictatorship baseline at the origin. This setup rests on the upstream result that spatial dimension D equals 3 (T8 in the forcing chain), which forces the eight-element lattice whose non-trivial elements number seven.
proof idea
The declaration is an inductive definition that introduces three constructors and attaches deriving clauses for DecidableEq, Repr, BEq, and Fintype. No tactics or lemmas are applied; the type is introduced directly to serve as a finite enumeration whose cardinality is later shown to be three.
why it matters
The definition supplies the three conditions whose count is equated to D=3 in downstream theorems arrowConditionCount and three_conditions_match_D. It is used by VotingParadoxesCert to certify that every non-dictatorial rule violates at least one condition, reproducing Arrow's impossibility inside the Recognition Science lattice. The construction directly instantiates the module's claim that the |F₂³ minus the origin| = 7 structure accounts for the classical voting paradoxes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.