← back to the atlas

On the existence of Pareto Efficient and envy-free allocations (d4-journals-jet-2021-0049)

Answer: Requires exponentially many communicated bits in \(m\), even for \(\tau=2\) and \(L=O(\log m)\); an upper bound of \(O(2^mL)\) bits holds.

The anchor (named result in the paper)

Theorem 3.2 — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximateAny protocol that calculates Pareto Efficient and envy-free allocation for two players with submodular uility functions needs an exponential number of bits.

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

The continuous mirror question, as graded

Given private submodular utility types \(u_L,u_R:2^{[m]}\to\mathbb{Q}\), each of mass \(\frac12\), and an atomless population of independent cells with one integral copy of every item per cell, output a mass vector \(x=(x_A)_{A\subseteq[m]}\) with \(x_A\ge0\) and \(\sum_A x_A=1\). Define \(U_L(x)=\sum_Ax_Au_L(A)\), \(U_R(x)=\sum_Ax_Au_R([m]\setminus A)\), and require \(U_L(x)\ge\sum_Ax_Au_L([m]\setminus A)\) and \(U_R(x)\ge\sum_Ax_Au_R(A)\), with no feasible \(y\) Pareto-improving both type-average utilities. Determine the worst-case communication needed for the two types to agree on \(x\).

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

A society is given by its support: the list of the \(\tau\) types with positive mass, each mass a binary rational; \(\tau\) is the support size, not the number of possible types. Here \(\tau=2\), with types \(L,R\) each of mass \(\frac12\).
Each type privately knows its submodular utility \(u_i:2^{[m]}\to\mathbb Q\), with each value encoded in at most \(L\) bits, where \(L\) is polynomially bounded in \(m\). Values may have either sign; monotonicity and normalization are not required.
The atomless population consists of cells of total measure one, each containing one representative of each type and one integral copy of each item. Items cannot move between cells. Every partition \((A,[m]\setminus A)\) is allowed.
An allocation is \(x_A\ge0\) with \(\sum_{A\subseteq[m]}x_A=1\), where \(x_A\) is the measure of cells assigning \(A\) to type \(L\). Define \(U_L(x)=\sum_Ax_Au_L(A)\) and \(U_R(x)=\sum_Ax_Au_R([m]\setminus A)\).
Require \(U_L(x)\ge\sum_Ax_Au_L([m]\setminus A)\) and \(U_R(x)\ge\sum_Ax_Au_R(A)\). Also require that no allocation \(y\), whether envy-free or not, satisfies \(U_i(y)\ge U_i(x)\) for both types with at least one strict inequality.
Two parties, each knowing only its own utility, must agree on an exact rational allocation, represented by its nonzero coordinates. Use deterministic protocols with unrestricted local computation; measure communicated bits in \(m,\tau,L\), and state any running times in these parameters.

Does this allocation problem admit communication polynomial in \(m,\tau,L\), or does it require exponentially many communicated bits in \(m\) even when \(\tau=2\)?

