Existence of the Core in Approval-Based Committee Elections
Patrick Becker, Matthias Greger, Dominik Peters
cs.GT
2026-09-11
A harmonic-entropy rule has all local optima in the ABC core, settling a 2017 open problem; a core+ committee is computable in polynomial time.
Approval-based multiwinner elections pick a committee of size k from m candidates, given n voters who each submit an approval set. A voter's utility is how many approved candidates made the committee. The design goal is proportional representation: a large enough group with shared tastes should receive a share of seats matching its size.
Aziz et al. (2017) imported the cooperative-game core into this model. The core is a stability condition: no coalition should be able to pool a proportional share of seats, buy an alternative slate, and make every member strictly better off. Formally, a coalition S may propose a set T under the Hare quota q = n/k. If |S| ≥ (n/k)|T| and every member of S strictly prefers T to the sitting committee W, then W is blocked. JR, EJR, and FJR still ask the coalition to be cohesive about the same candidates. The core does not. That is why it is harder.
Whether such a committee always exists has been open since 2017. Lackner and Skowron (2023) listed it as the main open question of the theory. Workarounds piled up: Proportional Approval Voting (PAV) is a 2-approximation to the core, the Method of Equal Shares (MES) a logarithmic one, and a Lindahl-equilibrium route recently reached a 3.65-approximation. Exact existence was known only in special cases: at most 8 seats, at most 15 candidates, at most seven voter types, at most eight voters, one-dimensional domains, or k copies of every candidate.
The general case stayed unsettled.
The new rule maximizes harmonic entropy over every size-k committee W and every payment system on W.
A payment system gives each voter one unit of budget to spend on approved winners; the leftover is a reserve ri. Each winner may collect at most the quota q. The accounting comes from the MES / Phragmén family, except that winners need not be paid in full, only bounded above. A payment system by itself does not buy fairness. The extra demand is that supporters of losers hold little leftover cash.
Harmonic entropy is a potential on payment vectors. For a probability vector x, a family of water-filling levels fℓ(x) records the height τ at which shaving mass above τ creates exactly ℓ new coordinates of that height. Picture pouring water onto a row of bars until you can fill ℓ extra cups to the same waterline. Then
F(x) = Σ{ℓ=0}^∞ (1/(ℓ+1) − fℓ(x))
If all mass sits on one coordinate, F = 0. If it is uniform on d coordinates, F equals the harmonic number H{d-1}, where Shannon entropy would be log d. F is continuous, concave, and symmetric, and appending a zero coordinate does not change its value. Spreading payments raises the score. That is the point: do not let a few voters dump their budget onto a few winners.
A water-filling operator Φ scoops a new coordinate out of the existing ones. Φ shifts the water-level sequence by one, so F(Φ(x)) − F(x) equals the largest coordinate of x. That identity pins how the objective moves when a candidate is added or deleted:
Together: if no single-candidate swap raises the objective by q − n/(k+1), every loser has reserve load strictly below q. Pair that with the condition that a voter's payment to any winner is at most that voter's reserve, and this is exactly the payment certificate for core+. core+ relaxes coalitions and proposals to [0,1] fractions, so it is strictly stronger than the integer core. The certificate is the Farkas dual of a fractional blocking LP. Checking core+ for a given committee is a linear program.
The construction welds PAV-style global welfare maximization to MES-style payment accounting. The potential is built so that a swap argument goes through. A local optimum is enough. A global maximum is not required.
For every quota in the range n/(k+1) < q ≤ n/k, every election instance has a size-k committee in core+. Global maximizers of harmonic entropy sit there, and so do local maxima under single-candidate swaps.
Under the Hare quota q = n/k the committee can be found in polynomial time. Local search truncates the infinite series at T = 8k²(k+1), turning the truncated objective into an LP with O(nkT) variables. Starting from an arbitrary size-k committee, the algorithm accepts a swap that lifts the truncated objective by at least δ/2. The working quota is the midpoint q = ½(n/k + n/(k+1)), and the improvement threshold is δ = n/(2k(k+1)). The midpoint is stricter than Hare: a smaller quota lets a smaller coalition afford a deviation, so a midpoint core+ committee is automatically in the Hare core. At most 4k(k+1)Hk swaps occur, and each round inspects at most k(m−k) neighbors.
core+ is also nonempty under the strict Droop quota n/(k+1). Take a sequence of quotas approaching Droop from above; some committee appears infinitely often, and that committee blocks every strict Droop fractional objection. No polynomial algorithm is given on this side.
Existence of a Hare-core committee has been formally checked in Lean as part of the ABCVotingLean project.
| Method | Guarantee | Scope |
| PAV | 2-approx to the core | general instances |
| MES | logarithmic approx | general instances |
| Lindahl rounding | 3.65-approx | general instances |
| PAV and other special cases | exact core | k≤8 / m≤15 / ≤7 types / ≤8 voters |
| harmonic entropy | exact core+ | every instance, poly-time |
Approval-based committee elections are the standard model for proportional committees, participatory budgeting with approvals, and multi-seat representation. The core asks whether there is a selection that no proportionally sized group can overturn by buying a strictly better alternative for every member. The answer is yes, and the search does not require enumerating all k-subsets. Local search plus an LP returns both the committee and a payment certificate.
This is not a drop-in replacement for PAV or MES. Each step evaluates k(m−k) neighbors, each neighbor an LP of size O(nk⁴). The theoretical status changed: the core is no longer a property that might be empty. It is an object that can be found and audited with an LP.
The authors say they are still mapping the rule's axioms beyond core+, and they hope harmonic entropy will travel to other proportional-representation problems.
The acknowledgements record that the rule and the core+ proof were found by GPT-6 Astra in a long interactive session. The starting point was Lindahl rounding; the model first produced an approximation factor around 2.065, then was pushed to an exact core. The authors checked the arguments and rewrote the proofs for human readers. That does not change the theorems. It does change how this proof entered the literature.
Polynomial time is an upper bound, not a runtime. With T = 8k²(k+1) the LP has size O(nk⁴), times at most 4k(k+1)Hk rounds and k(m−k) neighbors per round. There is no implementation and no timing data. At k=20, m=100 the worst-case bound is already heavy.
Droop existence has no polynomial algorithm attached. The Hare local search runs at a quota strictly between Hare and Droop.
core+ is stronger than integer core, so the implication to the core is clean. What is missing is a comparison of the new rule against PAV and MES on JR, EJR, FJR, monotonicity, and computational cost. The authors say those properties are still being mapped.
The Lean development covers Hare-core existence, not algorithm correctness and not the Droop case.
The proof is tied to approval utilities (utility equals intersection size) and unit budgets. For general monotone preferences, and for additive utilities in participatory budgeting, core non-emptiness remains open; the 3.65-approximation was aimed at that broader setting. Moving harmonic entropy over as-is would not automatically keep the water-filling swap inequalities.