← back to the atlas

High-Multiplicity Fair Allocation Using Parametric Integer Linear Programming (d4-conf-ecai-2023-0334)

Answer: —

The anchor (named result in the paper)

Theorem 1 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateLet I be an instance of the EEF–Allocation problem with the maximum input utility value umax = 2o(log |I|).

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

The continuous mirror question, as graded

Given finitely many complete utility types \(T\), a rational population distribution \(\mu\), indivisible item types with rational per-capita supplies \(q_i\), and additive utilities \(u_t(i)\), decide whether there exists a finitely supported mass allocation \(x_{t,b}\) over integral bundles \(b\in\mathbb{Z}_{\ge0}^m\) satisfying type-mass and supply constraints, envy-freeness across all positive-mass bundles, and Pareto efficiency under type-preserving mass couplings; construct such an allocation when one exists.

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

A society is given by its support: the list of the \(\tau\) complete utility types with positive mass, each mass \(\mu_t\) a binary rational, with \(\sum_t\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types.
There are \(m\ge1\) item types, binary rational per-capita supplies \(q_i>0\), and additive utilities \(u_t(i)\in\mathbb Z_{\ge0}\). Let \(L\) be the total input bit length. Fix a computable function \(g:\mathbb N\to\mathbb N\) satisfying \(g(L)=o(\log L)\), and impose the promise \(\max_{t,i}u_t(i)\le2^{g(L)}\).
A feasible allocation is a finitely supported family \(x_{t,b}\in\mathbb R_{\ge0}\), indexed by integral bundles \(b\in\mathbb Z_{\ge0}^m\), satisfying \(\sum_bx_{t,b}=\mu_t\) and \(\sum_{t,b}x_{t,b}b_i\le q_i\). Bundles have no additional size or coordinate bounds; unused supply is permitted.
Write \(u_t(b)=\sum_i u_t(i)b_i\). Envy-freeness requires \(u_t(b)\ge u_t(c)\) whenever \(x_{t,b}>0\) and \(x_{s,c}>0\), including comparisons within a type; utility ties are allowed.
An allocation \(x\) is Pareto-dominated if there exist a feasible finitely supported allocation \(y\) and nonnegative real coupling masses \(\gamma_{t,b,c}\) with \(\sum_c\gamma_{t,b,c}=x_{t,b}\), \(\sum_b\gamma_{t,b,c}=y_{t,c}\), and \(\gamma_{t,b,c}>0\Rightarrow u_t(c)\ge u_t(b)\), such that \(\sum_{t,b,c:\,u_t(c)>u_t(b)}\gamma_{t,b,c}>0\). The competitor need not be envy-free. Pareto efficiency means absence of such domination.

Is deciding whether an envy-free Pareto-efficient allocation exists solvable in polynomial time in \(m,\tau,L\), or is it NP-hard? If NP-hard, can it nevertheless be solved in \(f(m+\tau)\operatorname{poly}(L)\) time? In either algorithmic case, can such an allocation also be constructed when it exists?

The discrete problem admits an \(f(m+n)\operatorname{poly}(L)\)-time algorithm under the same subpolynomial utility bound, where \(n\) is the number of agents ([Bredereck et al.](https://arxiv.org/pdf/2005.04907)).
Without that bound, discrete existence is \(\Sigma_2^P\)-complete for additive preferences ([de Keijzer et al.](https://recherche.noiraudes.net/resources/papers/ADT09.pdf)); with unary utilities it is W[1]-complete parameterized by \(n\) even for identical preferences ([Bliem et al.](https://www.ijcai.org/Proceedings/16/Papers/022.pdf)).

Modeling choices made when packaging the task

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

1. Proved results and remaining question.

I prove that existence is NP-hard even with utilities in $\{0,1\}$, equal dyadic type masses, and dyadic supplies. Thus the hardness holds for every function $g$ in the question.

I also prove a constructive algorithm with running time
$$ F(m+\tau,\Delta)\operatorname{poly}(L), \qquad \Delta=\max_{t,i}u_t(i), $$
for a computable function $F$. In particular, this gives a constructive $f(m+\tau)\operatorname{poly}(L)$ algorithm whenever the utility bound is constant.

I do not establish the requested parameterized running time for the full, potentially unbounded, subpolynomial utility promise. That part remains open in this write-up.

2. Two structural lemmas.

Write $u_t$ for the utility vector of type $t$.

Lemma 1: envy-freeness fixes one integer utility level per type.
In an envy-free allocation, there is a vector
$$ U=(U_1,\ldots,U_\tau)\in\mathbb Z_{\ge0}^{\tau} $$
such that every bundle assigned positive mass to type $t$ has utility $U_t$.

Indeed, comparing two positively assigned bundles within type $t$ in both directions gives equality. Every type has nonempty support because $\mu_t>0$.

Moreover, every bundle assigned to any type satisfies
$$ u_s(b)\le U_s \qquad\text{for every type }s. $$
This follows by comparing that bundle with a positively assigned bundle of type $s$. Consequently, define
$$ B_t(U)= \left\{ b\in\mathbb Z_{\ge0}^{m}: u_t(b)=U_t,\ u_s(b)\le U_s\text{ for every }s \right\}. $$
An allocation is envy-free with utility vector $U$ exactly when type $t$ uses only bundles in $B_t(U)$.

Feasibility also implies
$$ 0\le U_t\le \frac{u_t\cdot q}{\mu_t}. $$
To see the upper bound, the aggregate utility assigned to type $t$ is $\mu_tU_t$, and its item consumption is coordinatewise at most $q$.

Lemma 2: a characterization of Pareto efficiency for binary utilities.
Suppose all utilities belong to $\{0,1\}$ and every item type is valued by at least one utility type. A feasible allocation is Pareto-efficient if and only if:

For necessity, suppose item $i$ has positive unused supply. Choose a type valuing $i$ and a positively assigned bundle $b$ of that type. For a sufficiently small positive mass $\varepsilon$, replace $b$ by $b+e_i$ on that mass. This is feasible and strictly improves those recipients.

Next, suppose positive mass of a bundle $b$ assigned to type $t$ contains item $i$, but $u_t(i)=0$. Choose a type $s$ with $u_s(i)=1$ and a positively assigned bundle $c$ of type $s$. Necessarily $s\ne t$. On an equal sufficiently small positive mass, replace
$$ b\longmapsto b-e_i, \qquad c\longmapsto c+e_i. $$
Consumption is unchanged, type $t$ loses no utility, and type $s$ strictly gains. Both modifications give finite allocations and couplings of the kind required in the question.

For sufficiency, let
$$ W(x)=\sum_{t,b}x_{t,b}u_t(b). $$
Every feasible allocation satisfies
$$ W(x)\le\sum_iq_i, $$
because each item contributes at most one unit of utility. The two stated conditions give equality. Any domination coupling would strictly increase $W$, contradicting this upper bound. This proves the lemma.

3. NP-hardness with binary utilities and dyadic data.

Reduce from graph $4$-colorability. This problem is NP-hard: adjoining one vertex adjacent to every vertex of a graph reduces $3$-colorability to $4$-colorability.

Let $G=(V,E)$ be a nonempty graph and write $N=|V|$. Construct a graph $H$ whose vertices are
$$ V(H)=V\times\{1,2,3,4\}. $$
Its edges are:

An independent set in $H$ contains at most one vertex from each set
$$ \{(v,1),(v,2),(v,3),(v,4)\}. $$
Thus an independent set of size $N$ is exactly a proper $4$-coloring of $G$.

Let $C=|E(H)|$, and let $T$ be the smallest power of two satisfying $T\ge C+1$. Set
$$ \mu=\frac1T. $$

The society has the following $T$ distinct utility types, each of mass $\mu$:

There is one vertex item $a_z$ for every $z\in V(H)$, with supply
$$ q_{a_z}=\frac{\mu}{4}. $$
There is also one private item $p_t$ for every non-main type $t$, with supply
$$ q_{p_t}=\mu. $$

All unspecified utilities are zero. The positive utilities are:

All masses and supplies are dyadic. There are
$$ \tau=T,\qquad m=4N+T-1, $$
and $T<2(C+1)$, so the construction has polynomial encoding length. The utility rows are distinct because every non-main type has its own private item.

Necessity. Suppose an envy-free Pareto-efficient allocation exists.

Every item is valued by some type, so Lemma 2 applies. All supplies are consumed, and items are assigned only to types valuing them.

In particular, all of private item $p_t$ is assigned to type $t$. Let $U_t$ be the integer utility level from Lemma 1.

For a constraint type $e=\{z,z'\}$, private-item consumption gives
$$ \mu U_e\ge q_{p_e}=\mu. $$
Its total utility cannot exceed the total supply of its three valued items:
$$ \mu U_e \le q_{p_e}+q_{a_z}+q_{a_{z'}} =\mu+\frac{\mu}{4}+\frac{\mu}{4} =\frac32\mu. $$
Therefore
$$ 1\le U_e\le\frac32. $$
Since $U_e$ is integral, $U_e=1$.

Its private item already accounts for aggregate utility $\mu$. Hence it receives no positive aggregate quantity of either endpoint vertex item. Filler types value no vertex items. Consequently, all vertex items are assigned to the main type.

The main type’s aggregate utility is therefore
$$ \sum_{z\in V(H)}q_{a_z} =4N\frac{\mu}{4} =N\mu. $$
Its common utility level is $U_0=N$.

Consider any positively assigned main-type bundle $b$. Pareto efficiency excludes private items from $b$, since the main type does not value them. For each edge $e=\{z,z'\}$ of $H$, envy-freeness of constraint type $e$ requires
$$ b_{a_z}+b_{a_{z'}}\le U_e=1. $$
The clique edges within each original vertex’s four choices imply that these coordinates are binary and that at most one choice is present for each $v$. Since
$$ \sum_zb_{a_z}=U_0=N, $$
exactly one choice is present for every $v$. The remaining edge constraints exclude equal colors on adjacent vertices. Hence $b$ determines a proper $4$-coloring of $G$.

Sufficiency. Conversely, suppose $G$ has a proper $4$-coloring.

Apply the four cyclic permutations of the colors to this coloring. Each resulting coloring determines a bundle of $N$ vertex items. Assign each bundle main-type mass $\mu/4$, merging coincident bundles if necessary.

For every $v$ and color $a$, exactly one of these four bundles contains $a_{(v,a)}$. Thus all vertex supplies are consumed exactly.

Give every non-main type its private singleton bundle on its entire mass $\mu$. This consumes every private supply exactly.

The allocation is envy-free:

Every allocated item is valued by its recipient, and every supply is exhausted. Lemma 2 proves Pareto efficiency.

We have proved the equivalence
$$ G\text{ is }4\text{-colorable} \quad\Longleftrightarrow\quad \text{the constructed society admits an envy-free Pareto-efficient allocation}. $$
Since $\Delta=1\le 2^{g(L)}$, this proves NP-hardness under the stated promise for every permitted $g$.

4. Exact integer-hull formulation for general utilities.

For an integer utility vector $U$, define
$$ C_t(U)= \left\{ c\in\mathbb Z_{\ge0}^{m}:u_t(c)\ge U_t \right\}, $$
and the integer hulls
$$ H_t^{=}(U)=\operatorname{conv}B_t(U), \qquad H_t^{\ge}(U)=\operatorname{conv}C_t(U). $$
Here convex hull means finite convex combinations.

Envy-free feasibility with utility vector $U$ is equivalent to
$$ \exists z_1,\ldots,z_\tau: \quad z_t\in H_t^{=}(U), \qquad \sum_t\mu_tz_t\le q. $$
The forward direction takes conditional mean bundles. For the reverse direction, a finite convex representation of each $z_t$, scaled by $\mu_t$, gives the required allocation.

Such an allocation is Pareto-dominated exactly when
$$ \exists w_1,\ldots,w_\tau: \quad w_t\in H_t^{\ge}(U), \qquad \sum_t\mu_tw_t\le q, \qquad \sum_t\mu_tu_t(w_t)>\sum_t\mu_tU_t. $$

For the forward direction, a domination coupling assigns each type only bundles of utility at least $U_t$. Its positive mass of strict improvements makes the displayed inequality strict.

Conversely, finite convex representations of the $w_t$ give an allocation $y$ supported on bundles of utility at least $U_t$. Couple it to the original allocation $x$ using
$$ \gamma_{t,b,c}=\frac{x_{t,b}y_{t,c}}{\mu_t}. $$
The marginals are $x$ and $y$. Every positive coupling entry is a weak improvement, and the strict aggregate inequality implies positive coupling mass of strict improvements.

In particular, Pareto efficiency of an envy-free allocation depends only on its utility vector $U$, rather than on its particular bundle distribution.

5. A constructive algorithm parameterized also by the utility bound.

Set
$$ k=m+\tau,\qquad \Delta_0=\max(1,\Delta). $$
The following argument proves a computable
$$ F(k,\Delta_0)\operatorname{poly}(L) $$
bound.

The integer-hull theorem of Eisenbrand and Rothvoss states that, for an integer matrix $A$ with bounded dimension and entries, one can compute a modulus $D$ and matrices $B,C$ such that, for every residue $r$, a computable vector $a_r$ satisfies
$$ \operatorname{conv}\{v\in\mathbb Z^d:Av\le b\} = \{v\in\mathbb R^d:Bv\le a_r+Cb\} \quad\text{when }b\equiv r\pmod D. $$
The computation depends only on the dimensions and coefficient bound; their Remark 1 allows repeated rows. See [Theorem 1 and Remark 1](https://arxiv.org/pdf/2501.02347).

For $B_t(U)$, the defining inequalities are
$$ -b_i\le0,\qquad u_s(b)\le U_s\quad(s=1,\ldots,\tau),\qquad -u_t(b)\le-U_t. $$
For $C_t(U)$, they are
$$ -c_i\le0,\qquad -u_t(c)\le-U_t. $$
Thus every coefficient matrix has dimensions bounded by $k$ and entries bounded in absolute value by $\Delta_0$. Every right-hand side is an integer linear function of $U$. These check all the theorem’s hypotheses.

Take a common multiple of the finitely many resulting moduli, and enumerate the residue vector of $U$ modulo this common modulus. The number of branches depends only on $k,\Delta_0$.

Within each branch, all the hulls have descriptions
$$ H_t^{=}(U)=\{z:B_t^{=}z\le a_t^{=}+E_t^{=}U\}, $$
$$ H_t^{\ge}(U)=\{w:B_t^{\ge}w\le a_t^{\ge}+E_t^{\ge}U\}. $$
These are linear inequalities jointly in the mean bundles and $U$.

Substitute them into the two systems in Section 4. Eliminate their real mean-bundle variables by Fourier–Motzkin elimination, retaining strict inequalities where they occur. This gives:

The number of variables eliminated and all resulting numbers of inequalities are bounded by functions of $k,\Delta_0$. Their coefficient encoding lengths are at most a parameter-dependent factor times a polynomial in $L$.

We seek an integer $U$ in the selected residue class satisfying
$$ 0\le U_t\le\frac{u_t\cdot q}{\mu_t}, \qquad \mathcal E(U), \qquad \neg\mathcal D(U). $$
The negation of a conjunction is a disjunction of negated individual inequalities. Branch on one violated inequality of $\mathcal D(U)$. Writing
$$ U=r+Dv,\qquad v\in\mathbb Z^\tau, $$
each resulting branch is an integer linear feasibility problem with $\tau$ variables.

After clearing denominators, strict inequalities can be replaced exactly by weak integer inequalities. For example, with integral data,
$$ a\cdot v<b \quad\Longleftrightarrow\quad a\cdot v\le b-1. $$
[Lenstra’s fixed-dimension integer-programming algorithm](https://pub.math.leidenuniv.nl/~lenstrahw/PUBLICATIONS/1983i/art.pdf) decides these systems and returns a feasible integer vector when one exists. The number of branches and their parameter-dependent sizes yield the claimed running time.

Construction. Once a suitable $U$ is found, delete item types valued by nobody. This preserves all utilities and all domination possibilities after projection. If no items remain, assigning empty bundles is sufficient.

Otherwise every coordinate is valued by some type. Hence $B_t(U)$ is bounded: if $u_s(i)>0$, then
$$ b_i\le\frac{U_s}{u_s(i)}. $$
Each $H_t^{=}(U)$ is therefore a rational polytope whose vertices are integral bundles. Enumerate its vertices and solve the finite allocation linear program over those bundles. Section 4 guarantees feasibility.

A basic feasible solution has at most $m+\tau$ positive allocation masses: after adding the $m$ supply slacks, the system has $\tau+m$ equations. Its masses are rational. Every positively used bundle satisfies the envy constraints, and the absence of $\mathcal D(U)$ proves Pareto efficiency. This construction has the same parameterized running-time bound.

6. What this does and does not settle.

For every fixed utility bound, the algorithm above proves constructive fixed-parameter tractability in $m+\tau$. This includes the binary-utility instances used in the hardness reduction.

For the full promise, however, the theorem supplies an unrestricted computable dependence on $\Delta$. Such a dependence cannot automatically be absorbed into $f(k)\operatorname{poly}(L)$. For example, a dependence $2^\Delta$ is already superpolynomial when
$$ \Delta=2^{\lfloor\sqrt{\log_2L}\rfloor}, $$
even though this utility bound satisfies the promise.

Thus the missing result is an algorithm whose dependence on the utility bound is sufficiently controlled—or another argument removing that parameter. The NP-hardness proof is complete; the requested parameterized classification for the full promise is not settled here.

⟨structured verdict parsed — rendered above⟩

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

The output is correct in its substantive proved claims but incomplete as an answer to the full task. The binary-utility NP-hardness reduction is valid. The integer-hull formulation and constructive algorithm parameterized by $m+\tau$ and the utility bound are also sound, subject to minor precision issues. The requested constructive $f(m+\tau)\operatorname{poly}(L)$ algorithm under the full subpolynomial utility promise remains unestablished, as the prover explicitly acknowledges.

1. Lemma 1: utility levels and envy constraints

Verified.

Within-type comparisons in both directions force all positively assigned bundles of type $t$ to have the same utility. This common utility is an integer because utilities and bundle coordinates are integers. Positive type mass ensures that each type has a positively assigned bundle.

For any allocated bundle $b$ and any type $s$, comparison with a positively assigned bundle of type $s$ gives
$$ u_s(b)\le U_s. $$
Conversely, membership of every positively assigned type-$t$ bundle in $B_t(U)$ supplies exactly the inequalities required for envy-freeness, including within-type comparisons.

The upper bound is correct:
$$ \mu_tU_t = \sum_bx_{t,b}u_t(b) \le u_t\cdot q. $$
This uses nonnegative utilities and the fact that type $t$ consumes no more than the total available supply coordinatewise. Division by $\mu_t$ is valid because $\mu_t>0$.

Zero utility vectors and utility ties cause no exception.

2. Lemma 2: binary-utility Pareto efficiency

Verified under its stated hypotheses.

For unused supply, a sufficiently small positive mass of recipients can receive one additional integral item. The modification consumes only that mass of additional supply and strictly improves recipients who value the item.

For an item assigned to a recipient who does not value it, the proposed transfer is valid:

These modifications admit the required couplings and preserve finite support.

For sufficiency, binary utilities imply
$$ W(x)\le\sum_iq_i. $$
Full consumption with every item assigned to a recipient valuing it attains equality. Any domination coupling would strictly increase $W$: utility differences are nonnegative everywhere and positive on a set of positive coupling mass. This contradicts the same bound for the competing allocation.

The lemma concerns arbitrary feasible competitors, so it matches the task’s Pareto definition.

3. NP-hardness reduction

Verified.

Source problem. The stated universal-vertex transformation correctly reduces graph $3$-colorability to graph $4$-colorability: the new vertex requires a color unavailable to every original vertex.

Graph construction. Each original vertex induces a clique on its four choices. An independent set therefore contains at most one choice per original vertex. An independent set of size $N$ selects exactly one choice for each original vertex, and the other edges prohibit equal colors on adjacent vertices. The claimed correspondence is correct.

Encoding and promise. There are polynomially many graph edges and hence polynomially many types and items. In particular,
$$ C=6N+4|E|. $$
The choice of $T$ satisfies
$$ C+1\le T<2(C+1). $$
The masses sum to one, all supplies are positive, and all masses and supplies are dyadic. Private items distinguish the non-main utility rows; each such row also differs from the main row. Thus the listed types are genuinely distinct support types.

All utilities are binary, so the construction satisfies the promised utility bound for every permitted $g$.

Necessity. Lemma 2 forces each private item to its unique valuing type and exhausts its supply. For a constraint type,
$$ 1\le U_e\le\frac32, $$
and integrality forces $U_e=1$. Its private-item consumption already supplies its entire aggregate utility, so it consumes no endpoint vertex items.

Consequently, all vertex supply goes to the main type, whose common utility is $N$. Each positively assigned main bundle satisfies
$$ b_{a_z}+b_{a_{z'}}\le1 $$
for every edge of $H$. The clique inequalities force binary coordinates and at most one choice per original vertex. Total utility $N$ forces exactly one choice per vertex. This produces a proper coloring.

This argument correctly excludes repeated copies of a vertex item despite the absence of coordinate bounds in the task.

Sufficiency. The four cyclic color permutations place each vertex item in exactly one of the four main bundles. Assigning mass $\mu/4$ to each therefore consumes exactly its supply. Private singleton bundles consume every remaining supply.

All envy comparisons are covered:

Every allocated item is valued by its recipient, so Lemma 2 establishes Pareto efficiency.

The reduction proves NP-hardness for the continuous problem under the full stated promise. It does not assert or establish membership in NP.

4. Integer-hull formulation

Verified.

Conditional means belong to the stated convex hulls because the allocations have finite support. Conversely, the definition of convex hull as finite convex combinations supplies finitely supported allocations with the required masses and consumption.

For domination, every positively assigned original type-$t$ bundle has utility $U_t$. The coupling condition therefore forces every positively assigned competing bundle of that type to have utility at least $U_t$.

The reverse coupling
$$ \gamma_{t,b,c}=\frac{x_{t,b}y_{t,c}}{\mu_t} $$
is well defined, nonnegative, and has both required marginals. Its positive entries are weak improvements. The strict aggregate utility inequality guarantees positive mass of strict improvements.

Thus Pareto efficiency really does depend only on $U$ among envy-free allocations with that utility vector. The competing allocation is correctly allowed to violate envy-freeness.

5. Algorithm parameterized by the utility bound

Verified in substance, with two minor precision issues.

Integer-hull theorem. The cited theorem provides residue-dependent affine descriptions of integer hulls for integer right-hand sides. Its repeated-row extension permits the matrices used here, with dependence also on the row count. The prover’s application satisfies these hypotheses: the matrices are integral, their dimensions are parameter bounded, their entries are bounded by $\Delta_0$, and their right-hand sides are integer linear functions of $U$. Unbounded hulls are not excluded by the theorem. See [Eisenbrand and Rothvoss, Theorem 1 and Remark 1](https://arxiv.org/pdf/2501.02347).

Minor issue: exact matrix dimensions. The displayed system for $B_t(U)$ has $m+\tau+1=k+1$ rows, rather than at most $k$ rows as literally claimed. Its dimension is still bounded by a function of $k$, so this does not affect the theorem application or running time.

Minimum clarification: replace “dimensions bounded by $k$” with “dimensions bounded by $k+1$” or “dimensions bounded by a function of $k$.”

Residue enumeration. A common multiple of the moduli suffices. Fixing $U$ modulo that common multiple fixes every right-hand-side residue, including coordinates involving $-U_t$. The number of branches depends only on the parameters.

Real-variable elimination. Fourier–Motzkin elimination, retaining strict inequalities, gives exact projections of the two finite linear systems. The resulting inequality counts and coefficient bit lengths have the claimed parameter-dependent bounds.

Negating the conjunction describing domination and branching on a violated inequality is logically correct. Substituting $U=r+Dv$ leaves only integer variables. Clearing rational denominators makes the stated conversion of strict inequalities exact.

Minor issue: precise integer-programming running time. The write-up invokes “fixed-dimension” polynomial solvability without explicitly stating that the polynomial exponent is independent of the dimension. That distinction matters for an FPT claim. The stronger bound needed here is available for Lenstra-type integer programming, so this is an expositional omission rather than a substantive algorithmic gap. The uniform polynomial dependence is explicitly discussed in [Dadush, Eisenbrand, and Rothvoss, introduction](https://pmc.ncbi.nlm.nih.gov/articles/PMC11870894/).

Minimum clarification: state a feasibility-and-witness theorem with running time $h(d)S^c$, where $d$ is the number of integer variables, $S$ is the system’s binary encoding length, and $c$ is an absolute constant. Identify $d=\tau$ and the established bound on $S$.

6. Construction

Verified.

Deleting globally unvalued items preserves utility comparisons and domination possibilities. Projecting allocations removes only utility-zero coordinates; conversely, projected allocations can be lifted with zero consumption of those coordinates.

After deletion, every coordinate is bounded in $B_t(U)$ by a positive coefficient in some envy constraint. Hence each relevant integer hull is a bounded rational polytope with integral vertices.

The previously computed hull descriptions have parameter-bounded numbers of inequalities. Enumerating their vertices therefore has the claimed parameterized complexity; the potentially large numerical values of $U$ affect binary encoding length rather than requiring enumeration of all bundles.

Using these vertices in an allocation linear program preserves feasibility. The basic-feasible-solution support bound of $m+\tau$ is correct after adding supply slacks. The allocation masses are rational, and the selected bundles have binary descriptions of the required length.

Absence of the domination system proves Pareto efficiency of the constructed allocation. The all-zero-utility case is also handled correctly by empty bundles.

7. Unresolved part of the assignment

Major incompleteness of scope, explicitly acknowledged by the prover.

The algorithm proves
$$ F(m+\tau,\Delta_0)\operatorname{poly}(L), $$
and hence constructive FPT for every fixed utility bound. It does not prove the requested bound with parameter $m+\tau$ alone under the full promise.

The warning about unrestricted dependence on $\Delta$ is correct. For the displayed example,
$$ \frac{2^{\lfloor\sqrt{\log_2L}\rfloor}}{\log_2L}\longrightarrow\infty, $$
so a factor $2^\Delta$ exceeds every fixed polynomial in $L$. Subpolynomial growth of $\Delta$ does not control an arbitrary computable function of $\Delta$.

Minimum additional requirement: establish a parameter-only running-time bound under the full promise, including construction, or establish an appropriate obstruction to such a bound. This requires additional mathematics; it cannot be supplied by clarifying the current argument. The prover does not claim otherwise.

The overall result is therefore partial despite the valid NP-hardness classification. Under the requested JSON convention, continuous_status must be "unresolved" when result_status is "partial".

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