Weak Strategyproofness in Randomized Social Choice

The paper contains no numbered theorem asserting hardness, tractability, approximation, or parameterized complexity, so bit (a) fails. The proposed plurality mass-transfer LP is a plausible new computational problem, but it adds costly coalition intervention and is not a computational mirror of Theorem 1. The paper therefore cannot receive a qualifying ChoCo mirror verdict.

The objection that survived

The proposed positive-mass transfer problem changes unilateral weak strategyproofness into a coalition-control problem and is not anchored in any named computational result.

What the mirror covers

The proposal concerns only the plurality-score example associated with Theorem 1; it leaves Theorem 2 and Theorems 3–6 as axiomatic characterizations or impossibilities.

Open questions for a prover

The case FOR (proponent)

The strict ChoCo verdict is that this paper has no qualifying computational anchor. Theorem 1 is an axiomatic possibility theorem; Theorem 2 is an axiomatic characterization; Theorems 3–6 are impossibility theorems. None asserts NP-hardness, membership in P, parameterized complexity, an algorithm, or an approximation result. Theorem 5 is explicitly attributed to Brandl et al. (2018), and the computer-assisted proof does not make it a computational-complexity result. So this paper is not a direct positive candidate under the programme’s named-result gate.

The strongest honest positive case is nevertheless Theorem 1, which is proved in this paper (the conference version gives a proof sketch and defers details to the full version):

Every score-based SDS on strict preferences satisfies weak strategyproofness.

A natural high-multiplicity regime exists. Consider a very large election or platform consultation with, say, millions of voters but only 120–500 recurring complete rankings over five or six alternatives. A type is a complete ranking, and its mass is the fraction of voters submitting it. Two voters with the same ranking and the same manipulation costs are interchangeable. The lottery remains the paper’s lottery; only the population profile becomes a rational mass vector.

The closest computational companion is:

*Continuous Plurality-SDS Robustness.*

An instance consists of a finite explicit type set \(T\subseteq L\), a rational mass vector \(\mu\), rational conversion costs \(\gamma(t,t')\), a target alternative \(c^\star\), and a rational probability threshold \(q\). A feasible intervention is a mass-transfer matrix \(x\), with

\[ \sum_{t'}x_{t,t'}\leq \mu_t, \qquad \mu'_u=\mu_u-\sum_vx_{u,v}+\sum_vx_{v,u}. \]

The rule is the plurality-score SDS from Theorem 1,

\[ p_{\mu'}(c)= \frac{\sum_{t:\,c\text{ is top in }t}\mu'_t} {\sum_d\sum_{t:\,d\text{ is top in }t}\mu'_t}. \]

The task is to find a minimum-cost transfer

\[ \min_x\sum_{t,t'}\gamma(t,t')x_{t,t'} \]

such that \(p_{\mu'}(c^\star)\ge q\), or report infeasibility. The transfer matrix is the certificate.

For this particular member of the theorem’s class, I would expect Class A: the plurality score is linear in the masses, so the probability constraint is linear and the problem is an LP with \(O(\tau^2)\) transfer variables. Its complexity would be polynomial in the explicit number of types \(\tau\) and the encoding length of the rational data, not necessarily polynomial in \(m\) alone. Replacing plurality by more general score-based rules generates further questions: power-transformed scores, Copeland scores with majority-cell disjunctions, Condorcet-score rules, and minimum mass needed to make a candidate’s probability one.

This is recognisably related to the authors’ object: it preserves complete rankings, population shares, their score-based SDS, and the same lottery semantics. It does not fractionalize preferences or outcomes. It also fits the programme’s computational targets by turning population mass into the intervention variable.

The decisive weakness is that this is an algorithmic companion, not a mirror of a computational result in the paper. More seriously, Theorem 1 concerns a single named voter changing her report. In an atomless population, one individual has zero mass, so the literal deviation becomes vacuous. A positive-mass transfer is instead a coordinated deviation by a whole type, hence a stronger and different notion; an infinitesimal derivative notion would be weaker and potentially vacuous. The paper does not resolve that semantic choice.

Thus the best positive claim is conditional: the paper supplies a very natural population object and a plausible Class-A robustness problem around Theorem 1. But under the programme’s strict rules, the correct final classification is “no qualifying computational anchor,” rather than a positive mirror verdict.

The case AGAINST (opponent, writing after the proponent)

The decisive objection is provenance. This paper contains no named computational result for ChoCo to continuize. Theorem 1 is an axiomatic possibility theorem; Theorem 2 is a characterization; Theorems 3–6 are existence impossibilities. The Isabelle/SMT verification behind Theorem 5 certifies a proof; it is not a complexity, algorithmic, approximation, or parameterized result. Under the programme’s named-result gate, there is therefore no computational object here whose high-multiplicity version can count as a mirror.

The proponent’s proposed robustness problem does not repair that gap. Weak strategyproofness concerns one voter changing one report while every other voter is fixed. In an atomless society, that voter has zero mass, so the deviation leaves the society unchanged and the axiom becomes vacuous. A positive-mass transfer is nontrivial, but it is a coordinated coalition deviation—a different strategic notion. Adding conversion costs, a target candidate, and a probability threshold creates a new bribery/control problem that the paper neither defines nor studies.

The plurality example makes the disconnect especially clear. With strict rankings, every unit of mass has exactly one top alternative, so the denominator in the proposed SDS is just total mass, namely one. The problem consequently reduces to minimum-cost mass transfer subject to a linear plurality threshold. That may be a perfectly legitimate ChoCo problem, but it would work for any linear population statistic; it uses neither weak strategyproofness nor the substantive score-based conditions of Theorem 1.

The strongest possible repair would define a continuum version of weak strategyproofness for a positive mass of identical voters changing reports. But that is group strategyproofness by another name. Taking the deviating mass to zero restores the vacuity problem; keeping it positive changes the strategic actor. Retaining individual atoms preserves the original axiom, but then one has not genuinely replaced the population by a continuum.

The other theorems do not help. Their finite counterexamples can be rewritten using rational masses, but that merely restates axiomatic impossibilities over a profile simplex. It does not produce the computational question the programme is designed to classify. Voting certainly has sensible high-multiplicity regimes; the failure is not the population model but the absence of a computational anchor.

So the strict negative verdict is strong: this paper does not supply a qualifying continuous mirror. The universal claim that no worthwhile extension could ever be designed is weaker than that verdict—one could study cohort manipulation or mass-transfer robustness—but such work would be an extension or re-modelling inspired by the paper, not a continuous mirror of one of its results.

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.