← back to the atlas

Justified Representation: From Hare to Droop (d4-conf-wine-2025-0012)

Answer: Polynomial-time solvable in \(m,\tau,k,L\) by a weighted implementation of Droop GJCR.

The anchor (named result in the paper)

Theorem 2 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateDroop GJCR selects a committee of size k and satisfies Droop-EJR+.

statement extracted from the paper’s text layer; consult the paper for the exact wording

The continuous mirror question, as graded

Given finite \(C\), \(k\), \(T\subseteq 2^{C}\), and rational \(\mu\in\mathbb{Q}_{\ge 0}^{T}\) with \(\sum_{t\in T}\mu_t=1\), compute \(W\subseteq C\) with \(|W|=k\) such that for every \(\ell\in[k]\) and \(x\) satisfying \(0\le x_t\le\mu_t\), \(\sum_t x_t>\ell/(k+1)\), and \(\left(\bigcap_{x_t>0}t\right)\setminus W\ne\varnothing\), some \(t\) with \(x_t>0\) has \(|t\cap W|\ge\ell\); equivalently, compute a committee returned by mass-Droop-GJCR using \(g_{W,\ell}(c)=\sum_{t:\,c\in t,\ |t\cap W|\le\ell-1}\mu_t\) and trigger \(g_{W,\ell}(c)>\ell/(k+1)\).

Packaged proof task (what the prover saw — nothing else)

Let \(C\) be a finite candidate set with \(m=|C|\), and let \(1\le k\le m\) be an integer.
A society is given by its support: a list \(T\subseteq 2^C\) of \(\tau=|T|\) approval types with positive binary rational masses \(\mu_t\), summing to \(1\). Empty approval types are allowed; \(\tau\) counts listed types, not possible types. Let \(L\) be the total input bit length.
A subgroup is a vector \(x\in\mathbb R^T\) with \(0\le x_t\le\mu_t\). A committee \(W\subseteq C\), \(|W|=k\), satisfies mass-Droop-EJR+ if, for every integer \(1\le\ell\le k\) and every subgroup \(x\) with \(\sum_{t\in T}x_t>\ell/(k+1)\) and \((\bigcap_{t:x_t>0}t)\setminus W\ne\varnothing\), some type \(t\) with \(x_t>0\) satisfies \(|t\cap W|\ge\ell\).

Is finding a committee satisfying mass-Droop-EJR+ polynomial-time solvable in \(m,\tau,k,L\), or is it NP-hard?

