| paper | Condorcet-consistent choice among three candidates |
| authors | Felix Brandt, Chris Dong, Dominik Peters |
| venue | GEB 2025 |
| filed under | voting · theory |
| judged by | gpt-5.6-luna / xhigh (triple__luna__xhigh__c6r1) |
| judge confidence | high |
| authors would recognise it | yes |
The six-ranking type simplex gives a natural, author-recognisable continuous version of reinforcement, and replication makes the high-multiplicity regime credible. However, Fact 1 is an axiomatic impossibility theorem rather than a qualifying computational result under the stated gate. The proposed witness-search wrapper is newly invented and, for fixed three-candidate rules, reduces to constant-dimensional margin comparisons.
fails bit a — no named computational result to mirror
No anchor survives; the decisive objection is that SAT was only used to discover and verify Fact 1, while the stated theorem itself is an axiomatic impossibility result.
fatal: True
The mirror covers Fact 1 and the related \(5\)-, \(8\)-, and \(9\)-voter reinforcement impossibilities; it leaves the axiomatic characterizations, participation results, rule comparisons, and empirical frequency analysis without a computational mirror.
The strongest honest positive case is a high-multiplicity mirror of the paper’s reinforcement results. It is natural and mathematically exact, but it has a serious formal limitation: the paper contains no numbered theorem proving NP-hardness, polynomial-time solvability, parameterized complexity, or approximation complexity. Thus this cannot be a fully compliant ChoCo anchor under the strict rule.
The closest anchor is Fact 1, proved in this paper by SAT solving rather than cited from elsewhere:
Every Condorcet extension violates reinforcement when \( |N^*|\ge 8 \).
In full, the result says that for every social choice function \(f\) which selects the unique Condorcet winner whenever one exists, there are profiles \(P\) and \(P'\) over disjoint electorates such that \(f(P)\cap f(P')\neq\varnothing\), but \(f(P+P')\neq f(P)\cap f(P')\). The paper explicitly says that the result was established computationally and that it does not have a human-readable proof. This is a genuine computationally discovered finite impossibility result, but it is not a complexity classification.
A faithful continuous-population version would use the six complete rankings of three candidates as types. A society is a nonzero rational mass vector \(\eta\in\mathbb{Q}_{\ge 0}^{6}\), where \(\eta_r\) is the mass of voters with ranking \(r\). Pairwise margins are linear in mass, for example \(M_{a,b}(\eta)=\sum_r\eta_r\sigma_r(a,b)\), and a Condorcet winner is a candidate whose two margins are positive. The decision variable is the winner set \(F(\eta)\), where \(F\) is an anonymous Condorcet extension.
The resulting problem could be called Minimum-Mass Reinforcement Witness for Three Candidates:
Given a finite description of an anonymous Condorcet extension \(F\) and an integer \(B\), decide whether there are two nonzero mass vectors \(\eta,\zeta\) whose primitive integer representations have total mass at most \(B\), such that
\(F(\eta)\cap F(\zeta)\neq\varnothing\)
but
\(F(\eta+\zeta)\neq F(\eta)\cap F(\zeta)\).
A solution is the two mass vectors, the common winner, and the three evaluated winner sets. Equivalently, one may write \(\mu=\eta/\|\eta\|_1\) and \(\nu=\zeta/\|\zeta\|_1\); the union is the mixture \(\lambda\mu+(1-\lambda)\nu\), with \(\lambda=\|\eta\|_1/(\|\eta\|_1+\|\zeta\|_1)\).
This is recognisably the authors’ problem: “adding electorates should preserve common winners” becomes “adding population masses should preserve common winners.” The regime is also plausible. A large three-candidate electorate may contain millions of voters but only six ballot types, with repeated blocs sharing the same complete ranking. Any finite witness can be replicated \(K\) times, producing arbitrarily large electorates with exactly the same mass distributions and the same reinforcement failure. Thus the continuous model is not merely a small-election restatement.
For fixed rules such as maximin, Nanson, or leximin, winner evaluation is polynomial—and in this three-candidate, six-type setting essentially constant-time—because all relevant margins are linear functions of the six masses. The SAT-style search for a bounded witness is therefore tractable for a fixed rule. The substantive result transfers in the opposite direction: the continuum does not remove the impossibility. If one insists on the programme’s trichotomy, this is closest to the hardness-transfer side, although the transferred object is an impossibility rather than NP-hardness.
The paper’s other especially relevant result is the theorem in §5.4 stating that maximin is continuous and that any continuous refinement of maximin equals maximin; combined with the preceding theorem, this yields the corollary that maximin is the only homogeneous and continuous Condorcet extension satisfying optimist participation. I would not use it as a second anchor: it is an axiomatic characterization, not a computational result, and atomless individual participation requires additional modelling choices.
The weakest point is decisive. The proposed mirror is a new population-level witness-search problem wrapped around an axiomatic theorem. The source paper does not provide an algorithm, complexity bound, or computational formulation for it, and with only three candidates and six types the fixed-rule version is likely too small to expose a meaningful complexity landscape. So the positive claim should be modest: the paper has a natural, author-recognisable continuous-population reformulation whose finite impossibility survives high multiplicity. It does not, strictly speaking, supply a qualifying ChoCo computational anchor.
The strongest negative point is that the proposed anchor fails ChoCo’s gate. Fact 1 is a finite impossibility theorem:
\[ \text{every Condorcet extension violates reinforcement when } |N^*|\ge 8. \]
SAT was used to discover and verify it, but the result contains no computational problem, input encoding, algorithm, complexity bound, approximation question, or parameterized question. It is an axiomatic impossibility statement. The same is true of the paper’s \(5\)-, \(8\)-, and \(9\)-voter reinforcement theorems, and of the maximin characterization in Section 5.4. Calling SAT a computational method does not turn the theorem into a computational-social-choice result.
The proposed six-type model is otherwise perfectly sensible. Indeed, this is where the negative case is weakest: three-candidate elections naturally admit the six complete rankings as voter types, and replication gives genuine high multiplicity. There is no valid objection based on identities, indivisibility, or an implausible population regime.
What fails is the proposed computational wrapper. In the continuous model, a society is a point \(\mu\) in the fixed simplex \(\Delta^5\), and reinforcement combines two societies by
\[ \lambda\mu+(1-\lambda)\nu. \]
For a fixed rule such as maximin, Nanson, or leximin, checking the winner set requires only six masses and a constant number of linear margin comparisons. The paper’s theorem therefore becomes an existential statement over a constant-dimensional simplex, not an algorithmic problem supplied by the paper.
The “minimum-mass” formulation does not repair this. Unnormalised masses can be scaled arbitrarily without changing any winner or reinforcement violation, so minimum mass collapses to zero. Restricting to primitive integer representations replaces mass by the denominator of a rational point, thereby reintroducing the discrete voter-count question that continuization was meant to remove. The paper’s bound of eight voters is precisely such a lattice/denominator fact; it has no intrinsic analogue for real population distributions.
One could invent a broader problem—say, testing reinforcement for a rule supplied by a circuit, or studying variable numbers of candidates. But then the representation of the rule becomes the central issue: arbitrary encodings can hide arbitrary computational hardness, while fixed standard rules remain finite-dimensional and easy to evaluate. That would be a new meta-complexity project, not a continuous mirror of a computational result in this paper.
So the defensible negative verdict is narrow but strong: this paper supplies no qualifying computational anchor. Its reinforcement results have a natural high-multiplicity reformulation, but that reformulation is an axiomatic restatement unless one adds an artificial denominator or rule-encoding problem. I cannot honestly claim that no future computational study inspired by it could be worthwhile; I can claim that the paper, as written, does not furnish one.
The adversarial triple: the proponent anchors on up to three named results; the opponent sees that case and must defeat every anchor; the judge decides which case convinced it. These are the pipeline’s own outputs, generated by tools/triple_run.py — no human edited them. The paper’s own text is not reproduced here beyond the quoted statement above.