Answer: Polynomial-time solvable, including with strictly dyadic output masses when the input masses and supplies are dyadic.
Theorem 3.3 — class: algorithmic
Given valuation types \(T\) with rational masses \(\mu\), item kinds \(O\) with rational per-capita supplies \(q\), and rational additive values \(v_t(o)\), output a finite-support distribution \(x\) over integer bundles \(k\) such that type masses and item supplies are respected, every supported type-bundle pair satisfies PROP1 relative to \(P_t = \sum_o q_o v_t(o)\), and \(x\) is Pareto optimal under type-wise couplings of old and new bundles. Determine whether this can be done in time polynomial in \(|T|\), \(|O|\), and the input bit-length.
A society is given by its support: a list of \(\tau=|T|\) valuation types with positive binary-rational masses \(\mu_t\), normalized by \(\sum_t\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types. There are \(m=|O|\) item kinds with positive binary-rational per-capita supplies \(q_o\); zero-supply kinds are omitted. Values \(v_t(o)\in\mathbb Q\) may be positive, negative, or zero, independently across types. Let \(L\) be the total input bit length.
A bundle is \(k\in\mathbb Z_{\ge0}^{m}\), with utility \(u_t(k)=\sum_o k_o v_t(o)\); empty bundles are allowed, and there is no individual bundle-size bound. A feasible allocation is a finite-support mass distribution \(x_{t,k}\ge0\) satisfying \(\sum_kx_{t,k}=\mu_t\) and \(\sum_{t,k}x_{t,k}k_o=q_o\) for every kind.
Set \(P_t=\sum_o q_o v_t(o)\). A supported pair \((t,k)\) satisfies PROP1 if \(u_t(k)\ge P_t\), or \(u_t(k)+v_t(o)\ge P_t\) for some kind with \(v_t(o)>0\), or \(u_t(k)-v_t(o)\ge P_t\) for some kind with \(k_o\ge1\) and \(v_t(o)<0\). Adding or removing one item is hypothetical; adding means obtaining one copy from elsewhere in the atomless society.
An allocation \(y\) Pareto improves \(x\) if both are feasible and, for each type, there is a nonnegative coupling \(\gamma_t(k,\ell)\) with marginals \(x_{t,k}\) and \(y_{t,\ell}\), supported only where \(u_t(\ell)\ge u_t(k)\), with strict inequality on positive total coupling mass. Competitors may have real masses and need not satisfy PROP1. Pareto optimality means no such finite-support competitor exists.
Is computing a feasible finite-support allocation with binary-rational masses, satisfying PROP1 at every supported pair and Pareto optimality under these couplings, possible in time polynomial in \(m,\tau,L\), or is this computation NP-hard?
For finitely many agents with additive mixed-sign utilities, a strongly polynomial-time algorithm computes a PROP1 and Pareto-optimal allocation, even with asymmetric entitlements ([Aziz, Moulin, and Sandomirskiy, 2020](https://eprints.gla.ac.uk/221523/1/221523.pdf)). No result settling the support-encoded atomless problem defined above was identified in the literature search.
The computation is possible in time polynomial in \(m,\tau,L\). This holds even if “binary-rational” means strictly dyadic: when the input masses and supplies have power-of-two denominators, the output masses can also have power-of-two denominators.
For arbitrary binary-encoded rational masses, the construction uses at most \(2\tau(m+1)\) supported pairs. The dyadic refinement uses \(O(\tau(m+1)^2)\) supported pairs. All bundle multiplicities and masses have polynomial encoding length.
The proof has two ingredients: an efficient allocation of aggregate quantities to types, and a mean-preserving rounding lemma for individual bundles.
For a nonnegative matrix \(A=(A_{to})\), define the aggregate utility of type \(t\) by
\( \displaystyle U_t(A)=\sum_o v_t(o)A_{to}. \)
Here \(A_{to}\) is the total per-capita quantity of kind \(o\) allocated to type \(t\), rather than the quantity received by one individual.
Compute an optimal solution \(A^*\) of the rational linear program
\( \displaystyle \begin{aligned} \text{maximize}\quad &\sum_t U_t(A),\\ \text{subject to}\quad &\sum_t A_{to}=q_o &&\text{for every }o,\\ &U_t(A)\ge \mu_tP_t &&\text{for every }t,\\ &A_{to}\ge 0 &&\text{for every }t,o. \end{aligned} \)
This program is feasible: the matrix \(A_{to}=\mu_tq_o\) satisfies \(U_t(A)=\mu_tP_t\). Its feasible region is bounded because \(0\le A_{to}\le q_o\).
We use the standard exact rational linear-programming theorem: a nonempty bounded rational linear program can be optimized in polynomial bit complexity, with a rational optimal solution of polynomial encoding length. The hypotheses hold here, and the program has polynomial dimension and encoding length. For background on exact polynomial-time rational optimization, see [Gleixner and Steffy, Section 1.3](https://arxiv.org/pdf/1912.12820).
Define
\( \displaystyle E=\{(t,o):A^*_{to}>0\}. \)
The following property will also allow us to adjust masses later.
Lemma 1. Every nonnegative aggregate allocation \(B\) satisfying the supply equalities and \(B_{to}=0\) outside \(E\) is Pareto optimal for aggregate type utilities.
Proof. Suppose another aggregate allocation \(C\) satisfies the supply equalities and
\( \displaystyle U_t(C)\ge U_t(B)\quad\text{for every }t, \)
with strict inequality for at least one type. Put \(D=C-B\).
Outside \(E\), we have \(B_{to}=A^*_{to}=0\), so \(D_{to}=C_{to}\ge0\). Inside \(E\), all entries of \(A^*\) are positive. Consequently, for sufficiently small \(\varepsilon>0\),
\( \displaystyle A^*+\varepsilon D\ge0. \)
The supply equalities remain satisfied because every column of \(D\) sums to zero. Moreover,
\( \displaystyle U_t(A^*+\varepsilon D) =U_t(A^*)+\varepsilon\bigl(U_t(C)-U_t(B)\bigr) \ge U_t(A^*)\ge\mu_tP_t. \)
Thus \(A^*+\varepsilon D\) is feasible for the linear program and has strictly larger objective value, contradicting optimality. \(\square\)
Consequence for the required Pareto notion. Any feasible finite-support allocation that assigns type \(t\) only kinds \(o\) with \((t,o)\in E\) is Pareto optimal under the specified couplings.
Indeed, for a purported improvement \(y\) of \(x\), let their aggregate matrices be \(C\) and \(B\). The coupling marginals give
\( \displaystyle U_t(C)-U_t(B) =\sum_{k,\ell}\gamma_t(k,\ell) \bigl(u_t(\ell)-u_t(k)\bigr)\ge0. \)
Strict improvement on positive coupling mass makes this expression positive for at least one type. This contradicts Lemma 1. The argument allows real competitor masses and imposes no fairness requirement on competitors.
We prove a rounding lemma that permits mixed signs.
Lemma 2. Let \(w\in\mathbb Q^d\), let \(p\in\mathbb Q_{\ge0}^d\), and let integer vectors \(a,c\) satisfy \(0\le a\le p\le c\). Set \(b=w\cdot p\).
In polynomial time, one can construct a rational probability distribution on at most \(2(d+1)\) integer vectors \(k\in[a,c]\) whose mean is \(p\), such that every supported \(k\) satisfies at least one of:
All output numbers have polynomial encoding length.
Consider the bounded rational polytope
\( \displaystyle Q=\{r\in[a,c]:w\cdot r=b\}. \)
Every vertex of \(Q\) has at most one noninteger coordinate. To see this, suppose two coordinates \(i,j\) are noninteger. Both are strictly between their integer bounds. There is a nonzero direction supported on these coordinates and orthogonal to \(w\), along which a sufficiently small perturbation in either direction stays in \(Q\). This contradicts extremality. A noninteger coordinate with coefficient zero likewise admits a two-sided perturbation.
Decompose \(p\) into at most \(d+1\) vertices of \(Q\); a polynomial-time construction is given below.
An integral vertex already gives an integer bundle of utility \(b\). Otherwise, its unique noninteger coordinate has the form
\( \displaystyle r_i=h+\theta,\qquad h\in\mathbb Z_{\ge0},\quad 0<\theta<1. \)
Replace this vertex by its two integer roundings \(k^-,k^+\), with probabilities \(1-\theta,\theta\). Their mean is \(r\).
If \(w_i>0\), only rounding down can decrease utility, and
\( \displaystyle w\cdot k^-+w_i=b+(1-\theta)w_i\ge b. \)
If \(w_i<0\), only rounding up can decrease utility. Since \(k_i^+=h+1\ge1\),
\( \displaystyle w\cdot k^+-w_i=b-\theta w_i\ge b. \)
Thus both roundings satisfy the claimed condition, and combining the distributions preserves the mean \(p\).
Here is an explicit decomposition procedure, including its bit-complexity justification.
At a current point \(p'\in Q\), restrict \(Q\) to the face obtained by fixing every coordinate of \(p'\) that is at a box endpoint. Find a vertex \(r\) of this face by lexicographically optimizing its coordinates, using at most \(d\) exact linear programs.
If \(r=p'\), stop. Otherwise, extend the ray from \(r\) through \(p'\) until it first reaches a new box boundary. Write its endpoint as
\( \displaystyle p''=r+s(p'-r),\qquad s>1. \)
Then
\( \displaystyle p'=\left(1-\frac1s\right)r+\frac1s\,p''. \)
At least one additional coordinate of \(p''\) is at a box endpoint, and previously fixed coordinates remain fixed. Therefore the procedure terminates after at most \(d\) such extensions and produces at most \(d+1\) vertices.
To bound intermediate bit lengths, clear denominators in the equality defining \(Q\), obtaining
\( \displaystyle \sum_i a_i' r_i=b' \)
with integer coefficients. Every vertex coordinate has denominator dividing
\( \displaystyle H=\prod_{i:a_i'\ne0}|a_i'|, \)
where an empty product is \(1\). This follows because all but at most one coordinate are at integer box endpoints, and the remaining coordinate is determined by the equality.
Write \(p'_j=N_j/D\) and \(r_j=R_j/H\), using common denominators. Suppose the ray extension reaches endpoint \(h\) in coordinate \(i\). Direct substitution gives
\( \displaystyle p''_j= \frac{R_jN_i+(hH-R_i)N_j-hDR_j} {HN_i-DR_i}. \)
Let \(W=\max\{1,\max_i(c_i-a_i)\}\). The absolute value of the displayed denominator is at most \(HDW\). Thus each extension increases the common denominator’s bit length by at most \(\log H+\log W+O(1)\). There are at most \(d\) extensions. Coordinates stay in the box, so their numerators also have polynomial bit length. The convex coefficients are products of at most \(d\) polynomial-length rationals.
This proves both polynomial running time and polynomial output encoding length. \(\square\)
For each type define its mean bundle
\( \displaystyle z_{to}=\frac{A^*_{to}}{\mu_t}. \)
The aggregate proportionality constraints imply
\( \displaystyle u_t(z_t)=\frac{U_t(A^*)}{\mu_t}\ge P_t. \)
Apply Lemma 2 with \(w_o=v_t(o)\), \(p=z_t\), and the coordinate bounds \(\lfloor z_t\rfloor,\lceil z_t\rceil\). Let \(\pi_{t,k}\) be the resulting probability distribution, and set
\( \displaystyle x_{t,k}=\mu_t\pi_{t,k}. \)
The type masses are correct:
\( \displaystyle \sum_kx_{t,k}=\mu_t. \)
The mean-preserving property gives exact supply conservation:
\( \displaystyle \sum_{t,k}x_{t,k}k_o =\sum_t\mu_tz_{to} =\sum_tA^*_{to} =q_o. \)
Every supported bundle satisfies PROP1: Lemma 2 supplies the required correction relative to \(u_t(z_t)\), which is at least \(P_t\). Its negative-item correction explicitly requires a present copy.
If \(A^*_{to}=0\), then \(z_{to}=0\), so both rounding bounds for that coordinate are zero. Thus every supported bundle uses only kinds permitted by \(E\). Lemma 1 and the coupling argument prove Pareto optimality.
This already resolves the question under the arbitrary binary-encoded rational interpretation.
For completeness, we now require output masses to be dyadic, assuming that all \(\mu_t,q_o\) are dyadic.
The preceding construction can produce nondyadic probabilities. We therefore construct a slightly larger set of PROP1 bundles, obtain positive rational masses on every bundle in that set, and then correct a sufficiently fine dyadic rounding.
Fix a type and omit coordinates with \(z_{to}=0\). Let the remaining dimension be \(d\), write \(z\) for the restricted mean, \(w\) for its valuation vector, and set \(b=w\cdot z\ge P_t\).
If \(d=0\), use only the empty bundle.
Otherwise, choose a nonnegative integer box \(\mathcal B\) in which \(z\) is strictly interior. For example, coordinate \(i\) can have bounds
\( \displaystyle \max\{0,\lfloor z_i\rfloor-1\}, \qquad \lceil z_i\rceil+1. \)
We construct a polynomial-size set \(S\) of PROP1 bundles such that \(z\) lies in the interior of \(\operatorname{conv}S\) in these \(d\) coordinates.
If \(w=0\), choose a sufficiently small positive rational \(\varepsilon\) and apply Lemma 2 to every point \(z\pm\varepsilon e_i\) in \(\mathcal B\). Let \(S\) contain all resulting bundles. Their utilities are zero, and \(0=b\ge P_t\). Their convex hull contains a neighborhood of \(z\).
Suppose \(w\ne0\). Choose a rational basis \(g_1,\ldots,g_{d-1}\) of
\( \displaystyle \{g:w\cdot g=0\}. \)
For instance, after choosing \(j\) with \(w_j\ne0\), use \(e_i-(w_i/w_j)e_j\) for \(i\ne j\). Choose a positive rational \(\varepsilon\) small enough that every \(z\pm\varepsilon g_i\) lies in \(\mathcal B\). Such a choice has polynomial encoding length, by using the minimum distance to the box boundary and the maximum basis-coordinate magnitude.
Apply Lemma 2 to \(z\) and to these points, always using \(\mathcal B\). Call the union of resulting bundles \(S_0\). Every bundle is PROP1 relative to \(b\), and
\( \displaystyle \operatorname{conv}S_0 \)
contains a neighborhood of \(z\) within the hyperplane \(w\cdot r=b\).
Next find a vertex \(r\) of
\( \displaystyle \mathcal B\cap\{r:w\cdot r=b\} \)
that maximizes coordinate \(j\). Since \(z_j>0\), this vertex has \(r_j>0\).
If \(r\) has a noninteger coordinate, its two integer roundings have utilities strictly on opposite sides of \(b\), and Lemma 2 shows both are PROP1. Add them to \(S_0\).
If \(r\) is integral, add \(r-e_j\) and \(r+e_j\). The former is nonnegative because \(r_j\ge1\). Both are PROP1: a utility-decreasing change is undone by adding the removed positive item or removing the added negative item. Their utilities are strictly on opposite sides of \(b\).
Let the enlarged set be \(S_1\). We claim that \(z\) is interior to \(\operatorname{conv}S_1\). Otherwise, the supporting-hyperplane theorem gives a nonzero vector \(h\) such that
\( \displaystyle h\cdot(s-z)\le0\quad\text{for all }s\in S_1. \)
The points \(z\pm\varepsilon g_i\) belong to its convex hull, forcing \(h\cdot g_i=0\) for every \(i\). Hence \(h\) is a multiple of \(w\). The added points with utilities on opposite sides of \(b\) rule out every nonzero such multiple. This proves the claim.
Finally, select an integer bundle \(h_t\) from this construction with utility at least \(b\); one exists by taking a favorable rounding of a vertex. Add
\( \displaystyle h_t+e_o \)
for every retained kind \(o\). These bundles are PROP1: a positive-valued addition preserves utility at least \(b\), while a negative-valued addition can be removed to recover \(h_t\). Adding points preserves the interior property.
Denote the final set by \(S_t\), restoring zero coordinates. It has \(O((d+1)^2)\) bundles, all with polynomial encoding length, all PROP1, and all using only edges in \(E\).
Because \(z_t\) is interior to \(\operatorname{conv}S_t\), it has a convex representation assigning positive weight to every member of \(S_t\). Explicitly, let \(\bar s\) be the average of its members. For sufficiently small \(\alpha>0\),
\( \displaystyle z'=\frac{z_t-\alpha\bar s}{1-\alpha} \)
still belongs to \(\operatorname{conv}S_t\). A representation of \(z'\), mixed with weight \(\alpha\) on the uniform distribution over \(S_t\), gives the claimed positive representation.
We can therefore solve the rational linear program maximizing \(\eta\), subject to
\( \displaystyle \sum_{k\in S_t}x_{t,k}=\mu_t,\qquad \sum_{k\in S_t}x_{t,k}k_o=A^*_{to},\qquad x_{t,k}\ge\eta \)
for all types, bundles, and coordinates. Its optimum satisfies \(\eta>0\). It returns polynomial-length rational masses.
Let \(R\) be the total number of pairs in these sets, and let
\( \displaystyle K=\max\{1,\max_{t,k,o}k_o\}. \)
Choose a dyadic grid size \(\delta=2^{-B}\) satisfying
\( \displaystyle \delta\le\frac{\eta}{2(1+2mRK)}. \)
Choose \(B\) also large enough that all input masses and supplies lie on this grid. Both requirements need only polynomially many bits.
Round every mass downward to this grid, obtaining \(\widetilde x_{t,k}\). Each error is less than \(\delta\).
First correct type totals. For every type, add
\( \displaystyle r_t=\mu_t-\sum_{k\in S_t}\widetilde x_{t,k}\ge0 \)
to the mass of its designated bundle \(h_t\). For a type with no retained coordinates, designate the empty bundle. These corrections are dyadic and satisfy \(\sum_t r_t<R\delta\).
Let the remaining supply discrepancy be
\( \displaystyle s_o=q_o-\sum_{t,k}\widetilde x_{t,k}k_o, \)
where the sum now includes the type corrections. Its absolute value is at most \(2RK\delta\): rounding changes each supply by at most \(RK\delta\), and the type corrections change it by at most another \(RK\delta\).
For each kind \(o\), choose a type \(t(o)\) with \(A^*_{t(o),o}>0\); one exists because \(q_o>0\). Add \(s_o\) to the mass of
\( \displaystyle h_{t(o)}+e_o \)
and subtract \(s_o\) from the mass of \(h_{t(o)}\). This preserves every type total and changes only the supply of kind \(o\), by exactly \(s_o\).
All resulting masses are dyadic. The total possible decrease of any mass is at most
\( \displaystyle \delta+2mRK\delta\le\eta/2. \)
Thus every final mass remains positive. The final allocation exactly satisfies all type and supply equalities.
Every supported bundle still belongs to its fixed PROP1 set \(S_t\). It also uses only edges in \(E\), so Lemma 1 proves Pareto optimality even though the correction may change aggregate utilities.
The aggregate linear program has \(\tau m\) variables and polynomial encoding length. Lemma 2 uses polynomially many exact linear programs and polynomial-length rational arithmetic.
The rational construction has at most \(2\tau(m+1)\) supported pairs. The dyadic refinement applies the rounding lemma to \(O(m)\) points per type, producing \(O(\tau(m+1)^2)\) pairs. Its additional linear program and mass corrections are polynomial-time operations.
Large supplies require large binary-encoded multiplicities, not an enumeration of individual copies. Indeed, the constructed bundle coordinates are bounded by a constant plus \(\max_{t,o}q_o/\mu_t\), whose logarithm has polynomial size. The dyadic grid exponent also has polynomial size because \(\eta\) is a positive rational of polynomial encoding length.
If \(m=0\), assigning the empty bundle to each type is immediate. Otherwise, the constructions above provide the required feasible, finite-support, PROP1, Pareto-optimal allocation in polynomial time.
⟨structured verdict parsed — rendered above⟩
The argument is sound in substance and establishes polynomial-time solvability, including the strictly dyadic interpretation, subject to two minor clarifications. I found no false central step, major gap, or obstruction to the claimed construction.
The proof addresses the support-encoded problem directly. It permits mixed-sign and zero valuations, unbounded integer bundle multiplicities, real competitor masses, and the specified individual-level Pareto couplings.
The feasibility witness \(A_{to}=\mu_tq_o\) is correct: it satisfies the supply equalities and gives \(U_t(A)=\mu_tP_t\).
Nonnegativity and the supply equalities imply \(0\le A_{to}\le q_o\), so this feasible region is bounded. Computing \(P_t\), forming the constraints, and encoding their rational coefficients require polynomial bit length.
The exact rational LP theorem is applicable here. The cited [Gleixner–Steffy paper, Section 1.3](https://arxiv.org/pdf/1912.12820), does discuss exact polynomial-time algorithms for rational linear programming.
The perturbation argument is valid.
The contradiction therefore establishes the stated support property. In particular, \(B\) itself need not satisfy the aggregate proportionality constraints. This stronger conclusion is essential for the later dyadic correction.
No rationality assumption on \(B\), \(C\), or the perturbation parameter is needed for this optimality argument.
The displayed coupling identity is correct. Because both allocations have finite support, their marginal conditions restrict the relevant coupling to finitely many bundle pairs.
Every utility difference on its support is nonnegative. Strict improvement on positive coupling mass therefore produces a strictly positive aggregate utility difference for at least one type.
Thus aggregate Pareto optimality excludes every competitor allowed by the task, including competitors with real masses and no PROP1 requirement.
The two-sided perturbation argument correctly excludes two noninteger coordinates at a vertex. A noninteger coordinate with zero coefficient is also excluded.
The later denominator argument uses the stronger statement that at most one coordinate can be away from its box endpoints. This follows immediately from the same perturbation argument: the relevant condition is being strictly between the endpoints, regardless of integrality. This is a routine consequence, rather than a substantive gap.
Both critical calculations are correct:
\(w\cdot k^-+w_i=b+(1-\theta)w_i\)
when \(w_i>0\), and
\(w\cdot k^+-w_i=b-\theta w_i\)
when \(w_i<0\).
The other rounding in each case has utility at least \(b\). In the negative case, the unfavorable rounding has \(k_i^+=h+1\ge1\), so the removal operation is permitted by the task.
The probabilities \(1-\theta\) and \(\theta\) preserve the vertex mean. Integer box endpoints ensure both rounded vectors remain in the box.
The decomposition procedure is valid:
Consequently, at most \(d\) extensions and \(d+1\) vertices suffice.
The common vertex denominator \(H\) is valid, including the empty-product convention when all coefficients vanish. Its encoding length is polynomial after clearing denominators.
I rechecked the ray-extension formula; its numerator and denominator are correct. The denominator is nonzero because the selected coordinate changes along the ray. The bound
\(\lvert HN_i-DR_i\rvert\le HDW\)
follows from both coordinate values belonging to the same box interval.
The resulting denominator growth is additive in bit length over at most \(d\) extensions. Bounded coordinate magnitudes then control numerator lengths. The convex coefficients likewise retain polynomial encoding length.
Thus Lemma 2 supplies the claimed polynomial-time distribution on at most \(2(d+1)\) bundles.
All required properties follow from the written argument.
The supported-pair bound \(2\tau(m+1)\) is correct. Large bundle multiplicities are represented in binary; their numerical magnitude does not require enumerating copies.
This part settles the arbitrary binary-encoded rational interpretation.
The proposed box places every retained positive coordinate of \(z\) strictly inside its interval.
For \(w=0\), the perturbed means surround \(z\), and every generated bundle has utility zero, which is at least \(P_t\).
For \(w\ne0\), the proposed vectors form a rational basis of the utility hyperplane’s direction space. Their encoding lengths are polynomial, and the stated box-distance argument permits a sufficiently small rational perturbation of polynomial encoding length.
The resulting convex hull contains a relative neighborhood of \(z\) in that hyperplane.
The vertex maximizing coordinate \(j\) has \(r_j\ge z_j>0\). Both subsequent cases work:
The supporting-hyperplane application is justified: the hull is a compact convex polytope containing \(z\). The relative neighborhood forces any supporting normal to be a multiple of \(w\), and the two strict utility sides exclude such a nonzero normal.
Adding further bundles preserves interiority. The argument establishing a representation positive on every member of the finite set is also valid.
Minor issue 1 — omitted zero-valued addition case. The justification for adding \(h_t+e_o\) discusses positive and negative valuations but omits \(v_t(o)=0\). This allowed case is immediate because the utility is unchanged.
Minimum clarification: Explicitly include zero-valued additions in that justification.
The positive representations establish that a common strictly positive \(\eta\) is feasible across all types. The LP has polynomially many variables and rational coefficients of polynomial encoding length.
Minor issue 2 — mismatch with the stated LP theorem. The displayed LP leaves \(\eta\) without a lower bound. Its feasible region is therefore unbounded: decreasing \(\eta\) preserves feasibility. The bounded-region version of the LP theorem stated earlier does not literally apply to this formulation.
This is an expositional issue, not a substantive obstacle. The objective is bounded above by the type-total equalities and the inequalities \(x_{t,k}\ge\eta\).
Minimum clarification: State the exact rational LP theorem for a nonempty rational feasible region with finite optimal value, or explicitly restrict this LP to nonnegative \(\eta\) and verify boundedness.
The numerical bounds and conservation arguments check out.
The total possible decrease of any original mass is bounded by
\(\delta+2mRK\delta\le\eta/2\).
Hence every final mass stays positive. Reuse of a designated bundle across several corrections is covered by the factor \(m\).
The corrections retain the fixed PROP1 bundle sets and use only edges in \(E\). Lemma 1 consequently remains applicable even if aggregate utilities change.
The stated support bounds and polynomial encoding bounds are consistent with the constructions. A positive rational \(\eta\) of polynomial encoding length allows a grid exponent of polynomial size. The additional divisibility requirement for dyadic input masses and supplies also requires only polynomially many bits.
The empty-item case is handled explicitly. Types with no retained coordinates are handled by the empty bundle. Zero utility vectors, negative proportional benchmarks, and integer means do not invalidate the construction.
No blocking mathematical issue remains. The two clarifications above require no new lemma or new mathematical argument.
⟨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.