arrow_axiom_count
plain-language theorem explainer
The theorem states that the inductive type enumerating Arrow's four axioms has cardinality exactly four. Social choice researchers embedding Arrow's impossibility result inside Recognition Science would cite this count when equating the non-dictatorial axiom set to configDim at three spatial dimensions. The proof is a direct one-line computation that invokes the decide tactic on the derived Fintype instance.
Claim. Let $A$ be the set whose elements are the four Arrow axioms: unrestricted domain, Pareto efficiency, independence of irrelevant alternatives, and non-dictatorship. Then $|A| = 4$.
background
The module interprets Arrow's 1951 impossibility theorem inside the Recognition Science framework by attaching a J-cost to violations of independence of irrelevant alternatives at the canonical band. ArrowAxiom is the inductive type whose four constructors are unrestrictedDomain, pareto, iia, and nonDictatorship; it derives DecidableEq, Repr, BEq, and Fintype. The module document notes that this cardinality equals configDim at D = 3 after removal of the dictatorial option, forcing the non-trivial axiom count by the spatial-dimension parameter.
proof idea
The declaration is a one-line wrapper that applies the decide tactic. The tactic evaluates Fintype.card on the Fintype instance automatically generated from the four-constructor inductive type ArrowAxiom.
why it matters
The result supplies the axiom_count field required by the downstream definition arrowViolationCert, which packages the Arrow-IIA-violation J-cost certificate. It supplies the structural link stated in the module document: any non-trivial social welfare function carries J-cost at least J(φ) on IIA. The count is forced by the framework landmark D = 3 that yields configDim = 4, closing one step in the Arrow theorem's RS interpretation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.