← back to the atlas

The Metric Distortion of Randomized Social Choice Functions: C1 Maximal Lottery Rules and Simulations (aamas25-00093)

Answer: Polynomial-time solvable in \(m,\tau,L\), including exact rational output for finite values and detection of \(+\infty\).

The anchor (named result in the paper)

Proposition 2 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateFix a profile 𝑅, a lottery 𝑝, and an alterna- tive 𝑥∗. If the optimal objective value 𝑜∗ 𝐿𝑃 of LP 1 is bounded, then dist(𝑝, 𝑅,𝑥∗) = 𝑜∗ 𝐿𝑃 and otherwise dist(𝑝, 𝑅,𝑥∗) = ∞.

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

The continuous mirror question, as graded

Given \(m\) alternatives \(X\), an explicit finite set \(T\) of complete ranking types with rational masses \(\mu_t\) summing to \(1\), a rational lottery \(p\in\Delta(X)\), and \(x^\ast\in X\), compute \(\sup_d \frac{\int_\Omega\sum_{x\in X}p(x)d(v,x)\,d\lambda(v)}{\int_\Omega d(v,x^\ast)\,d\lambda(v)}\), where \(\Omega\) is atomless, \(\lambda(\Omega_t)=\mu_t\), and \(d\) ranges over measurable metrics on \(\Omega\cup X\) consistent almost everywhere with each type's ranking, using the paper's \(0/0\) and positive-over-zero conventions.

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

Given \(m\geq 1\) alternatives \(X\), a society is given by its support: a list \(T\) of \(\tau\geq 1\) distinct strict complete ranking types with positive binary rational masses \(\mu_t\) summing to \(1\). Here \(\tau=|T|\) is the support size, not the number of possible rankings. Also given are a rational lottery \(p\in\Delta(X)\) and an alternative \(x^\ast\in X\); let \(L\) be the total binary input length.
Represent the society by \(\Omega=[0,1]\) with Lebesgue measure \(\lambda\), partitioned into intervals \(\Omega_t\) of lengths \(\mu_t\), disjoint from \(X\).
An admissible distance function is a finite-valued measurable pseudometric \(d\) on \(\Omega\sqcup X\), with integrable voter-to-alternative distances. Distinct points may have zero distance. For each \(t\), almost every \(v\in\Omega_t\) must satisfy \(d(v,x)\leq d(v,y)\) whenever \(x\succ_t y\); voters of the same type need not have identical distances.
Define \(D(T,\mu,p,x^\ast)=\sup_d \frac{\int_\Omega\sum_{x\in X}p(x)d(v,x)\,d\lambda(v)}{\int_\Omega d(v,x^\ast)\,d\lambda(v)}\), with \(0/0=1\) and \(z/0=+\infty\) for \(z>0\). The comparator \(x^\ast\) is fixed and need not minimize social cost.

Is computing \(D(T,\mu,p,x^\ast)\) exactly, including detecting \(+\infty\), possible in polynomial time in \(m,\tau,L\), or is this problem NP-hard?

