The simplified dual of a Condorcet-dimension program has optimum exactly 1/(k+1): a conjecture true with room to spare, and the weak-duality step that does not close
Abstract
Let C be a set of m candidates, S the m! strict rankings of C, and Mₖ the committees of size k. Zilberstein, Berker, Li and Martins [zblm] attack the question whether every election admits a Condorcet winning set of size 4 with a mixed-integer program, and then propose an analytic route: relax that program, simplify its dual to min u quads.t.quad textstyleΣ γ_(W,c)=1,qquad u ≥ Σ_(c succₛ W)γ_(W,c) (s ∈ S),qquad γ ≥ 0, and conjecture that its optimum uₖ^* satisfies uₖ^* ≤ 2/k, whence — "by weak duality" — the bound α ≤ 2/k and Condorcet winning sets of size 4. We evaluate the program. Read as that paper's own probabilistic restatement of the conjecture has it, with the pairs ranging over {(W,c):W ∈ Mₖ, c ∈ Csetminus W}, its optimum is exactly 1/(k+1) for every m>k ≥ 0, independent of m. So the conjecture is true — but by a factor 2(k+1)/k>2, so it cannot be tight; read literally, with the printed index set c ∈ C, the optimum is 0 and the conjecture is vacuous. The inference it is meant to support does not hold: explicit finite elections at k=1,2,3,4 — two of them printed in [zblm], the other three attaining values its own table prints — have α^*(m,k) strictly above 1/(k+1). We locate the gap in the derivation — the step eliminating the big-M constant Q needs a quantity that is always at most 1/(m-k) to equal 1 — and we close the route at its root: the relaxation being dualised has optimum exactly 1/(k+1)+Q(m-k-1)/(m-k), which at the paper's own Q=1 is at least 1 for all m ≥ 2k+1; so every bound weak duality against it can certify is at least 1, and for k ≥ 3 — in particular for the k=4 the conclusion turns on — no dual certificate for it can prove α ≤ 2/k. Nothing here bounds the Condorcet dimension: whether every election has a Condorcet winning set of size 4 remains open. Every statement below is machine-checked in Lean 4, apart from those that say, at the point where they stand, that they are external computations.
Open review
This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.
Archived files
- Version 1 · current (opens in a new tab)
Source snapshot 2026-09-07 03:53 UTC
File fingerprint
552f7ea37075b7006f11881fbda15d56f240bb0c3697fad248a9df10b085cfa0
Claim ledger
Stated results
CD1candidate2026-09-02
The optimum of the simplified dual LP of arXiv:2604.19851, read as its own 'Dual Bound Probabilistic Interpretation' states it (pairs (W,c) with c in C W), is exactly 1/(k+1) for every m > k >= 0 – in particular it does not depend on the number of candidates m
CD2candidate2026-09-02
The source's Conjecture (Dual Bound on alpha), u*ₖ <= 2/k, is TRUE – and true with a factor 2(k+1)/k > 2 to spare, so it cannot be tight and cannot be the mechanism it is proposed as
CD3correction2026-09-02
Read literally – the printed constraint sums over c in C, not c in C W – the simplified dual has optimum 0, because a pair with c in W is never covered; so the conjecture is vacuous as printed, and the two readings of the source's own two statements of it give different optima (0 and 1/(k+1))
CD4correction2026-09-02
The elimination of the big-M constant Q that produces the simplified dual is invalid: for every feasible gamma, sum over committees of min_c gamma_(W,c) is at most 1/(m-k), so the coefficient of Q in the source's dual objective is at least 1 - 1/(m-k) >= 1/2 whenever m >= k+2 and can never vanish
CD5correction2026-09-02
Weak duality against the simplified dual FAILS: explicit finite elections at k = 1, 2, 3, 4 in which no size-k committee is alpha-undominated for an alpha strictly larger than 1/(k+1) – 5/6 and 2/3 at k = 1, 2/5 at k = 2, 3/10 at k = 3, 3/13 at k = 4
CD6routine2026-09-02
Negative controls: the dual optimum is neither at or below 1/(k+2) nor at or above 1/k; IsDualOpt pins a unique value; there is no feasible gamma at all when m <= k, so the hypothesis k < m is load-bearing; Beats is neither always true nor always false; the covered set is nonempty; the witness elections do not reach 1/2 at k=2 or 1/4 at k=4, and at the diagonal m = k+1 the cyclic election does not beat 1/3
CD7candidate2026-09-02
The LP relaxation the source dualises has optimum exactly 1/(k+1) + Q*(m-k-1)/(m-k), for every m > k >= 0 and every Q >= 0: the upper bound by summing the alpha constraint over all (m-k)C(m,k) pairs, the attaining point being the impartial-culture profile with y identically 1/(m-k)
CD8correction2026-09-02
The source's analytical route is closed at the root: at its own Q = 1 the LP relaxation's optimum is at least 1 for every m >= 2k+1, and 2/k <= 1 for every k >= 2, so NO dual certificate for this relaxation can establish alpha <= 2/k – the relaxation is already weaker than the trivial bound alpha <= 1, independently of the invalid Q elimination of CD4 (qualification per the referee 2026-09-03: for k >= 3; at k = 2 the conjectured bound is the trivial alpha <= 1 – the Lean statement is the narrow form)
CD9correction2026-09-02
The source's Table tab:dual-milp is the LP relaxation WITH the 'Fixed W*' symmetry breaking, not the plain LP relaxation its caption names: all 21 printed cells reproduce under fixed W* and – all 21 printed cells reproduce under fixed W*, while the plain relaxation reproduces only the six diagonal cells k = m-1 (where both equal 1/m) and misses all fifteen off-diagonal ones (5/6 at (4,2) where the table prints 0.750)
CD10prose2026-09-02
For every k >= 1 the cyclic election on m = k(k+2) candidates with m voters (voter j ranking candidate c in position (c-j) mod m) has alpha = (k+1)/(k(k+2)) > 1/(k+1), so weak duality against the simplified dual fails at EVERY committee size, not only the four checked by decide
This ledger entry is reported in prose and is not bound to a Lean theorem.Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- arXiv:2604.19851v1, Itai Zilberstein, Ratip Emin Berker, George Li, Ruben Martins, *Is Four Enough? Automated Reasoning Approaches and Dual Bounds for Condorcet Dimensions of Elections*, GAIW-26 (the 8th Games, Agents, and Incentives Workshop at AAMAS-2026). Primary category cs.GT (cross-list cs.AI), submitted 2026-04-21, v1 is the only version (checked against the arXiv abs page 2026-09-02; the local corpus copy in cseconₛ5ₚart₀009 is byte-identical to the live e-print apart from a trailing newline).
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7