Proportionality and Strategyproofness in Multiwinner Elections

Both proposed anchors are named impossibility theorems about axiomatic committee rules, not algorithmic, hardness, or computational-formulation results proved by this paper. Their continuous versions are coherent distributional rule-existence questions, but they quantify over an arbitrary global $F$ rather than define an instance-wise computational task. Thus the paper fails the computational-anchor gate despite a mathematically clean finite-to-continuum transfer.

The objection that survived

The proposed $F:\Delta(T)\to\binom{C}{k}$ is an arbitrary globally quantified rule, so the mirror lacks an instance-wise input, finite representation, objective, or computational task.

What the mirror covers

The proposed mirror covers Theorems 6.1 and 6.8 as distributional axiomatic obstructions, but leaves the SAT encoding as proof machinery, cited PAV complexity results, and the remaining axiomatic discussion untouched.

Open questions for a prover

The case FOR (proponent)

The strongest honest case is a qualified one. The paper contains no named theorem establishing an NP-hardness, polynomial-time, W[1]-hardness, or FPT result. Its computational contribution is a SAT-assisted proof of axiomatic impossibility. Thus, under a strict ChoCo requirement that anchors be complexity results, this paper has no fully admissible anchor. The NP-completeness of PAV winner determination mentioned in Section 7 is cited prior work, not a numbered result proved here.

If axiomatic impossibilities are admitted as computational anchors, however, there is a genuine and fairly clean continuous-population mirror.

Take a fixed candidate set $C$, committee size $k$, and approval types

\[ T=\{A\subset C:\emptyset\neq A\neq C\}. \]

A society is a distribution $\mu=(\mu_A)_{A\in T}$, where $\mu_A$ is the fraction of voters with approval set $A$. A committee rule is now a function

\[ F:\Delta(T)\longrightarrow \binom{C}{k}. \]

Let $U(\mu)=\bigcup_{\mu_A>0}A$. A society is party-list if all positive-mass approval types are pairwise disjoint.

The paper has no numerical objective to preserve: its underlying problem is rule existence. The continuous decision variable is the selected committee $F(\mu)$, while the strategic operation is a mass transfer. If a mass $\varepsilon$ of type $A$ reports $B$, write $\mu^{A\to B,\varepsilon}$ for the resulting distribution.

The high-multiplicity regime is quite plausible. Consider a large platform, civic consultation, or recommendation service selecting $k$ items from a catalogue of $m$ candidates. Millions of users may fall into a relatively small number of repeated approval templates: demographic cohorts, interest segments, or recurring organizational constituencies. Here $n\gg\tau$, where $\tau$ is the number of realized approval types. The paper’s base obstruction already uses only four candidates and a handful of types; its replication arguments allow arbitrarily large electorates.

My lead anchor is Theorem 6.1, proved in this paper. It states:

If $k\ge3$, $n$ is divisible by $k$, and $m\ge k+1$, then no approval-based committee rule satisfies weak efficiency, proportionality, and strategyproofness.

Here weak efficiency excludes candidates approved by nobody; proportionality requires that, on a party-list profile, every singleton ballot $\{c\}$ occurring at least $n/k$ times must have $c$ elected; and strategyproofness forbids a voter from reporting a proper subset of their truthful approval ballot if this would make the committee contain a strict superset of their truly approved elected candidates. The theorem is proved here using a SAT base case and induction lemmas, not cited from elsewhere.

The corresponding continuous problem is:

Continuous Proportional–Subset-Strategyproof Rule Existence. Given $C$, $k$, and $T$, does there exist a rule $F:\Delta(T)\to\binom Ck$ such that:

\[ F(\mu)\subseteq U(\mu) \]

whenever $|U(\mu)|\ge k$;

\[ \mu_{\{c\}}\ge \frac1k \quad\text{and $\mu$ is party-list} \quad\Longrightarrow\quad c\in F(\mu); \]

and, for every true type $A$, every nonempty $B\subsetneq A$, and every $0<\varepsilon\le\mu_A$,

\[ F(\mu^{A\to B,\varepsilon})\cap A \not\supsetneq F(\mu)\cap A. \]

A solution is an explicitly defined committee rule $F$, together with a proof that these conditions hold for every distribution $\mu$.

The expected answer is impossibility, and the transfer from Theorem 6.1 is exact. If such an $F$ existed, then for every finite profile $P$ with empirical distribution $\mu^P$, define

\[ f_n(P)=F(\mu^P). \]

Changing one voter from $A$ to $B$ changes the distribution by a mass transfer of $\varepsilon=1/n$. The continuous axioms therefore induce the finite axioms. Choosing any large $n$ divisible by $k$ contradicts Theorem 6.1. Thus the continuous question is not merely an analogy: every finite obstruction embeds into it. In the programme’s trichotomy, this is closest to Class B, although the anchor is an impossibility theorem rather than an NP-hardness theorem.

The authors should recognize this as their problem. The candidate set, approval types, committee size, proportionality threshold, and manipulation are unchanged; only voter counts become masses. The one necessary co-modification is strategic: literal individual strategyproofness becomes vacuous in a nonatomic population, because one individual has zero mass and cannot change $\mu$. The non-vacuous continuum analogue must therefore prohibit a positive-mass homogeneous cohort from benefiting by changing its report. That is naturally interpreted as type-level or bloc strategyproofness.

This is also the weakest point. A referee could reasonably say that the paper studies unilateral manipulation by an individual, whereas the proposed mirror studies coordinated mass manipulation. If the authors insist on literal individual strategyproofness, every distribution-only rule is automatically strategyproof, and the mirror loses the paper’s central content. The positive case survives only if type-level manipulation is accepted as the correct high-multiplicity analogue.

