Answer: Polynomial-time solvable: the decision problem belongs to \(\mathrm P\), with running time \((m\tau(L+\log(m\tau)))^{O(1)}\).
Proposition A.2 — class: algorithmic
Given \(m\), rational types \(s^1,\ldots,s^\tau\in\Delta^m\), rational masses \(\mu\in\Delta^\tau\), and \(\bar{x}\in\Delta^m\), decide whether there exists \(y\in\Delta^m\) such that \(d_t(y)\le d_t(\bar{x})\) for every \(t\) with \(\mu_t>0\), with strict inequality for at least one such \(t\), where \(d_t(z)=\sum_{j=1}^m|s^t_j-z_j|\).
Let \(m\ge 2\) and \(\Delta^k=\{z\in\mathbb R_{\ge0}^k:\sum_{j=1}^k z_j=1\}\).
A society is given by its support: \(\tau\ge1\) distinct rational types \(s^1,\ldots,s^\tau\in\Delta^m\), each with a positive binary rational mass \(\mu_t\), where \(\sum_{t=1}^\tau\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types.
The input also contains a rational outcome \(\bar x\in\Delta^m\); let \(L\) be the total binary input bit length. State running times in \(m,\tau,L\).
For each supported type, define \(d_t(z)=\sum_{j=1}^m|s_j^t-z_j|\).
Decide whether there exists a real outcome \(y\in\Delta^m\) satisfying \(d_t(y)\le d_t(\bar x)\) for every supported type, with strict inequality for at least one supported type.
Is this decision problem in \(\mathrm P\), with running time polynomial in \(m,\tau,L\), or is it \(\mathrm{NP}\)-hard?
For a finite list of agents with these ideal distributions and disutilities, checking Pareto optimality—and hence deciding whether a Pareto improvement exists—is polynomial-time solvable. No separate result for the mass-input version is supplied.
The decision problem is in \(\mathrm P\), with running time polynomial in \(m,\tau,L\). The masses do not enter the algorithm: the requested inequalities concern exactly the \(\tau\) supported types.
For each \(t\in\{1,\ldots,\tau\}\), compute the rational threshold
\(D_t=d_t(\bar x)=\sum_{j=1}^m|s_j^t-\bar x_j|\), and let \(B=\sum_{t=1}^{\tau}D_t\).
Introduce outcome variables \(y_j\) and auxiliary variables \(a_{tj}\). Consider the following rational linear program:
The absolute-value constraints imply
\(a_{tj}\ge |s_j^t-y_j|\). Consequently, every feasible solution satisfies
\(d_t(y)\le\sum_{j=1}^m a_{tj}\le D_t\) for every supported type.
The program is feasible: take \(y=\bar x\) and \(a_{tj}=|s_j^t-\bar x_j|\). This solution has objective value \(B\).
An optimum is attained. Indeed, every feasible outcome has \(0\le y_j\le 1\). Also,
\(D_t\le\sum_{j=1}^m(s_j^t+\bar x_j)=2\), so nonnegativity and the row-sum constraints give \(0\le a_{tj}\le 2\). Thus the feasible region is nonempty, closed, and bounded. Write \(F^\star\) for its minimum objective value.
We prove that a Pareto improvement exists if and only if \(F^\star<B\).
An improvement implies \(F^\star<B\). Suppose \(y\in\Delta^m\) satisfies \(d_t(y)\le D_t\) for every \(t\), with strict inequality for at least one \(t\). Set \(a_{tj}=|s_j^t-y_j|\). These variables satisfy every constraint, and their objective value is
\(F=\sum_{t=1}^{\tau}d_t(y)<\sum_{t=1}^{\tau}D_t=B\).
Hence \(F^\star<B\).
The inequality \(F^\star<B\) implies an improvement. Let \((y,a)\) be an optimal solution. Feasibility gives \(d_t(y)\le D_t\) for every \(t\), while
\(\sum_{t=1}^{\tau}d_t(y)\le\sum_{t=1}^{\tau}\sum_{j=1}^m a_{tj}=F^\star<B\).
If every type had \(d_t(y)=D_t\), the leftmost sum would equal \(B\), contradicting this inequality. Therefore at least one supported type strictly improves.
The algorithm therefore solves the linear program exactly and answers “yes” precisely when \(F^\star<B\). It requires no numerical tolerance for strict inequalities.
The program has \(m+m\tau\) variables and \(O(m\tau)\) constraints.
The thresholds \(D_t\) and \(B\) can be computed exactly in polynomial time. To check their encoding lengths, let \(Q\) be the product of the denominators of all input coordinates. Its binary length is \(O(L)\). Every coordinate difference, every \(D_t\), and \(B\) can be represented using denominator \(Q\). Since \(D_t\le 2\) and \(B\le 2\tau\), their numerators have binary length \(O(L+\log(m\tau))\). All remaining coefficients belong to \(\{-1,0,1\}\).
Thus, even with a dense matrix encoding, the linear program has total binary length
\(O((m\tau)^2(L+\log(m\tau)))\).
The polynomial-time theorem for rational linear programming applies to this explicitly represented rational program: an exact optimum can be computed in time polynomial in its binary encoding length. See the [MIT linear programming algorithm notes](https://courses.csail.mit.edu/6.854/21/Scribe/s14-lpAlgorithms/s14-lpAlgorithms.html). Comparing that rational optimum with \(B\) also takes polynomial time. The resulting running time can be stated as
\((m\tau(L+\log(m\tau)))^{O(1)}\).
No expansion into agents according to the masses is necessary. Even exponentially small positive masses leave the program’s size unchanged.
⟨structured verdict parsed — rendered above⟩
The prover resolves the assigned problem correctly. The LP characterizes the existence of a real Pareto improvement, and its size and rational encoding length are polynomial in \(m,\tau,L\). No substantive or minor gaps were found.
The task imposes one weak inequality for each supported type and requires at least one strict inequality. The masses do not occur in these conditions. Consequently, omitting the positive masses from the optimization is correct.
The prover uses precisely \(\tau\) supported types and does not expand rational masses into repeated agents. Thus it addresses the specified input representation directly.
Each threshold \(D_t=d_t(\bar x)\) is a nonnegative rational number computable from the input.
For every pair \(t,j\), the inequalities
\(a_{tj}\ge s_j^t-y_j\) and \(a_{tj}\ge y_j-s_j^t\)
give \(a_{tj}\ge |s_j^t-y_j|\). Summing and applying the row constraint yields
\(d_t(y)\le\sum_j a_{tj}\le D_t\).
Conversely, any outcome satisfying all the required weak inequalities admits the auxiliary assignment \(a_{tj}=|s_j^t-y_j|\). This assignment satisfies every auxiliary and row constraint. The formulation therefore neither excludes an eligible outcome nor admits an outcome violating a weak inequality.
The proposed feasible point \(y=\bar x\), \(a_{tj}=|s_j^t-\bar x_j|\) satisfies every constraint and has objective value \(B\).
The bound \(D_t\le 2\) follows from \(|s_j^t-\bar x_j|\le s_j^t+\bar x_j\) and the two simplex equalities. Nonnegativity and the row constraints then imply \(0\le a_{tj}\le 2\). The outcome coordinates satisfy \(0\le y_j\le 1\).
The feasible region is a nonempty, closed, bounded subset of a finite-dimensional real space. Its linear objective therefore attains a minimum. This justifies the subsequent use of an optimal solution.
For an improving outcome, the exact absolute-value assignment has objective
\(F=\sum_t d_t(y)\).
Every summand is at most \(D_t\), and at least one is strictly smaller. Since the sum is finite, \(F<B\), hence \(F^\star<B\).
This direction is valid for real outcomes; rationality of the improving witness is not assumed.
At an optimal feasible solution, each type satisfies \(d_t(y)\le D_t\), and
\(\sum_t d_t(y)\le F^\star<B\).
If every weak inequality were an equality, this sum would equal \(B\). Therefore at least one type strictly improves.
The argument remains valid even if some auxiliary variables exceed their corresponding absolute values. No unstated equality between those quantities is needed.
There are \(m+m\tau\) variables and \(O(m\tau)\) constraints. These counts include the simplex, nonnegativity, absolute-value, and row constraints.
The denominator-product argument is correct: the binary length of \(Q\) is bounded by the sum of the input denominator lengths, hence is \(O(L)\). Every coordinate difference, threshold, and \(B\) has a representation with denominator \(Q\). The bounds \(D_t\le 2\) and \(B\le 2\tau\) establish polynomial numerator lengths.
The matrix and objective coefficients are in \(\{-1,0,1\}\). The original type coordinates also appear as rational right-hand sides; their encoding lengths are already bounded by \(L\). Thus the stated dense encoding bound
\(O((m\tau)^2(L+\log(m\tau)))\)
is valid.
The invoked theorem is the standard polynomial-time solvability of explicitly represented rational LPs, including exact rational optimization when a finite optimum exists. Its hypotheses are satisfied: the program has rational data, polynomial encoding length, and a feasible attained finite optimum. The [cited MIT notes](https://courses.csail.mit.edu/6.854/21/Scribe/s14-lpAlgorithms/s14-lpAlgorithms.html) discuss polynomial-time LP algorithms and recovery of a vertex after approaching optimality.
Exact comparison of the rational optimum with \(B\) takes polynomial time. Hence the stated running time
\((m\tau(L+\log(m\tau)))^{O(1)}\)
follows, without numerical tolerance.
The proof covers \(\tau=1\), zero thresholds, boundary outcomes, and arbitrarily small positive masses. In particular, if \(B=0\), nonnegativity forces \(F^\star=0\), and the algorithm correctly rejects improvement.
No repair or additional clarification is required.
⟨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.