D_equals_spatial_dim
plain-language theorem explainer
The declaration establishes that Arrow's three conditions form a set of cardinality exactly three, matching the spatial dimension D in Recognition Science. Voting theorists and social choice researchers working in the RS framework would cite it to identify the binary axes of the F₂³ lattice with unrestricted domain, Pareto efficiency, and independence of irrelevant alternatives. The proof is a one-line decision procedure that counts the constructors of the ArrowCondition inductive type.
Claim. The set of Arrow conditions has cardinality three: $|$unrestricted domain, Pareto efficiency, independence of irrelevant alternatives$| = 3$.
background
The module recasts Arrow's impossibility theorem by treating its three conditions as binary axes on the D=3 lattice F₂³. ArrowCondition is the inductive type whose constructors are unrestrictedDomain, paretoEfficiency, and iia; it derives DecidableEq, Repr, BEq, and Fintype. The module documentation states that these three independent axis constraints force the only element satisfying all of them to be the dictatorship baseline, yielding the |F₂³ excluding zero| = 7 structure for non-dictatorial rules.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality Fintype.card ArrowCondition = 3. Because ArrowCondition is a finite inductive type with exactly three constructors and already derives Fintype, the decision procedure enumerates the constructors and confirms the cardinality without further lemmas.
why it matters
This equality anchors the sociology module by linking the three Arrow conditions directly to the spatial dimension D=3 from the core RS forcing chain (T8). It supplies the cardinality step that lets the module derive voting paradoxes from the F₂³ lattice structure described in the module documentation. No downstream results are recorded, so the declaration functions as a foundational interface between classical social choice and the Recognition Science derivation of D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.