A useful second anchor is Theorem 6.8, also proved in this paper by a computer-aided argument. It states:

If $k=2$, $m\ge4$, and $n$ is even, then no approval-based committee rule satisfies weak efficiency, JR on party lists, and superset-strategyproofness.

JR on party lists requires that whenever a ballot $A$ occurs at least $n/k=n/2$ times in a party-list profile, the elected committee contain at least one candidate from $A$. Superset-strategyproofness allows arbitrary ballot changes, not only subset reports, and forbids a change that strictly increases the elected candidates belonging to the voter’s truthful approval set.

Its continuous mirror is:

Continuous JR–Superset-Strategyproof Rule Existence. For $k=2$, $m\ge4$, determine whether there exists $F:\Delta(T)\to\binom C2$ such that weak efficiency holds and

\[ \mu_A\ge\frac12 \quad\text{and $\mu$ is party-list} \quad\Longrightarrow\quad F(\mu)\cap A\neq\emptyset, \]

while for every true type $A$, every report $B\in T$, and every $0<\varepsilon\le\mu_A$,

\[ F(\mu^{A\to B,\varepsilon})\cap A \not\supsetneq F(\mu)\cap A. \]

Again, a solution is the rule $F$, not a SAT encoding. Any such rule would induce a finite rule on every even-$n$ empirical profile, contradicting Theorem 6.8. This supplies a natural continuous question for the $k=2$ case that Theorem 6.1 does not cover.

These mirrors cover only the paper’s impossibility results, not its SAT encoding as an object of study, not the cited NP-completeness of PAV winner determination, and not all of its axiomatic discussion. They are not novelty collisions: the paper studies finite profiles with named voters, not a rule defined on distributions over approval types. Existing high-multiplicity work would support the regime rather than undermine it.

The further questions are substantive:

Does impossibility remain under a weaker form of mass strategyproofness, such as deviations by an entire type but not arbitrary submasses?
What happens for randomized or irresolute continuous rules?
Does restricting the support to candidate-interval approval types restore a compatible rule?
Can one characterize the finite set of distributional witnesses responsible for the impossibility?

So I would present this as a credible but limited positive case: the paper admits a genuine continuous-population reformulation, and its impossibilities transfer cleanly to that setting. I would not present it as a strong ChoCo computational-complexity paper, because it has no named complexity anchor and its central issue is axiomatic rule existence rather than optimization or algorithm design.

The case AGAINST (opponent, writing after the proponent)

The strongest negative case starts with the programme’s gate: this paper has no admissible computational anchor. Its results concern the existence or nonexistence of social choice functions satisfying axioms for fixed $n$, $m$, and $k$. SAT is used as proof machinery; the paper does not define an instance-wise optimization problem, an algorithmic task, a complexity class, or an approximation guarantee. The NP-completeness of PAV winner determination is cited prior work, not a result established by this paper.

Theorem 6.1 nevertheless has a mathematically legitimate continuous reformulation, so the objection should not be that approval types are implausible. Large populations with repeated approval templates are perfectly sensible, and the approval ballot contains all information relevant to the paper’s axioms. Nor is the transfer argument wrong.

The fundamental problem is that the proposed mirror is not a computational problem about a society. It asks whether there exists an arbitrary function

\[ F:\Delta(T)\to\binom{C}{k} \]

satisfying global constraints over every distribution. The input distribution $\mu$ is not supplied to an algorithm that must compute a committee: it is quantified over while the entire function $F$ is being synthesized. There is no objective, pricing problem, separation oracle, or finite representation of a candidate solution. Thus the continuous version remains an axiomatic rule-existence question, merely on an uncountable domain.

The strategic repair does not fix this. Literal individual strategyproofness indeed becomes vacuous for a distribution-only rule, so the proposed positive-mass deviation is the only sensible nontrivial variant. But it changes unilateral manipulation into manipulation by a homogeneous bloc of mass. That may be a reasonable new axiom, yet it is not a computationalization of the paper’s theorem. If one asks only about rational empirical distributions, the construction $f_n(P)=F(\mu^P)$ simply pulls the continuous rule back to finite profiles. If one asks for a finitely described $F$, one must add a representation language or a regularity condition absent from the paper. If one fixes a particular rule such as AV or PAV, one obtains a different winner-determination problem, not the rule-existence theorem.

Theorem 6.8 fares no better. Its proposed continuous version again asks for an arbitrary global function satisfying JR and a bloc version of strategyproofness. The finite obstruction can be embedded at distributions with denominator $2$, and the same dichotomy remains: infinitesimal individual deviations are vacuous, while positive-mass deviations are a new coalition axiom. Neither choice produces an instance-wise computational task. The SAT-generated cycle of finite profiles becomes a finite collection of mass vectors, not an optimization landscape.

One might try to impose continuity or a finite description on $F$ to recover computational content. That either changes the problem or creates a degeneracy: with committees as a discrete codomain, an ordinarily continuous $F$ on the connected simplex would be constant. A bespoke piecewise-constant representation could be interesting, but it would be a new model whose computational significance comes from the added representation, not from this paper.

So the proponent’s two mirrors are valid mathematical reformulations, and the high-multiplicity interpretation is defensible. That is the honest weakness of the negative case. But under ChoCo’s stated scope they do not supply a worthwhile continuous computational mirror: both remain axiomatic synthesis problems, and the paper contains no named complexity result to continuize. A continuous PAV winner-determination project might be valuable, but it would mirror cited prior work rather than this paper’s contribution.

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.