← back to the atlas

Fairly Allocating Goods in Parallel (aamas25-00099)

Answer: —

The anchor (named result in the paper)

Theorem 6.6 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateAlgorithm 1 is a parallel algorithm that returns an EF1 and Pareto Optimal allocation of 𝑚 indivisible items to 𝑛 agents with restricted-additive valuations, from a set of 𝑡 different inherent item-values, in time 𝑂(log2(𝑚𝑛)) using 𝑂(𝑚5.5+𝑡𝑛5.5) processors. Notice that binary valuations are a special case of restricted additive valuations (with one inherent item value). Thus, we get an RNC algorithm for binary valuations.

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

The continuous mirror question, as graded

Given rational good-class supplies \(\rho_g\), inherent values \(w_g\), a finite type set \(\Theta\) with rational masses \(\mu_\theta\), valuation masks \(A_\theta\), and a bundle-size bound \(K\), let \(y_{\theta,b}\) be the mass of type \(\theta\) receiving integral bundle \(b \in \mathbb{Z}_{\ge 0}^q\) with \(\lVert b \rVert_1 \le K\). Require \(\sum_b y_{\theta,b}=\mu_\theta\) and \(\sum_{\theta,b} b_g y_{\theta,b}=\rho_g\). Output a finite-support law satisfying support-wise \(\mathrm{EF1}\) and population Pareto optimality, where for every supported pair either \(u_\theta(b) \ge u_\theta(b')\) or some integral good can be removed from \(b'\) to make that inequality hold, and no measure-preserving reassignment weakly improves every agent while strictly improving positive mass.

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

A society is an atomless population of total mass \(1\), given by its support: a list \(\Theta\) of \(\tau\) types with positive binary-rational masses \(\mu_\theta\) summing to \(1\). Here \(\tau\) is the support size, not the number of possible types.
There are \(m\geq1\) good classes, with positive binary-rational supplies \(\rho_g\) and inherent values \(w_g\). Type \(\theta\) has a mask \(A_\theta\subseteq\{1,\ldots,m\}\) and restricted additive utility \(u_\theta(b)=\sum_{g\in A_\theta}w_gb_g\); every class belongs to at least one mask. Let \(t=|\{w_g:g=1,\ldots,m\}|\).
Given a binary-encoded integer \(K\geq1\), admissible bundles are \(B_K=\{b\in\mathbb Z_{\geq0}^{m}:\|b\|_1\leq K\}\). A law consists of nonnegative rational masses \(y_{\theta,b}\), listed only where positive, satisfying \(\sum_b y_{\theta,b}=\mu_\theta\) and \(\sum_{\theta,b}b_gy_{\theta,b}=\rho_g\).
Support-wise EF1 means that for every ordered pair \((\theta,b),(\theta',b')\) with positive mass, either \(u_\theta(b)\geq u_\theta(b')\), or there is a class \(g\) with \(b'_g>0\) such that \(u_\theta(b)\geq u_\theta(b'-e_g)\), where \(e_g\) is the corresponding unit vector.
Population Pareto optimality means there is no nonnegative real reassignment \(z_{\theta,b,c}\), with \(b,c\in B_K\), satisfying \(\sum_c z_{\theta,b,c}=y_{\theta,b}\) and \(\sum_{\theta,b,c}c_gz_{\theta,b,c}=\rho_g\), such that every positive entry has \(u_\theta(c)\geq u_\theta(b)\) and \(\sum_{\theta,b,c:\,u_\theta(c)>u_\theta(b)}z_{\theta,b,c}>0\). Competing reassignments need not satisfy EF1.
Find a finite-support law satisfying both properties, or determine that none exists. Let \(L\) be the total binary input length; state running times in \(m,\tau,L,K,t\).

Is this problem solvable in time polynomial in \(m,\tau,L\), or is it NP-hard?

For finite societies without a bundle cap, [Garg and Psomas](https://www.ifaamas.org/Proceedings/aamas2025/pdfs/p839.pdf) give a randomized parallel EF1 and Pareto-optimal allocation algorithm taking \(O(\log^2(mn))\) time with \(O(m^{5.5+t}n^{5.5})\) processors, where \(n\) is the number of agents; for fixed \(t\), this gives polynomial sequential time.
No result settling this exact support-wise EF1 and population Pareto-optimal mass problem was located in the literature search.

Modeling choices made when packaging the task

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

Partial resolution

I do not settle whether the requested construction problem is polynomial-time solvable or NP-hard.

I establish a new hardness result for verification:

Checking population Pareto optimality of a supplied law is $\mathrm{coNP}$-complete, even when the law is feasible and support-wise EF1, there are only two types and three positive support entries, and $K=m-2$.

This concerns the exact population Pareto comparison in the question, including arbitrary real reassignment masses. It does not imply hardness of finding a valid law. Indeed, every society used in the reduction below has an easily constructed EF1 and Pareto-optimal law.

I also give self-contained proofs of the small-support theorem, the $\Sigma_2^p$ upper bound for existence, and a finite exact construction algorithm.

1. Pareto optimality depends only on positive support

Let a feasible law have positive support
$$ S=\{(\theta_i,b_i):1\leq i\leq s\}, $$
with masses $y_i>0$. For each source $i$, define
$$ C_i=\{c\in B_K:u_{\theta_i}(c)\geq u_{\theta_i}(b_i)\}. $$
For $c\in C_i$, let
$$ d_{i,c}=c-b_i, \qquad a_{i,c}=\mathbf 1_{\{u_{\theta_i}(c)>u_{\theta_i}(b_i)\}}. $$

Consider the finite linear program
$$ \max \sum_{i,c\in C_i}a_{i,c}\lambda_{i,c} $$
subject to
$$ \lambda_{i,c}\geq0, \qquad \sum_{i,c\in C_i}\lambda_{i,c}=1, \qquad \sum_{i,c\in C_i}d_{i,c}\lambda_{i,c}=0. $$
It is feasible because diagonal transitions $c=b_i$ are permitted.

Lemma 1. The supplied law is population Pareto optimal if and only if this linear program has optimum zero.

Proof. Suppose first that a Pareto-improving reassignment exists. Write its entries as $z_{i,c}$. The source-mass equations imply
$$ \sum_{i,c}z_{i,c}=\sum_i y_i=1. $$
Supply preservation implies
$$ \sum_{i,c}(c-b_i)z_{i,c}=0. $$
Every positive entry is weakly improving, and strictly improving entries have positive total mass. Thus $\lambda_{i,c}=z_{i,c}$ is feasible and has positive objective.

Conversely, suppose a feasible $\lambda$ has positive objective. Put
$$ o_i=\sum_c\lambda_{i,c}. $$
Choose $\delta>0$ sufficiently small that $\delta o_i\leq y_i$ for every $i$. Define
$$ z_{i,c} = \delta\lambda_{i,c} + (y_i-\delta o_i)\mathbf 1_{\{c=b_i\}}. $$
These entries are nonnegative and have source totals $y_i$. Their total supply change is
$$ \delta\sum_{i,c}(c-b_i)\lambda_{i,c}=0. $$
All positive transitions are weakly improving, and the strictly improving transitions have positive total mass. This is a Pareto improvement. $\square$

In particular, Pareto optimality depends only on the positive support, rather than on its positive masses. Deleting support entries preserves Pareto optimality whenever the remaining entries support a feasible law. Deleting entries also preserves support-wise EF1.

Short certificates of nonoptimality

The normalized transition polytope above is compact. Its objective therefore attains a maximum at a vertex.

At a vertex, the columns corresponding to positive variables are linearly independent. Otherwise, a nonzero dependence would give sufficiently small feasible perturbations in both directions, contradicting vertexhood. There are only $m+1$ equality rows, so a vertex has at most $m+1$ positive transitions.

The equality coefficients are integers of absolute value at most $K$, except for the normalization coefficients, which are $1$. Choosing independent rows and applying Cramer's rule gives rational coefficients of bit length
$$ O\!\left((m+1)\bigl(\log(K+1)+\log(m+2)\bigr)\right). $$
For example, the denominator bound follows from Hadamard's determinant bound on a square submatrix of order at most $m+1$.

Consequently, non-Pareto-optimality has a polynomial-size certificate consisting of at most $m+1$ transitions and their rational coefficients. One checks admissibility, weak utility improvement, normalization, zero supply change, and positive coefficient on strict transitions using exact rational arithmetic.

Thus checking Pareto optimality of an explicitly supplied law belongs to $\mathrm{coNP}$.

2. A hardness construction for verification

The starting hardness fact is NP-completeness of positive-integer SUBSET SUM: given positive integers $s_1,\ldots,s_r,S$, determine whether
$$ \sum_{i=1}^r s_i x_i=S, \qquad x_i\in\{0,1\}. $$
This is the standard exact-sum problem in [Karp's NP-completeness results](https://www.cs.umd.edu/~gasarch/BLOGPAPERS/Karp.pdf).

We first encode it as an integer-sum equation whose nonnegative integer solutions automatically have bounded multiplicities.

2.1 An encoding that prevents repeated choices

Let $s_{\max}=\max_i s_i$ and choose the integer
$$ B=2+r+r s_{\max}+S. $$
Then
$$ B>r+1,\qquad B>r s_{\max},\qquad B>S. $$
Put $J=B^{r+1}$. For each $i$, introduce two denominations
$$ a_{i,0}=J+B^i, \qquad a_{i,1}=J+B^i+s_i. $$
The target is
$$ T=rJ+\sum_{i=1}^r B^i+S. $$

Lemma 2. Every nonnegative integer solution of
$$ \sum_{i=1}^r \bigl(a_{i,0}q_{i,0}+a_{i,1}q_{i,1}\bigr)=T $$
satisfies
$$ q_{i,0}+q_{i,1}=1 \quad\text{for every }i, \qquad \sum_i s_iq_{i,1}=S. $$
Conversely, every SUBSET SUM solution gives such an integer solution.

Proof. Let
$$ \ell_{\max}=B^r+s_{\max}, \qquad U=\sum_{i=1}^r B^i+S. $$
The choice of $B$ gives
$$ r\ell_{\max} < rB^r+B \leq (r+1)B^r < B^{r+1}=J, $$
and likewise
$$ U<rB^r+B\leq(r+1)B^r<J. $$

Every denomination lies between $J$ and $J+\ell_{\max}$. If at most $r-1$ coins were used, their sum would be less than $rJ$. If at least $r+1$ coins were used, their sum would exceed
$$ rJ+U=T. $$
Hence exactly $r$ coins are used.

Subtracting their common contribution $rJ$ leaves an equality of lower parts. The coefficient of every positional digit $B^i$ is at most $r<B$, while the sum in the units position is at most $r s_{\max}<B$. Thus no carries occur. Uniqueness of base-$B$ representation forces every positional coefficient to equal $1$, and the units sum to equal $S$. These are precisely the asserted equations.

The converse follows by choosing denomination $a_{i,1}$ when $x_i=1$ and $a_{i,0}$ when $x_i=0$. $\square$

List the resulting $n=2r$ denominations as $a_1,\ldots,a_n$. We have proved that
$$ \sum_{i=1}^n a_iq_i=T,\qquad q_i\in\mathbb Z_{\geq0}, $$
is solvable exactly when the original SUBSET SUM instance is solvable. Moreover, every solution has $q_i\in\{0,1\}$ and uses exactly $r$ coins.

All these integers have polynomial binary encoding length: their bit lengths are $O(r\log B)$.

2.2 The society and supplied law

Introduce $n+5$ classes:
$$ v,h,d,c,f,g_1,\ldots,g_n. $$
There are two types, $\alpha$ and $\beta$, with
$$ \mu_\alpha=\mu_\beta=\frac12, $$
and masks
$$ A_\alpha=\{v,h,d,f,g_1,\ldots,g_n\}, $$
$$ A_\beta=\{v,h,d,c,g_1,\ldots,g_n\}. $$
Thus $\alpha$ excludes only $c$, and $\beta$ excludes only $f$. Every class belongs to a mask.

Set
$$ K=n+3,\qquad D=K-2,\qquad M=4K,\qquad H=MT-D. $$
Because $T\geq1$ and $D<K$, we have
$$ H>\frac{MT}{2}>0. $$
Define
$$ P_{\max}=\max\{H,D,1,Ma_1,\ldots,Ma_n\}, \qquad V=KP_{\max}+1, $$
and choose the positive dyadic rational
$$ \varepsilon=2^{-\lceil\log_2(K+1)\rceil}. $$
In particular,
$$ K\varepsilon<1. $$

The inherent values are:

| Class | Inherent value |
|---|---:|
| $v$ | $V$ |
| $h$ | $H$ |
| $d$ | $1$ |
| $c$ | $D$ |
| $f$ | $\varepsilon$ |
| $g_i$ | $Ma_i$ |

For the proof, introduce an auxiliary integer-valued linear function
$$ p(b)=Vb_v+Hb_h+b_d+Db_c+\sum_i Ma_i b_{g_i}. $$
The bonus class $f$ has coefficient zero in this function. The utilities satisfy
$$ u_\alpha(b)=p(b)-Db_c+\varepsilon b_f, \qquad u_\beta(b)=p(b). $$

The supplied law has three positive entries:
$$ b^\alpha=e_v+e_h+D e_d, \qquad y_{\alpha,b^\alpha}=\frac12, $$
$$ b^I=e_v+\sum_i e_{g_i}, \qquad y_{\beta,b^I}=\frac14, $$
$$ b^C=e_v+e_c+e_f, \qquad y_{\beta,b^C}=\frac14. $$
Their sizes are $K$, $K-2$, and $3$, respectively.

Define the supplies from this law:
$$ \rho_v=1,\quad \rho_h=\frac12,\quad \rho_d=\frac D2,\quad \rho_c=\rho_f=\frac14,\quad \rho_{g_i}=\frac14. $$
They are positive dyadic rationals, and the law is feasible by construction.

Here
$$ m=n+5,\qquad \tau=2,\qquad K=m-2,\qquad t\leq m. $$
The construction, including the supplied law, has polynomial binary encoding length and is computable in polynomial time.

2.3 The supplied law is support-wise EF1

Every support bundle contains exactly one unit of $v$, which both types like. Consequently, every recipient has utility at least $V$.

After removing that unit from any support bundle, either type's evaluation is at most
$$ KP_{\max}+K\varepsilon < KP_{\max}+1 = V. $$
Thus, for every ordered pair of support entries, removing the common class $v$ from the compared bundle eliminates envy. The supplied law is support-wise EF1.

2.4 A Pareto improvement forces an exact integer sum

Suppose a Pareto-improving reassignment exists.

For a transition from the $\alpha$ source, weak improvement implies
$$ p(c)-Dc_c+\varepsilon c_f \geq V+MT. $$
Since $c_f\leq K$ and $K\varepsilon<1$, this gives
$$ p(c)>V+MT-1. $$
The function $p$ is integer-valued on bundles, so
$$ p(c)\geq V+MT=p(b^\alpha). $$

For either $\beta$ source, weak improvement directly implies
$$ p(c)\geq p(b). $$
Supply preservation gives
$$ \sum_{\theta,b,c}z_{\theta,b,c}\bigl(p(c)-p(b)\bigr)=0. $$
Every summand with positive mass has a nonnegative price change. Therefore every positive transition preserves $p$ exactly.

A $\beta$ transition consequently preserves utility exactly. Hence some positive $\alpha$ transition must be strict. For its destination $c$,
$$ p(c)=V+MT, \qquad -Dc_c+\varepsilon c_f>0. $$
Because $\varepsilon c_f<1\leq D$, these conditions force
$$ c_c=0,\qquad c_f\geq1. $$

We now classify such a destination.

First,
$$ MT=H+D\leq2P_{\max}<V. $$
A bundle without $v$ has price at most $KP_{\max}<V$, while a bundle containing at least two units of $v$ has price at least $2V>V+MT$. Thus
$$ c_v=1. $$
Its remaining price must equal $MT$.

Since $2H>MT$, it contains at most one unit of $h$. If $c_h=1$, the remaining price is $D$. Every ordinary class costs at least $M>D$, and $c_c=0$, so this remaining price requires exactly $D$ filler units. Together with $v$, $h$, and at least one bonus unit, that would give size at least
$$ 1+1+D+1=K+1, $$
which violates the cap. Therefore $c_h=0$.

The price equation is now
$$ M\sum_i a_i c_{g_i}+c_d=MT. $$
Because $0\leq c_d\leq K<M$, reducing modulo $M$ forces $c_d=0$. Hence
$$ \sum_i a_i c_{g_i}=T. $$
Lemma 2 turns this into a solution of the original SUBSET SUM instance.

This necessity argument used only nonnegativity and supply conservation of the real reassignment masses. Fractional population splitting therefore cannot circumvent the integer equation.

2.5 An exact integer sum gives a Pareto improvement

Conversely, suppose
$$ \sum_i a_iq_i=T $$
has a solution. Lemma 2 guarantees $q_i\in\{0,1\}$.

Use these destinations:
$$ c^\alpha=e_v+\sum_iq_i e_{g_i}+e_f, $$
$$ c^I=e_v+\sum_i(1-q_i)e_{g_i}+e_h+e_c, $$
$$ c^C=e_v+D e_d. $$
They respect the cap because
$$ |c^\alpha|=2+\sum_iq_i\leq n+2<K, $$
$$ |c^I|=3+n-\sum_iq_i\leq n+3=K, \qquad |c^C|=D+1=K-1. $$

Type $\alpha$ strictly gains:
$$ u_\alpha(c^\alpha)=V+MT+\varepsilon > V+MT=u_\alpha(b^\alpha). $$
The two $\beta$ sources preserve utility:
$$ u_\beta(c^I) = V+M\sum_i a_i-MT+H+D = u_\beta(b^I), $$
$$ u_\beta(c^C)=V+D=u_\beta(b^C). $$
Finally,
$$ b^\alpha+b^I+b^C=c^\alpha+c^I+c^C. $$
Reassigning mass $1/4$ from each of the three sources to its corresponding destination therefore preserves every supply. Leave the remaining mass $1/4$ at $b^\alpha$.

This is a Pareto improvement.

Combining both directions, the supplied law is non-Pareto-optimal exactly when the original SUBSET SUM instance is solvable. Nonoptimality is therefore NP-hard, even under all the stated restrictions. Section 1 proves its membership in NP.

Theorem 3. Checking population Pareto optimality of a supplied feasible, support-wise EF1 law is $\mathrm{coNP}$-complete, even with $\tau=2$, three positive support entries, and $K=m-2$.

3. Why this does not prove hardness of the requested construction

Every society in the preceding reduction has a simple valid law, independently of the SUBSET SUM answer.

Starting from the supplied law, exchange one filler unit for the bonus unit on equal masses $1/4$:
$$ b^{\alpha\prime}=b^\alpha-e_d+e_f, \qquad b^{C\prime}=b^C-e_f+e_d. $$
The new law gives mass $1/4$ to each of
$$ (\alpha,b^\alpha),\quad (\alpha,b^{\alpha\prime}),\quad (\beta,b^I),\quad (\beta,b^{C\prime}). $$
All bundles respect the cap, and the exchange preserves supplies.

Every bundle still contains exactly one unit of $v$. The argument in Section 2.3 therefore proves support-wise EF1.

For any feasible law $y$, its aggregate utility is
$$ \sum_{\theta,b}y_{\theta,b}u_\theta(b) = \sum_g p(e_g)\rho_g - D\sum_b y_{\alpha,b}b_c + \varepsilon\sum_b y_{\alpha,b}b_f. $$
Consequently,
$$ \sum_{\theta,b}y_{\theta,b}u_\theta(b) \leq \sum_g p(e_g)\rho_g+\varepsilon\rho_f. $$
The modified law attains this upper bound: all bonus supply goes to $\alpha$, and no currency supply goes to $\alpha$.

It therefore maximizes aggregate utility over all feasible real laws. A population Pareto improvement would strictly increase aggregate utility, contradicting this maximality. The modified law is population Pareto optimal.

Thus the reduction establishes a verification barrier, while its underlying construction instances are all yes-instances. It cannot serve as a hardness reduction for existence.

4. Small valid laws and polynomial encoding length

Theorem 4. Every yes-instance has a valid law with at most $m+\tau$ positive entries and polynomial binary encoding length.

Proof. Start with a valid law and restrict attention to its positive support $S$. The mass and supply equations have the form
$$ Ay=h,\qquad y\geq0, $$
with $m+\tau$ rows. This polytope is nonempty and bounded because each variable is bounded by its type's mass.

Choose a vertex. Its positive columns must be linearly independent: a dependence would permit sufficiently small feasible perturbations in both directions. Hence at most
$$ \operatorname{rank}(A)\leq m+\tau $$
entries are positive.

Deleting the other entries preserves both EF1 and Pareto optimality by Section 1.

Let $d=m+\tau$. The matrix coefficients are integers bounded by $K$. Clearing a common denominator of the input vector $h$ costs $O(L)$ bits. Selecting independent rows and applying Cramer's rule and Hadamard's determinant bound shows that each positive mass has bit length
$$ O\!\left( L+d\bigl(\log(K+1)+\log(d+1)\bigr) \right). $$
Each bundle requires $O(m\log(K+1))$ bits. The complete law therefore has polynomial encoding length. $\square$

Explicit vertex selection

The minor vertex-selection issue identified in the notes has a direct repair. For a nonempty bounded rational polytope with an explicit inequality description, successively minimize its first coordinate, then its second coordinate over the preceding optimal face, and so on. After all coordinates have been fixed, the remaining face is a singleton.

That singleton is a vertex: if it were the midpoint of distinct feasible points, optimality of the first coordinate would force both points into the first optimal face; repeating coordinate by coordinate would force both to equal the singleton.

This uses one exact rational LP per coordinate. Each intermediate set is a face of the original polytope, so its coordinate optimum occurs at an original vertex. Standard determinant bounds therefore keep the added optimal-value equalities at polynomial bit length. The same procedure applies to the minimal face containing a specified point, obtained by imposing its tight inequalities as equalities.

5. A finite exact algorithm and an existence upper bound

Write
$$ R=\sum_g\rho_g. $$
Every feasible law satisfies
$$ R=\sum_{\theta,b}|b|y_{\theta,b}\leq K. $$
Conversely, when $R\leq K$, feasibility alone is witnessed by
$$ y_{\theta,Ke_g}=\mu_\theta\frac{\rho_g}{K}, \qquad y_{\theta,0}=\mu_\theta\left(1-\frac RK\right). $$
These masses have the prescribed type totals and supplies. Thus $R>K$ is an immediate obstruction.

For the simultaneous requirements, let
$$ M_K=|B_K|=\binom{K+m}{m}, \qquad N=\tau M_K, \qquad d=m+\tau. $$

An exact algorithm is:

If no candidate succeeds, report that no valid law exists.

For step 2, EF1 is equivalent to
$$ u_\theta(b)\geq u_\theta(c)- \max\bigl(\{w_g:g\in A_\theta,\ c_g>0\}\cup\{0\}\bigr). $$
Thus each comparison is computable by exact rational arithmetic.

The transition LP has at most $dM_K$ variables. Both LPs have rational coefficients of polynomial bit length in $m,\tau,L,\log(K+1)$. Standard polynomial-time rational linear programming therefore gives the running-time bound
$$ (d+1)(\tau M_K)^d \operatorname{poly}\!\left( dM_K,m,\tau,L,\log(K+1) \right). $$
There is no additional dependence on $t$ beyond the values already encoded in $L$.

Correctness follows from Theorem 4: every yes-instance has a support among those enumerated. Conversely, every output is feasible and has both properties. Any zero entries produced by the feasibility LP can be deleted without losing either property.

Finally, existence belongs to $\Sigma_2^p$. Existentially guess the polynomial-size law guaranteed by Theorem 4, check feasibility and EF1, and universally exclude the polynomial-size nonoptimality certificates from Section 1.

6. Remaining question

The new result proves that a general algorithm cannot rely on polynomial-time Pareto verification of arbitrary candidate laws unless $\mathrm P=\mathrm{NP}$. It leaves open whether a construction algorithm can produce valid laws through a different method.

The target classification—polynomial-time construction in $m,\tau,L$ versus NP-hardness—remains unresolved.

⟨structured verdict parsed — rendered above⟩

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

The output is correct as a partial resolution, but it does not settle the requested polynomial-time versus NP-hardness classification. Its verification hardness result, small-support theorem, existence upper bound, and finite construction algorithm withstand scrutiny. The unresolved construction complexity is the sole major issue relative to USER_TASK.

1. Support dependence and nonoptimality certificates

Lemma 1 correctly captures the population Pareto comparison, including arbitrary real reassignment masses.

In the forward direction, the source equations give total reassignment mass $1$, and supply preservation gives zero aggregate displacement. Thus the improving reassignment satisfies the normalized transition LP and has positive objective.

In the converse direction, every source mass $y_i$ is positive and there are finitely many sources. Consequently, the stated choice of $\delta>0$ satisfying $\delta o_i\leq y_i$ exists. Adding the remaining source mass to the diagonal transition gives exactly the required source totals. Zero aggregate displacement preserves supplies, and the positive LP objective produces positive strictly improving mass. No rationality assumption on the competing reassignment is introduced.

The conclusion that Pareto optimality depends only on positive support follows. The deletion claim is also correctly qualified: the remaining support must admit a feasible law. EF1 survives deletion because its comparisons range only over retained entries.

The certificate argument is sound:

Admissibility, utility comparisons, normalization, displacement cancellation, and strict improvement can all be checked exactly in polynomial time in the supplied input and certificate lengths. Thus the claimed membership of Pareto verification in $\mathrm{coNP}$ is established.

2. Integer encoding in Lemma 2

The starting positive-integer SUBSET SUM problem is an appropriate NP-complete source; the cited [Karp paper](https://www.cs.umd.edu/~gasarch/BLOGPAPERS/Karp.pdf) is the standard reference for the exact-sum problem, historically named KNAPSACK there.

For the conventional nonempty source list, $r\geq1$, all displayed inequalities in the encoding are valid. In particular, the choice of $B$ ensures
$$ r\ell_{\max}<J,\qquad U<J. $$

The coin-count argument correctly excludes both alternatives:

Exactly $r$ coins therefore occur. After subtracting $rJ$, every positional coefficient is at most $r<B$, and the units contribution is at most $rs_{\max}<B$. The target units digit also satisfies $S<B$. Hence the no-carry argument is justified, and uniqueness of base-$B$ representation yields precisely the asserted equations.

The converse is immediate from the displayed denominations. The encoding length $O(r\log B)$ is correct. This lemma genuinely excludes repeated choices in every nonnegative integer solution.

3. Society construction, feasibility, and EF1

All constructed values and supplies are positive and have polynomial binary encoding length. Both masks satisfy the required coverage condition.

The bundle sizes are correctly computed:
$$ |b^\alpha|=D+2=K,\qquad |b^I|=n+1=K-2,\qquad |b^C|=3. $$

The supplies match the three listed source masses exactly. In particular, $\rho_v=1$, and every other class receives the stated positive supply.

The auxiliary function $p$ is integer-valued, and both utility identities agree with the masks:
$$ u_\alpha(b)=p(b)-Db_c+\varepsilon b_f,\qquad u_\beta(b)=p(b). $$

The EF1 argument is valid. Every source has a valued unit of $v$, so its recipient obtains utility at least $V$. Removing that unit from any compared support bundle leaves utility strictly below $V$, by the displayed bound and $K\varepsilon<1$. This checks every ordered pair of support entries.

The restrictions $\tau=2$, three positive support entries, and $K=m-2$ are all satisfied. The construction permits $t$ to grow; it establishes no fixed-$t$ hardness claim.

4. Necessity of an exact sum for a Pareto improvement

The crucial integer-rounding step is correct. For an $\alpha$ transition, weak improvement and $\varepsilon c_f<1$ imply
$$ p(c)>V+MT-1. $$
Since $p(c)$ is integral, its price cannot decrease. For $\beta$, nondecreasing price follows directly from its utility definition.

Supply preservation makes the total price change zero. Since every positive transition has nonnegative price change, every such transition must preserve price individually. This reasoning remains valid for real reassignment masses.

It follows correctly that $\beta$ cannot strictly improve. A Pareto improvement therefore contains a strict $\alpha$ transition. For that transition, price preservation and the utility identity force
$$ c_c=0,\qquad c_f\geq1. $$

The destination classification is sound:

The resulting equation is exactly the integer equation covered by Lemma 2. No fractional splitting loophole remains in this argument.

5. Sufficiency and verification completeness

The proposed destinations are nonnegative integer bundles because Lemma 2 guarantees $q_i\in\{0,1\}$. All three cap bounds are valid.

The utility calculations also check:

The bundle identity preserves every class supply when mass $1/4$ is moved from each source. Leaving the remaining $\alpha$ mass at its original bundle satisfies all source equations.

Thus the supplied law is nonoptimal exactly when the SUBSET SUM instance is solvable. Together with the certificate result, this establishes the claimed $\mathrm{coNP}$-completeness of verification under the stated restrictions.

This is a verification result, not a hardness reduction for construction or existence.

6. Explicit valid laws for the reduction societies

The modified law is feasible. The two bundle changes cancel class by class, and their sizes respect the cap. Each retained bundle contains one unit of $v$, so the earlier EF1 bound applies.

The aggregate-utility identity is correct. Nonnegativity and supply preservation imply the stated upper bound, and the modified law attains it by assigning all $f$ supply to $\alpha$ and no $c$ supply to $\alpha$.

The bound applies to feasible real laws as well as rational laws. A population Pareto improvement would strictly increase aggregate utility, contradicting maximality. The modified law is therefore population Pareto optimal.

This section rigorously establishes why the verification reduction does not resolve the requested hardness question: all its society instances admit explicit valid laws.

7. Small support and encoding length

Theorem 4 is correct. Restricting to the original positive support gives a nonempty bounded rational polytope. At a vertex, positive columns are independent, so there are at most $m+\tau$ positive entries.

Both required properties survive the support deletion, using the already proved support dependence and the hereditary nature of EF1.

The determinant-based mass bit bound is valid: clearing the input denominators costs $O(L)$ bits, while the relevant matrix coefficients are bounded by $K$. The bundle encodings also have the stated polynomial length.

The explicit vertex-selection paragraph is sound. Successive coordinate minimizations produce nonempty faces of the original bounded polytope and eventually a singleton vertex. Its determinant justification for polynomial bit lengths is appropriate.

8. Finite algorithm and existence upper bound

The feasibility obstruction $R>K$ follows directly from the bundle cap. The converse feasibility witness has nonnegative masses when $R\leq K$, correct type totals, and correct supplies.

The support enumeration is complete by Theorem 4. Its EF1 formula correctly covers empty bundles and bundles containing no class valued by the evaluating type.

The transition LP and feasibility LP have explicit rational descriptions with the stated size bounds. Polynomial-time exact rational linear programming applies to these descriptions. Infeasibility can be detected, and feasible masses of polynomial encoding length can be returned.

The number of enumerated supports is bounded by the displayed factor, so the stated running-time bound is valid. It is a finite bound, not polynomial in the binary input length in general. The assertion about $t$ correctly describes this algorithm only.

Deleting zero masses returned by the feasibility LP preserves both properties. Consequently, both successful output and exhaustive rejection are justified.

The $\Sigma_2^p$ existence upper bound also follows: guess the polynomial-size law from Theorem 4, check feasibility and EF1, and universally exclude the polynomial-size nonoptimality certificates from Section 1. This classifies the existence decision problem, not the construction problem as polynomial-time solvable.

Issue and minimum required follow-up

Major — requested complexity classification remains unresolved. Sections 3 and 6 explicitly acknowledge this limitation. Neither verification hardness nor the existence upper bound proves polynomial-time construction or NP-hardness of the task in USER_TASK.

No expositional clarification can remove this issue. Another round must supply a result that actually classifies the requested construction task. The valid intermediate results should be retained, and the distinction between verification and construction must remain explicit.

I found no additional mathematical errors or gaps in the established partial results.

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