Known results: Cole and Tao establish existence and an exponential communication lower bound for two-player envy-free, Pareto-efficient mixed allocations with submodular utilities, together with an exponential communication upper bound ([original source](https://arxiv.org/html/1906.07257)). The formulation above has exactly the same feasible vectors, utility expressions, and private inputs as that mixed-allocation problem; consequently this target is already settled, rather than open.

Modeling choices made when packaging the task

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

Result

The problem requires exponentially many communicated bits in \(m\), even when \(\tau=2\) and \(L=O(\log m)\). An exponential communication upper bound also holds, with exact rational output.

Applying the known lower bound

Cole and Tao’s Theorem 3.2 gives an exponential communication lower bound for finding an envy-free, Pareto-efficient mixed allocation between two players with submodular utilities. The paper states a bound of \(\Omega(2^{m/2})\); its hard instances have integer utility values between \(0\) and \(3m/2\), requiring only \(O(\log m)\) bits per value. Theorem 3.1 establishes existence for finite allocation sets closed under swapping players’ bundles. [Cole–Tao, *On the Existence of Pareto Efficient and Envy-Free Allocations*, Sections 3 and 5](https://arxiv.org/html/1906.07257)

Here is the precise identification of models. Write \(A^c=[m]\setminus A\). Identify a pure two-player allocation with the partition \((A,A^c)\), and identify its mixing probability with \(x_A\). Then:

The cell interpretation introduces no additional restriction: an atomless space can be partitioned into finitely many measurable pieces of prescribed measures \(x_A\), with partition \((A,A^c)\) implemented on the corresponding piece.

Consequently, any deterministic protocol for the stated problem would also solve the cited mixed-allocation problem with identical communication. Requiring exact rational output restricts acceptable outputs and cannot invalidate that lower bound.

Since the hard family has \(\tau=2\) and \(L=O(\log m)\), communication polynomial in \(m,\tau,L\) is impossible.

Exact rational solutions with small support

For completeness, the exact-output requirement causes no existence obstruction. I prove that a suitable allocation always exists with at most three nonzero coordinates, each having \(O(L)\)-bit rational probability.

Define
\[ a_A=u_L(A),\qquad b_A=u_R(A^c), \]
and
\[ d_{L,A}=u_L(A)-u_L(A^c),\qquad d_{R,A}=u_R(A^c)-u_R(A). \]

Let \(E\) be the polytope given by the probability-simplex constraints and
\[ \sum_A d_{L,A}x_A\geq0,\qquad \sum_A d_{R,A}x_A\geq0. \]

The pure allocation set is finite and closed under swapping, because swapping replaces \(A\) by \(A^c\). The existence theorem therefore supplies \(x^*\in E\) that is Pareto efficient. Its applicability does not require nonnegative, normalized, or monotone utilities.

A positive supporting objective

Put \(p_L=U_L(x^*)\) and \(p_R=U_R(x^*)\). Consider the linear program
\[ \max_y\ \sum_A(a_A+b_A)y_A \]
subject to
\[ y_A\geq0,\qquad \sum_Ay_A=1,\qquad \sum_Aa_Ay_A\geq p_L,\qquad \sum_Ab_Ay_A\geq p_R. \]

It is feasible and bounded. Pareto efficiency implies that its optimum is \(p_L+p_R\): any larger objective value would give a Pareto improvement.

Its dual is
\[ \min_{t,\alpha,\beta}\ t-\alpha p_L-\beta p_R \]
subject to
\[ \alpha,\beta\geq0,\qquad t\geq(1+\alpha)a_A+(1+\beta)b_A \quad\text{for every }A. \]

By linear-programming strong duality, an optimal dual solution exists. Set \(w_L=1+\alpha>0\) and \(w_R=1+\beta>0\). Equality of the primal and dual optima gives
\[ t=w_Lp_L+w_Rp_R. \]
Thus \(x^*\) maximizes \(w_LU_L+w_RU_R\) over the entire allocation simplex.

Let \(I\) contain precisely the partitions maximizing \(w_La_A+w_Rb_A\). Every allocation supported on \(I\) maximizes this positive weighted objective and is therefore Pareto efficient: a Pareto improvement would strictly increase that objective.

A rational vertex

The polytope
\[ Q=\{x\in E:x_A=0\text{ whenever }A\notin I\} \]
is nonempty because it contains \(x^*\). Its defining coefficients are rational, even if the supporting weights are irrational. Choose a vertex \(z\) of \(Q\).

This is also a vertex of \(E\). Indeed, if \(z\) were a nontrivial convex combination of two points of \(E\), nonnegativity and its zero coordinates outside \(I\) would force both points to lie in \(Q\), contradicting its extremality there.

Let \(s\) be the number of positive coordinates of \(z\), and let \(r\leq2\) be the number of active envy inequalities. If \(s>1+r\), there is a nonzero perturbation on those \(s\) coordinates preserving normalization and all active envy equalities. Sufficiently small perturbations in both directions preserve positivity and the inactive inequalities. This contradicts extremality. Hence
\[ s\leq1+r\leq3. \]

The positive coordinates are determined by an invertible subsystem consisting of normalization and at most two active envy equalities. Its coefficients have \(O(L)\)-bit rational encodings. Cramer’s rule for a matrix of order at most three gives \(O(L)\)-bit rational coordinates.

Thus \(z\) is an exact rational, envy-free, Pareto-efficient allocation whose representation uses \(O(m+L)\) bits.

An exponential upper bound and local running time

The parties exchange their complete utility tables in a public subset order. There are \(2^m\) values per party, so this costs \(O(2^mL)\) communicated bits. Both then perform the same deterministic computation:

The Pareto test is exact: its optimum exceeds \(U_L(x)+U_R(x)\) exactly when a Pareto improvement exists. The preceding argument guarantees that some enumerated candidate passes.

There are \(O(2^{3m})\) candidate systems. Exact rational linear programming takes time polynomial in its explicitly encoded input size, so the local computation after tabulation takes \(2^{O(m)}\operatorname{poly}(L)\) bit operations. This excludes any unspecified cost of evaluating the private utility functions to obtain their tables.

Therefore, for \(\tau=2\), the worst-case communication is exponential: a lower bound of \(\Omega(2^{m/2})\) on the cited hard family and an upper bound of \(O(2^mL)\). The lower bound persists despite the existence of succinct exact outputs.

⟨structured verdict parsed — rendered above⟩

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

Verdict

The prover resolves the assigned problem correctly. The exponential communication lower bound applies to the stated model, and the additional argument establishes that exact rational output is always possible with small support. The proposed upper-bound protocol is valid.

No major or minor mathematical issues were found.

Step-by-step verification

1. The cited results and their applicability

The cited paper defines mixed allocations as distributions over allowable assignments, envy-freeness through expected bundle comparisons, and Pareto efficiency against all mixed allocations. Theorem 3.1 assumes a swappable allocation set. The communication setting uses private utility functions and includes all partitions; Theorem 3.2 supplies the submodular two-player lower bound. These match the hypotheses used by the prover. [Cole–Tao, Sections 3–5](https://arxiv.org/html/1906.07257)

The claimed quantitative bound \(\Omega(2^{m/2})\) appears in the paper’s introduction. Its hard construction uses \(m=2p\) items and integer values bounded by \(3p=3m/2\), so the asserted \(O(\log m)\) encoding length is valid. Restricting to this even-item family already excludes communication polynomial in the task’s parameters. [Cole–Tao, introduction and Section 5](https://arxiv.org/html/1906.07257)

The existence result permits arbitrary cardinal utilities. Thus the task’s allowance of negative values and lack of normalization or monotonicity do not obstruct its application. [Cole–Tao, abstract and Theorem 3.1](https://arxiv.org/html/1906.07257)

2. Identification of the two models

All five identifications are correct:

The atomless-cell interpretation imposes no extra restriction on these vectors: there are finitely many partitions, and prescribed nonnegative measures summing to one can be realized by measurable pieces of an atomless probability space.

The fixed type masses introduce no additional input or constraint in the explicitly defined utility expressions. In particular, the proof does not confuse support size with the number of possible types.

Consequently, the lower-bound transfer preserves both private information and communication cost. Requiring exact rational output cannot weaken a lower bound applying to protocols allowed to return arbitrary valid mixed allocations.

3. Existence of an envy-free, Pareto-efficient starting point

The polytope \(E\) correctly encodes normalization, nonnegativity, and both envy inequalities.

The pure allocation set is finite and closed under exchanging the players’ bundles, since this sends \(A\) to \(A^c\). The existence theorem therefore supplies the claimed \(x^*\).

No submodularity assumption is needed for this existence step; submodularity is used in the cited lower bound.

4. The positive supporting objective

The auxiliary primal linear program is correctly formulated.

The displayed dual has the correct signs. The lower-bound utility constraints produce nonnegative multipliers \(\alpha,\beta\), the dual objective is \(t-\alpha p_L-\beta p_R\), and the coordinate constraints are
\[ t\geq(1+\alpha)a_A+(1+\beta)b_A. \]

Finite-dimensional linear-programming strong duality applies to this feasible, bounded primal and supplies an attained dual optimum. Equality of the optimal values gives the stated identity for \(t\).

Thus \(x^*\) maximizes the positive weighted objective over the entire simplex. Both weights are strictly positive, so every allocation attaining this maximum is Pareto efficient. This excludes improvements with either one or both utility coordinates strict.

5. The rational vertex and support bound

The set \(I\) is a finite set of maximizing partitions. The supporting-objective conclusion ensures that \(x^*\) has no positive coordinate outside \(I\), so \(Q\) is nonempty.

Although the weights used to identify \(I\) need not be rational, the constraints defining \(Q\) are rational: they consist of the rational constraints of \(E\) and coordinate equations. The argument does not require computing those weights.

The transfer of extremality from \(Q\) to \(E\) is valid. Nonnegative coordinates prevent a convex decomposition in \(E\) from introducing positive mass outside the support restriction.

The perturbation argument correctly yields \(s\leq1+r\leq3\):

This contradicts the vertex property. Dependence among active equations does not invalidate the argument.

At a vertex, the normalization and active envy equations have full rank on the positive coordinates. An invertible subsystem therefore determines those coordinates. Utility differences have \(O(L)\)-bit rational encodings, and the system has order at most three. The stated Cramer’s-rule bit bound is valid.

The resulting representation uses \(O(m+L)\) bits: at most three subset identifiers and three rational probabilities.

6. Communication protocol and running time

Exchanging the two complete tables costs \(O(2^mL)\) bits under a fixed public subset order.

The enumeration covers the vertex established above because it includes every support of size at most three and the relevant choices of active envy equalities. Feasibility checks exclude invalid candidates.

The Pareto test is exact. Its threshold constraints prohibit losses, and its objective exceeds the candidate’s utility sum exactly when at least one player strictly gains.

The number of candidate systems is \(O(2^{3m})\). Each Pareto test has explicitly encoded rational data of size \(2^{O(m)}\operatorname{poly}(L)\), so polynomial-time exact rational linear programming gives the claimed total bound \(2^{O(m)}\operatorname{poly}(L)\).

The qualification excluding unspecified utility-evaluation costs is appropriate: the task supplies unrestricted local computation without specifying how private functions are accessed. Once their tables are available, the stated computation bound is justified.

Both parties can use the same fixed enumeration and exact tests, so agreement requires no further communication.

Feedback to the prover

No repair is required. The conclusion, exact-output guarantee, communication bounds, and stated local-computation bound are supported by the write-up.

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