For explicitly listed discrete voters, Droop GJCR is polynomial-time computable and always returns a size-\(k\) committee satisfying Droop-EJR+. [Casey and Elkind](https://arxiv.org/html/2508.00811v1)
No result settling this exact computational problem with binary rational masses was located.

Modeling choices made when packaging the task

Prover output (gpt-6.1-sol / high, Bolzano prover prompt)

Result

Finding a committee satisfying mass-Droop-EJR+ is polynomial-time solvable in \(m,\tau,k,L\).

The algorithm is a weighted implementation of Droop GJCR from [Casey and Elkind, Section 3.2](https://arxiv.org/html/2508.00811v1#S3.SS2). Below, we prove correctness directly for masses and establish polynomial bit complexity without expanding the society into individual voters.

1. A finite characterization of violations

For any candidate set \(U\subseteq C\), define the representation of type \(t\) by \(r_t(U)=|t\cap U|\). For \(c\in C\setminus U\) and \(1\le\ell\le k\), let

\[ S(c,\ell,U)=\{t\in T:c\in t,\ r_t(U)<\ell\}, \qquad M(c,\ell,U)=\sum_{t\in S(c,\ell,U)}\mu_t. \]

Lemma 1. A size-\(k\) committee \(W\) satisfies mass-Droop-EJR+ if and only if \(M(c,\ell,W)\le\ell/(k+1)\) for every \(c\in C\setminus W\) and \(1\le\ell\le k\).

Proof. Suppose \(M(c,\ell,W)>\ell/(k+1)\). Set \(x_t=\mu_t\) for \(t\in S(c,\ell,W)\), and set \(x_t=0\) otherwise. This is an admissible subgroup exceeding the required mass threshold. All its positive types approve the unelected candidate \(c\), and every such type has representation below \(\ell\). Thus it violates the axiom.

Conversely, suppose a subgroup \(x\) violates the axiom at level \(\ell\). Choose \(c\in(\bigcap_{t:x_t>0}t)\setminus W\). Every type with \(x_t>0\) belongs to \(S(c,\ell,W)\), because every such type has representation below \(\ell\). Consequently,

\[ M(c,\ell,W)\ge\sum_{t:x_t>0}\mu_t \ge\sum_{t\in T}x_t>\frac{\ell}{k+1}. \]

This proves the equivalence. \(\square\)

In particular, fractional subgroups require no continuous optimization: a violation exists precisely when one of these finitely many full-type sums exceeds its threshold.

2. The algorithm

Fix any ordering of the candidates. Initialize \(W=\varnothing\). Process the levels \(\ell=k,k-1,\ldots,1\) in that order.

At level \(\ell\), repeatedly perform the following operation:

After all levels finish, add arbitrary unelected candidates until \(|W|=k\).

We must prove that the greedy phase never selects more than \(k\) candidates, so the completion step is well defined.

3. The greedy phase selects at most \(k\) candidates

We use charges only to analyze the algorithm; it does not compute them.

Whenever the algorithm selects a candidate \(c\) at level \(\ell\), write \(S=S(c,\ell,W)\) for the supporting types immediately before selection, and let \(s=\sum_{t\in S}\mu_t\). Charge each \(t\in S\) an amount \(\mu_t/s\). Types outside \(S\) receive no charge.

Each selected candidate therefore generates total charge exactly \(1\). The charge per unit mass to a participating type is \(1/s\). Since selection requires \(s>\ell/(k+1)\), this charge satisfies

\[ \frac1s<\frac{k+1}{\ell}. \]

Lemma 2. At every prefix of the greedy phase, each type’s cumulative charge per unit mass is strictly below \(k+1\).

Proof. Fix a prefix and a type \(t\). If \(t\) has received no charge, the assertion holds.

Otherwise, consider its last charge within that prefix, incurred at some level \(\ell\). Immediately before that selection, eligibility gives \(r_t(W)\le\ell-1\). Every earlier charge to \(t\) came from a distinct selected candidate that \(t\) approves. Hence \(t\) had received at most \(\ell-1\) earlier charges, and at most \(\ell\) charges including this last one.

Because the algorithm processes levels in decreasing order, every one of these charges occurred at a level \(h\ge\ell\). Each charge per unit mass was therefore strictly below

\[ \frac{k+1}{h}\le\frac{k+1}{\ell}. \]

The cumulative charge per unit mass is strictly below \(\ell\cdot(k+1)/\ell=k+1\). There are no later charges within the chosen prefix, by the choice of the last charge. \(\square\)

Now suppose a prefix has selected \(q\) candidates, and let \(b_t\) denote type \(t\)’s cumulative charge per unit mass. Summing charges by candidates and then by types gives

\[ q=\sum_{t\in T}\mu_t b_t <\sum_{t\in T}\mu_t(k+1)=k+1. \]

The strict inequality follows from Lemma 2, positivity of the masses, and their sum being \(1\). Since \(q\) is an integer, \(q\le k\).

Thus every prefix contains at most \(k\) selections. In particular, the greedy phase selects at most \(k\) candidates, and padding to size \(k\) is possible because \(m\ge k\).

4. Correctness of the final committee

Let \(V\) be the final committee, including padding. Fix \(1\le\ell\le k\), and let \(W_\ell\) be the selected set when processing level \(\ell\) finished.

The stopping condition at that level guarantees

\[ M(c,\ell,W_\ell)\le\frac{\ell}{k+1} \quad\text{for every }c\in C\setminus W_\ell. \]

Consider any \(c\in C\setminus V\). Since \(W_\ell\subseteq V\), the candidate \(c\) was also outside \(W_\ell\). Moreover, adding candidates cannot decrease a type’s representation, so \(r_t(V)\ge r_t(W_\ell)\) for every \(t\). Therefore

\[ S(c,\ell,V)\subseteq S(c,\ell,W_\ell), \qquad M(c,\ell,V)\le M(c,\ell,W_\ell) \le\frac{\ell}{k+1}. \]

This holds for every required \(c\) and \(\ell\). Lemma 1 proves that \(V\) satisfies mass-Droop-EJR+.

Empty approval types cause no difficulty: they belong to no supporting set and receive no charges.

5. Polynomial bit complexity

Write each input mass as \(\mu_t=p_t/q_t\), where \(p_t,q_t\) are positive binary integers. Compute a common denominator and integer weights:

\[ D=\prod_{t\in T}q_t, \qquad a_t=p_t(D/q_t). \]

These are exact integers, with \(\mu_t=a_t/D\) and \(\sum_t a_t=D\). The bit length of \(D\) is at most \(1+\sum_t\log_2 q_t\), hence \(O(L)\). Since \(0<a_t\le D\), the weights also have \(O(L)\) bits.

Every selection test can now be implemented by the integer comparison

\[ (k+1)\sum_{t\in S(c,\ell,W)}a_t>\ell D. \]

All integers in these comparisons have \(O(L+\log k)\) bits. In particular, an arbitrarily small positive excess over the Droop threshold is detected exactly.

Maintain the counts \(r_t(W)\), updating them after each selection. A complete candidate scan uses \(O(m\tau)\) arithmetic operations. Each successful scan selects one candidate, and each unsuccessful scan finishes one level. There are at most \(k\) successful scans and exactly \(k\) level-ending scans. Thus the greedy phase uses \(O(km\tau)\) arithmetic operations on integers of polynomial bit length.

Constructing the integer weights, updating counts, and padding the committee also take polynomial time. Consequently, the entire algorithm runs in polynomial time in \(m,\tau,k,L\).

The charges used in the proof are never computed, and no population of \(D\) individual voters is constructed.

⟨structured verdict parsed — rendered above⟩

Adversarial review (gpt-6.1-sol / medium, Bolzano verifier prompt)

Verdict: proved. The output resolves the assigned problem: it gives an algorithm for finding a size-\(k\) committee satisfying mass-Droop-EJR+ and proves polynomial running time in \(m,\tau,k,L\). I found no major or minor mathematical issues.

In the forward direction of Lemma 1, the proposed subgroup satisfies \(0\le x_t\le\mu_t\). Its mass exceeds \(\ell/(k+1)\), every positive type approves the same unelected candidate \(c\), and every positive type has representation below \(\ell\). These are exactly the conditions for a violation.

Conversely, a violating subgroup has positive total mass, so its positive support is nonempty. The axiom’s failed conclusion means that every positive type has representation below \(\ell\). The chosen common unelected candidate therefore puts every positive type in \(S(c,\ell,W)\). Both inequalities comparing supporting mass, full-type mass, and subgroup mass are valid.

The lemma preserves the strict threshold correctly: equality with \(\ell/(k+1)\) is allowed. It addresses arbitrary real subgroups without assuming their coordinates are rational.

The selection rule is explicit and uses only the finite sums from Lemma 1. Selecting an unelected candidate strictly enlarges \(W\); finishing a level decreases the level. Thus the greedy phase terminates independently of the later size bound.

The attribution to Droop GJCR agrees with Definition 14 in [Casey and Elkind, Section 3.2](https://arxiv.org/html/2508.00811v1#S3.SS2). Crucially, the output proves the weighted version directly; it does not rely on applying a discrete-voter theorem to rational masses without justification.

A selection has supporting mass \(s>\ell/(k+1)>0\), so every charge is well defined. The total charge for that selection is
\(\sum_{t\in S}\mu_t/s=1\).

Because \(\mu_t>0\), the charge per unit mass for a participating type is exactly \(1/s\). The strict bound \(1/s<(k+1)/\ell\) follows from the selection condition.

Fixing the last charge within an arbitrary prefix is legitimate. Immediately before this charge at level \(\ell\), eligibility gives \(r_t(W)\le\ell-1\). Every earlier charge corresponds to a distinct selected candidate approved by \(t\); therefore the number of earlier charges cannot exceed \(r_t(W)\). Approved selections that did not charge \(t\) do not invalidate this inequality.

Levels are processed in decreasing order, so all charges under consideration occurred at levels \(h\ge\ell\). Each therefore contributes strictly less than \((k+1)/\ell\) per unit mass. There are at most \(\ell\) such charges, giving the stated strict cumulative bound. An uncharged type has cumulative charge zero, also strictly below \(k+1\).

Summing charges by selections and by types gives \(q=\sum_t\mu_tb_t\). Since the support is finite, all masses are positive, and their sum is one, the strict typewise bound implies \(q<k+1\). Integrality then yields \(q\le k\).

This argument applies to every prefix and does not presuppose that the algorithm already respects the size limit. Padding is consequently well defined because \(m\ge k\).

The stopping condition at level \(\ell\) establishes the required bound for every candidate then unelected. Any candidate outside the final committee was also outside \(W_\ell\).

Subsequent selections and padding can only increase representation. Hence the asserted supporting-set inclusion and mass inequality hold. Applying Lemma 1 to the final size-\(k\) committee establishes the full axiom for every permitted level and subgroup.

The product denominator \(D\) has \(O(L)\) bits, even though its numerical value may be exponentially large. Each \(a_t=p_t(D/q_t)\) is an exact positive integer. Normalization gives \(\sum_ta_t=D\), and therefore \(a_t\le D\).

The integer comparison exactly implements the strict rational threshold. Its operands have \(O(L+\log k)\) bits. Constructing \(D\) and the weights uses polynomially many operations on polynomial-length integers.

Each scan uses \(O(m\tau)\) arithmetic operations. The proved size bound permits at most \(k\) successful scans, and there is one terminating scan per level. Thus the stated \(O(km\tau)\) arithmetic-operation bound is valid, and polynomial operand lengths give polynomial bit complexity.

Empty approval types are correctly excluded from supporting sets. The argument also covers exact threshold equality, \(k=1\), \(k=m\), and a greedy phase with no selections. No additional assumptions, missing lemmas, or repairs are needed.

⟨structured verdict parsed — rendered above⟩

Tier: machine-proved, adversarially reviewed by an independent model. No human has checked this proof. Generated from pipeline artifacts by tools/atlas_build.py.