For a finite electorate of \(n\) voters, the same fixed-comparator supremum is computable in polynomial time by a linear program with \(O(nm^2)\) constraints, including detection of an infinite value. [Frank and Lederer](https://arxiv.org/pdf/2403.18340)
No result settling this precise atomless computation problem was located in the literature search.

Modeling choices made when packaging the task

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

Result

The problem is polynomial-time solvable, including exact computation of every finite value and detection of \(+\infty\).

The key is that every admissible atomless pseudometric can be replaced by one whose distances depend only on voter types, while preserving all social costs. This gives a rational linear program with \(O((m+\tau)^2)\) variables and \(O((m+\tau)^3)\) constraints.

The proof below establishes this reduction directly. It does not require extending the specialized finite-electorate LP of [Frank and Lederer, Proposition 2](https://arxiv.org/pdf/2403.18340).

1. Exact aggregation by ranking type

Let \(Y=X\sqcup T\), where each element of \(T\) is treated as a new point representing its ranking type.

Lemma. For every admissible pseudometric \(d\) on \(\Omega\sqcup X\), there is a finite pseudometric \(q\) on \(Y\) such that

\(q(x,y)=d(x,y)\) for \(x,y\in X\), and

\[ \text{ } \]

\(q(t,x)=\dfrac{1}{\mu_t}\int_{\Omega_t}d(v,x)\,d\lambda(v)\)

for every \(t\in T\) and \(x\in X\). Moreover, \(q(t,x)\leq q(t,y)\) whenever \(x\succ_t y\).

Proof. For each \(t\in T\), let \(\nu_t\) be the probability measure obtained by restricting Lebesgue measure to \(\Omega_t\) and dividing by \(\mu_t\). For each \(x\in X\), let \(\nu_x\) be the point mass at \(x\).

For distinct \(i,j\in Y\), define

\(q(i,j)=\displaystyle\int\!\!\int d(a,b)\,d\nu_i(a)\,d\nu_j(b),\)

and set \(q(i,i)=0\).

These integrals are finite. Indeed, the triangle inequality gives

\(d(a,b)\leq d(a,x^\ast)+d(b,x^\ast).\)

Each term on the right is integrable under the relevant probability measure: for a type measure this follows from the assumed integrability of voter-to-alternative distances and \(\mu_t>0\); for an alternative point mass it follows from finite-valuedness of \(d\). Measurability and Tonelli’s theorem therefore justify the integrals.

Nonnegativity and symmetry follow from the corresponding properties of \(d\). For three distinct labels \(i,j,k\in Y\), integrate

\(d(a,c)\leq d(a,b)+d(b,c)\)

against the product probability measure \(\nu_i\otimes\nu_j\otimes\nu_k\). The marginals give exactly

\(q(i,k)\leq q(i,j)+q(j,k).\)

If labels repeat, the triangle inequality follows directly from \(q(i,i)=0\), symmetry, and nonnegativity. Thus \(q\) is a pseudometric.

The stated formulas for alternative-to-alternative and type-to-alternative distances follow from the definitions. Finally, integrating the almost-everywhere inequality \(d(v,x)\leq d(v,y)\) over \(\Omega_t\) gives \(q(t,x)\leq q(t,y)\). This proves the lemma.

2. Every finite type pseudometric is realizable

Conversely, suppose \(q\) is a finite pseudometric on \(Y\) satisfying the ranking inequalities.

Define \(f:\Omega\sqcup X\to Y\) by \(f(v)=t\) for \(v\in\Omega_t\), and \(f(x)=x\) for \(x\in X\). Set

\(d_q(a,b)=q(f(a),f(b)).\)

Pullback preserves nonnegativity, symmetry, zero self-distance, and every triangle inequality. Hence \(d_q\) is a pseudometric. It is measurable because it is constant on the finitely many products of partition pieces, and it is bounded because \(Y\) is finite. Its voter-to-alternative distances are therefore integrable.

For \(v\in\Omega_t\), the ranking inequalities hold because \(d_q(v,x)=q(t,x)\). Thus \(d_q\) is admissible, and

\(\displaystyle\int_\Omega d_q(v,x)\,d\lambda(v)=\sum_{t\in T}\mu_tq(t,x).\)

Applying this construction to the aggregated pseudometric from Section 1 preserves the social cost of every alternative.

Consequently, the possible pairs of numerator and denominator in the atomless problem are exactly those obtained from finite pseudometrics on \(X\sqcup T\) satisfying the rankings.

3. The linear program

Let \(C\) be the set of arrays \(q\) indexed by \(Y\times Y\) satisfying:

This is a polyhedral cone: all its constraints are homogeneous and linear.

Define the two linear functionals

\(A(q)=\displaystyle\sum_{t\in T}\mu_t\sum_{x\in X}p(x)q(t,x),\)

\(B(q)=\displaystyle\sum_{t\in T}\mu_tq(t,x^\ast).\)

By Sections 1 and 2, the original problem is precisely the supremum of \(A(q)/B(q)\) over \(q\in C\), with the given zero-denominator conventions.

Consider the rational linear program

\(\displaystyle \text{maximize }A(q)\quad\text{subject to }q\in C,\qquad B(q)=1.\)

It is always feasible. In particular, define \(q^0\) by assigning distance zero between any two type points, distance zero between any two alternatives, and distance one between a type point and an alternative. This is a pseudometric satisfying every ranking inequality. Since the masses and lottery probabilities each sum to one,

\(B(q^0)=A(q^0)=1.\)

Thus the LP value is at least \(1\).

4. Equality with the original supremum

Let \(V\) be the LP supremum, allowing \(V=+\infty\).

First, every LP-feasible \(q\) pulls back to an admissible atomless pseudometric with denominator \(1\) and numerator \(A(q)\). Therefore,

\(D(T,\mu,p,x^\ast)\geq V.\)

For the reverse inequality, take any \(q\in C\).

Positive denominator. If \(B(q)>0\), homogeneity gives \(q/B(q)\in C\) with denominator one. Hence

\(\dfrac{A(q)}{B(q)}=A\!\left(\dfrac{q}{B(q)}\right)\leq V.\)

Zero denominator and zero numerator. If \(B(q)=A(q)=0\), its prescribed ratio is \(1\), which is at most \(V\).

Zero denominator and positive numerator. If \(B(q)=0<A(q)\), then, for every real \(s\geq0\),

\(q^0+s q\in C,\qquad B(q^0+s q)=1,\qquad A(q^0+s q)=1+sA(q).\)

The LP is therefore unbounded, so \(V=+\infty\), matching the prescribed ratio.

These cases exhaust all possibilities because \(A(q)\) and \(B(q)\) are nonnegative. Together with the aggregation equivalence, they prove

\(D(T,\mu,p,x^\ast)=V.\)

In particular, the original supremum is infinite exactly when the normalized LP is unbounded.

5. Exact polynomial-time computation

Write \(N=m+\tau\). Using one variable for each unordered pair of distinct points in \(Y\), the LP has:

All constraint coefficients are rational. The metric and ranking constraints use only small integer coefficients; normalization uses the input masses \(\mu_t\); the objective uses products \(\mu_t p(x)\). Multiplying two input rationals increases their binary encoding length by at most the sum of their encoding lengths, up to a constant. Thus the entire LP has encoding length polynomial in \(m,\tau,L\).

We apply the standard polynomial-time theorem for rational linear programming: an explicitly represented rational LP can be classified as infeasible, unbounded, or having a finite optimum in time polynomial in its binary encoding length; in the finite case, its exact rational optimum and an optimal rational solution can be computed in polynomial time. The required hypotheses hold here, and feasibility has already been established.

Therefore the algorithm returns \(+\infty\) if the LP is unbounded, and otherwise returns its exact rational optimum. In the finite case, pulling back an optimal solution also shows that the atomless supremum is attained.

⟨structured verdict parsed — rendered above⟩

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

The prover’s claim is proved. The aggregation preserves every alternative’s social cost, the normalized LP handles all denominator cases correctly, and its explicit rational encoding has polynomial size. I found no major or minor mathematical issues.

Each \(\nu_t\) is a probability measure because \(\mu_t>0\). For every label \(i\in Y\), the function \(a\mapsto d(a,x^\ast)\) is integrable under \(\nu_i\): this follows from the assumed voter-to-alternative integrability for type labels, and finite-valuedness for alternative labels.

The stated bound
\[ d(a,b)\leq d(a,x^\ast)+d(b,x^\ast) \]
therefore bounds each defining double integral by a finite quantity. Measurability and nonnegativity justify Tonelli’s theorem, and the bound establishes finiteness. No integrability of voter-to-voter distances needs to be assumed separately.

Nonnegativity and symmetry follow from those of \(d\), and the diagonal is explicitly set to zero.

For three distinct labels, integrating the pointwise triangle inequality against the three probability measures gives exactly the claimed inequality. Each term reduces to its corresponding double integral because the unused measure has total mass one.

Resetting diagonal entries to zero causes no difficulty: when labels repeat, the triangle inequality reduces either to an equality or to nonnegativity. In particular, the argument does not incorrectly identify \(q(t,t)\) with the potentially positive average distance between two voters of type \(t\).

Point masses give \(q(x,y)=d(x,y)\), and the normalized type measures give the stated formula for \(q(t,x)\). Integrating each almost-everywhere ranking inequality preserves its direction. All conclusions of the lemma follow.

The map \(f\) is defined on the given partition and fixes alternative labels. Pulling back \(q\) preserves the pseudometric axioms, including triangle inequalities involving voters of the same type.

The resulting distance function is measurable on the finite collection of products of partition pieces. It is bounded because \(Y\) is finite, so every voter-to-alternative distance is integrable. Its ranking inequalities hold throughout each type piece.

The displayed social-cost formula follows from constancy on each piece and its measure \(\mu_t\). Thus the two constructions establish the asserted equality of attainable numerator-denominator pairs. Neither construction requires voters originally sharing a type to have identical distances.

The constraints defining \(C\) are precisely the finite pseudometric axioms and the required weak ranking inequalities. They are homogeneous linear constraints, so the stated cone properties are valid.

The proposed \(q^0\) is a valid pseudometric. Distances within either class are zero, and distances between classes are one; its triangle inequalities hold for every placement of the three labels. All ranking inequalities hold with equality.

Since the masses and lottery probabilities each sum to one, the computation \(A(q^0)=B(q^0)=1\) is correct. Consequently, normalization is always feasible and its supremum is at least one.

Every normalized feasible point is realizable, establishing \(D\geq V\).

Conversely:

Nonnegativity of both functionals makes these cases exhaustive. This establishes \(D=V\), including the stated equivalence between an infinite original supremum and an unbounded normalized LP. The argument also covers an infinite supremum arising from arbitrarily large positive-denominator ratios.

With \(N=m+\tau\), the variable count \(\binom{N}{2}\), the \(O(N^3)\) triangle-constraint count, and the \(O(\tau m^2)\) ranking-constraint count are correct. Symmetry and zero diagonal can be incorporated through the unordered-pair representation.

All coefficients are rational. The products \(\mu_t p(x)\) have binary encoding length bounded polynomially by the input length, and the explicitly enumerated LP has polynomial total encoding length in \(m,\tau,L\).

The rational linear-programming theorem is stated with the relevant computational guarantees: polynomial-time classification and exact rational optimization for a finite optimum. Its hypotheses are satisfied by this explicitly represented rational LP, whose feasibility has already been established. Its application therefore justifies both exact finite output and detection of infinity.

The finite-attainment claim also follows from the stated theorem’s optimal-solution guarantee and the already verified pullback construction.

The argument never requires \(x^\ast\) to minimize social cost. It permits zero distances between distinct points, as the task requires. Positive masses justify every division by \(\mu_t\), while zero lottery probabilities cause no difficulty. The construction remains valid for \(m=1\) and for \(\tau=1\).

No additional clarification or repair is needed. The empty display in Section 1 is a harmless formatting artifact and does not obscure any mathematical assertion.

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