← back to the atlas

d4-journals-geb-2022-0057 (d4-journals-geb-2022-0057)

Answer: Every mass-MD execution terminates with exactly \(k\) candidates, and its possible outputs are exactly the size-\(k\) mass-PSC committees.

The anchor (named result in the paper)

Lemma 1 — class: other

PDF text-layer excerpt — equations and symbol order may be approximateThe MD rule always terminates and outputs $W \ : \ |W|=k$.

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

The continuous mirror question, as graded

Given a rational distribution \(\mu\) over ranking types and a normalized quota \(q\in(1/(k+1),1/k]\), let \(M(S)\) be the mass of types whose \(|S|\)-prefix is exactly \(S\). Run MD by adding candidates to satisfy demands \(\min\{\lfloor M(S)/q\rfloor,|S|\}\); does this mass-based procedure terminate with a committee of size \(k\), and are its possible outputs exactly the committees satisfying mass-PSC?

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

Let \(C\) contain \(m\ge 1\) candidates, let \(1\le k\le m\) be an integer, and let the rational quota satisfy \(q\in(1/(k+1),1/k]\). Committees are subsets of candidates, with no fractional membership.
A society is given by its support: the list of the \(\tau\) strict ranking types with positive mass, each mass \(\mu_r\) a binary rational, with \(\sum_r\mu_r=1\). Here \(\tau\) is the support size, not the number of possible rankings. Let \(L\) be the total input bit length; state any running times in \(m,\tau,L,k\).
The \(j\)-prefix \(P_j(r)\) is the unordered set of the first \(j\) candidates in ranking \(r\); for nonempty \(S\subseteq C\), put \(M(S)=\sum_{r:P_{|S|}(r)=S}\mu_r\).
A coalition is a vector of submasses \(0\le a_r\le\mu_r\). It solidly supports \(S\) if every ranking with \(a_r>0\) places every candidate in \(S\) above every candidate outside \(S\). A size-\(k\) committee \(W\) satisfies mass-PSC if, for every nonempty \(S\subseteq C\), every positive integer \(\ell\), and every such coalition with \(\sum_r a_r\ge\ell q\), one has \(|W\cap S|\ge\min\{\ell,|S|\}\).
Mass-MD starts with \(W=\varnothing\) and processes stages \(j=1,\ldots,m\) in order. At stage \(j\), while some occurring \(j\)-prefix \(S\) has \(|W\cap S|<\min\{\lfloor M(S)/q\rfloor,|S|\}\), choose any such \(S\) and any \(c\in S\setminus W\), and add \(c\) to \(W\).
Advance only when no demand at that stage remains unmet; output after stage \(m\), including when \(k\) candidates have already been selected. Possible outputs range over all choices of deficient sets and candidates.
For every admissible input, does every mass-MD execution terminate with exactly \(k\) candidates, and are its possible outputs exactly the size-\(k\) mass-PSC committees, or is there a counterexample to either property?
For finite electorates, every MD execution terminates with exactly \(k\) candidates, and its possible outputs are exactly the PSC committees. [Aziz and Lee](https://www.cse.unsw.edu.au/~haziz/dummett.pdf)
No separate result establishing or refuting these properties for the specified rational-mass formulation was located.

Modeling choices made when packaging the task

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

Result

Both properties hold for every admissible input. Every mass-MD execution terminates with exactly \(k\) candidates, and its possible outputs are precisely the size-\(k\) mass-PSC committees.

The proof uses an exact reduction to a finite electorate. Allowing fractional coalition submasses introduces no additional demands.

1. Mass-PSC is equivalent to prefix inequalities

For each nonempty \(S\subseteq C\), define
\(d(S)=\min\{\lfloor M(S)/q\rfloor,|S|\}\).

We first prove that a committee \(W\) satisfies mass-PSC if and only if
\(|W\cap S|\ge d(S)\)
for every nonempty \(S\subseteq C\).

Because rankings are strict, a ranking \(r\) places every member of \(S\) above every candidate outside \(S\) exactly when \(P_{|S|}(r)=S\). Consequently, every coalition solidly supporting \(S\) has total mass at most \(M(S)\). This maximum is attained by taking
\(a_r=\mu_r\) when \(P_{|S|}(r)=S\), and \(a_r=0\) otherwise.

For necessity, suppose \(W\) satisfies mass-PSC. Put \(h=\lfloor M(S)/q\rfloor\). If \(h=0\), the required inequality is automatic. Otherwise, the maximal supporting coalition has mass \(M(S)\ge hq\), so mass-PSC, applied with \(\ell=h\), gives
\(|W\cap S|\ge\min\{h,|S|\}=d(S)\).

For sufficiency, suppose all the prefix inequalities hold. If a coalition solidly supporting \(S\) has mass at least \(\ell q\), then \(M(S)\ge\ell q\), and hence \(\lfloor M(S)/q\rfloor\ge\ell\). Therefore
\(|W\cap S|\ge d(S)\ge\min\{\ell,|S|\}\),
as required.

Nonoccurring sets have \(M(S)=0\) and impose no constraint. Thus there are at most \(m\tau\) relevant prefix sets.

2. Exact scaling to a finite electorate

Write the input rationals as
\(\mu_r=u_r/v_r\) and \(q=a/b\),
with positive integer denominators. Choose
\(D=b\prod_{r=1}^{\tau}v_r\),
and define
\(n_r=D\mu_r\), \(n=D\), and \(Q=Dq\).

All these quantities are positive integers. Construct a finite electorate containing exactly \(n_r\) voters with ranking \(r\). Its total number of voters is
\(\sum_r n_r=D\sum_r\mu_r=D=n\).

The quota satisfies
\(n/(k+1)<Q\le n/k\),
because multiplying the assumed inequalities for \(q\) by \(D\) preserves them. The candidate set, strict rankings, and committee size are unchanged. Thus this finite instance satisfies the hypotheses of the finite-electorate MD theorem.

For every nonempty \(S\subseteq C\), let \(N(S)\) be the set of voters whose top-\(|S|\) set is \(S\). Then
\(|N(S)|=DM(S)\),
and therefore
\(\lfloor |N(S)|/Q\rfloor=\lfloor M(S)/q\rfloor\).

In the finite electorate, \(N(S)\) is the maximal solid coalition supporting \(S\). Applying the same maximal-coalition argument as in Section 1, finite \(Q\)-PSC is equivalent to
\(|W\cap S|\ge\min\{\lfloor |N(S)|/Q\rfloor,|S|\}\)
for every nonempty \(S\).

The displayed floor identity proves that finite \(Q\)-PSC and mass-PSC select exactly the same committees. This argument does not require an arbitrary fractional coalition to correspond to an integer voter subset.

3. Every execution is preserved

At stage \(j\), the occurring prefix sets are identical in the two instances: every supported ranking has \(n_r>0\), and no new ranking was introduced.

For any such prefix \(S\), its finite demand is
\(\min\{\lfloor |N(S)|/Q\rfloor,|S|\}=d(S)\).

Consequently, at every state \((j,W)\), both procedures have exactly the same deficient sets. After choosing a deficient \(S\), both permit exactly the candidates in \(S\setminus W\). Their conditions for advancing a stage and for terminating are also identical.

Hence every mass-MD execution corresponds, choice for choice, to a finite MD execution, and conversely. This correspondence includes processing the remaining stages after \(k\) candidates have been selected.

Aziz and Lee’s Lemma 1 establishes that every finite MD execution terminates with exactly \(k\) candidates; their Theorem 1 establishes that its possible outputs are exactly the PSC committees. Their procedure processes all stages, including after selecting \(k\) candidates. [Aziz and Lee, *A characterization of proportionally representative committees*, Lemma 1 and Theorem 1](https://www.cse.unsw.edu.au/~haziz/dummett.pdf).

Applying those results to the scaled instance and using the two correspondences above proves both asserted properties.

4. Computation directly from the support

The scaled electorate need not be explicitly constructed. Although \(D\) can be exponentially large in value, its binary length is \(O(L)\), since its factors are input denominators.

Here is one elementary implementation and its bit-complexity bound.

Represent prefix sets by \(m\)-bit incidence vectors. At each stage, group equal prefixes by comparing each against previously encountered groups. Across all stages, this costs \(O(m^2\tau^2)\) bit operations. Sum the integer weights \(n_r\) in each group and compute its demand by dividing that sum by \(Q\). All operands have \(O(L)\) bits, so elementary integer arithmetic gives a total arithmetic cost of \(O(m\tau L^2)\), including denominator clearing.

During execution, rescan the current stage’s at most \(\tau\) groups after each addition and once to finish the stage. There are \(k\) additions and \(m\) stage completions. Computing each intersection size from incidence vectors costs \(O(m)\), giving \(O(m\tau(m+k))\) further bit operations.

Thus one execution can be computed in
\(O(m^2\tau^2+m\tau L^2+m\tau(m+k))\)
bit operations, directly from the supported rankings.

The same prefix table permits verification of a supplied size-\(k\) committee’s mass-PSC property in polynomial time. These bounds concern one execution or one committee verification; they make no assertion that all possible outputs can be enumerated in polynomial time.

⟨structured verdict parsed — rendered above⟩

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

The output proves both requested properties. The reduction preserves the demands, the admissible choices at every stage, and the committee constraints exactly. The cited finite-electorate results apply with the stated quota. No major or minor mathematical issues were found.

1. Equivalence between mass-PSC and prefix inequalities

The strict-ranking assumption is used correctly: a ranking solidly supports a nonempty set \(S\) precisely when its first \(|S|\) candidates form \(S\). This remains valid for \(S=C\), where the condition concerning outside candidates is vacuous.

Consequently, \(M(S)\) is exactly the maximum mass of a coalition solidly supporting \(S\). The proposed maximal coalition satisfies every bound \(0\le a_r\le\mu_r\).

The necessity argument correctly separates the case \(h=\lfloor M(S)/q\rfloor=0\). When \(h>0\), it is an admissible positive integer in the definition, and the maximal coalition meets the threshold \(hq\).

The sufficiency argument also respects the quantifiers: for any qualifying coalition and positive integer \(\ell\), its mass is at most \(M(S)\), so \(\lfloor M(S)/q\rfloor\ge\ell\). Taking the minimum with \(|S|\) preserves the required inequality.

Thus the equivalence is established. Fractional submasses create no additional constraints beyond those imposed by the maximal supporting coalition. Nonoccurring sets have zero demand, and the bound of \(m\tau\) relevant sets correctly counts prefixes of supported rankings.

2. Exact scaling

The denominator product \(D=b\prod_r v_r\) is a positive integer divisible by every denominator used. Therefore all \(n_r=D\mu_r\) and \(Q=Dq\) are positive integers. The voter count is exactly \(n=D\), because the masses sum to one.

Multiplication by positive \(D\) correctly gives
\[ n/(k+1)<Q\le n/k. \]

The scaled electorate retains the candidate set, strict rankings, and supported ranking types. For every nonempty \(S\), the identity \(|N(S)|=DM(S)\) is exact. Since \(Q=Dq>0\), the displayed floor identity follows without rounding error.

The maximal-coalition argument applies equally to voter subsets. It establishes that finite \(Q\)-PSC and mass-PSC impose identical committee inequalities. The proof correctly avoids assuming that each fractional coalition must correspond to an integer voter subset.

3. Execution correspondence and cited results

At each state \((j,W)\), the two procedures have identical occurring prefix sets and identical demands. They therefore permit identical deficient-set choices and identical candidate additions. Their stage-advancement and termination conditions agree.

This establishes correspondence for whole executions, including their ordering of additions and all stages after reaching \(k\) selected candidates.

I checked the cited source. Its setting uses strict rankings and a quota in the interval \(n/(k+1)<Q\le n/k\). Its MD procedure has the same demand test, candidate choices, and stage progression. Lemma 1 supplies termination with exactly \(k\) candidates; Theorem 1 supplies the equivalence between PSC committees and possible MD outcomes. The source also explicitly retains all stages after selecting \(k\) candidates. Thus the theorem hypotheses and procedural correspondence are verified. [Aziz and Lee, *A characterization of proportionally representative committees*](https://www.cse.unsw.edu.au/~haziz/dummett.pdf).

Both conclusions now follow from the correspondences already proved. No additional lemma is missing.

4. Running-time audit

The exponential value of \(D\) does not invalidate the algorithmic claim: its binary length is \(O(L)\). Each scaled weight, quota, and prefix-group sum also has \(O(L)\) bits.

The stated accounting is valid:

Finding an eligible candidate and updating the committee are covered by these bounds. The prefix table also supports polynomial-time verification of a supplied size-\(k\) committee.

The complexity claim concerns computing one execution and verifying one committee. It does not claim polynomial-time enumeration of all outputs.

Feedback

No clarification or repair is required. The proof resolves the rational-mass formulation as specified, including arbitrary permitted choices, exact quota thresholds, and continued processing through stage \(m\).

⟨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.