votingParadoxesCert
plain-language theorem explainer
Recognition Science derives Arrow's impossibility from the D=3 lattice F₂³. The definition votingParadoxesCert packages the exact count of Arrow conditions together with the uniqueness of the dictatorship rule. Decision theorists and sociologists cite it when connecting social-choice impossibilities to the three binary axes. It is assembled by direct field assignment from the arrowConditionCount theorem and the arrow_dictatorship_only theorem.
Claim. A certificate $V$ for voting paradoxes consists of the pair of statements that the set of Arrow conditions has cardinality three and that every voting rule satisfying all three conditions coincides with the dictatorship.
background
In the Recognition Science framework the three classical voting paradoxes are recovered from sigma conservation on the D=3 lattice F₂³. The structure VotingParadoxesCert is defined by two fields: the cardinality of ArrowCondition equals three, and every voting rule that meets the three admissibility criteria equals the dictatorship. The module documentation states that Arrow's conditions correspond to the three independent axis constraints of F₂³ and that the only element satisfying all three is the dictatorship baseline.
proof idea
The definition is a direct record construction. It supplies the three_conditions field from the theorem arrowConditionCount and the arrow_uniqueness field from the theorem arrow_dictatorship_only.
why it matters
This definition supplies the sociology-side certificate imported by the downstream votingParadoxesCert in Decision.VotingParadoxesFromJCost. It closes the derivation of Arrow's impossibility theorem from the Recognition Science forcing chain at the step where D=3 spatial dimensions are fixed. The parent result in the Decision module uses the certificate to link J-cost to social-choice paradoxes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.