Answer: —
Theorem 3 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateDeciding whether an EF allocation exists is NP-Hard even for symmetric {0, 1, d}-graphical valuations.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite set of agent types \(T\) with rational masses \(\mu_t\), and item types \(G\) with rational per-capita supplies \(q_g\), where each item type has positive value for exactly two endpoint types and those values are in \(\{1,d\}\), does there exist an envy-free assignment of integral bundles to individuals? Formally, find masses \(x_{t,B}\ge 0\) over bundles \(B\in\mathbb{N}^{G}\) satisfying \(\sum_B x_{t,B}=\mu_t\) and \(\sum_{t,B}x_{t,B}B_g=q_g\), such that every positive-mass bundle pair \((t,B),(s,B')\) satisfies \(U_t(B)\ge U_t(B')\), where \(U_t(B)=\sum_g v_{t,g}B_g\).
A society is given by its support: a list \(T\) of \(\tau\) types with positive binary-rational masses \(\mu_t\), normalized by \(\sum_{t\in T}\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types.
There are \(m=|G|\) item types, with nonnegative binary-rational per-capita supplies \(q_g\). Each item type has two distinct endpoint types; at most one item type has any given unordered endpoint pair. An input integer \(d\ge 2\) is encoded in binary. Endpoint values belong to \(\{1,d\}\), may differ, and all other values are zero.
Individuals receive bundles \(B\in\mathbb Z_{\ge 0}^{G}\), allowing multiple units of an item type and empty bundles. Utilities are additive: \(U_t(B)=\sum_{g\in G}v_{t,g}B_g\). Items may be assigned to individuals who value them at zero.
An assignment consists of real masses \(x_{t,B}\ge 0\) satisfying \(\sum_Bx_{t,B}=\mu_t\) and \(\sum_{t,B}x_{t,B}B_g=q_g\) for every item type. It is envy-free if \(U_t(B)\ge U_t(B')\) whenever \(x_{t,B}>0\) and \(x_{s,B'}>0\), including \(t=s\); utility ties are permitted.
Let \(L\) be the total binary input length, including masses, supplies, endpoint data, and \(d\).
Is deciding whether such an envy-free assignment exists solvable in time polynomial in \(m,\tau,L\), or is it \(\mathrm{NP}\)-hard?
For finite agents and distinct indivisible items on a simple graph, envy-free allocation existence is NP-hard even with symmetric endpoint values in \(\{1,d\}\), while binary graphical valuations admit a polynomial-time algorithm ([source](https://arxiv.org/html/2410.14272v1)).
No complexity classification for exactly the mass model above was located.
The unrestricted decision problem remains unresolved here. I prove three results:
All arguments below apply to the stated mass model, except the explicitly identified auxiliary problem in Section 4.
Delete every item with zero supply. Nonnegativity of the supply equations implies that its coordinate is zero in every occupied bundle.
An occupied pair is a pair $(t,B)$ with $x_{t,B}>0$. Define
$$
V_t:=\sum_{g\in G}v_{t,g}q_g,
$$
and
$$
a_t:=\max\bigl(\{0\}\cup\{v_{t,g}:g\in G,\ v_{t,g}>0\}\bigr),
\qquad
\ell_t:=\max\{\lceil V_t\rceil,a_t\}.
$$
Here, all remaining items have positive supply.
In any envy-free assignment, each type $t$ has a nonnegative integer utility $u_t$ such that
$$
U_t(B)=u_t
\quad\text{for every occupied pair }(t,B),
$$
and
$$
U_t(B)\leq u_t
\quad\text{for every occupied pair }(s,B).
$$
Proof. Bundles form a countable set. Since $\mu_t>0$, the mass equation guarantees an occupied bundle for type $t$.
Comparisons in both directions between two occupied bundles belonging to $t$ force their utilities to agree. Their common utility is an integer because valuations and bundle coordinates are integers. Comparing an occupied bundle of $t$ against any other occupied bundle gives the second assertion. $\square$
Every envy-free assignment satisfies
$$
\ell_t\leq u_t\leq
\left\lfloor\frac{V_t}{\mu_t}\right\rfloor.
$$
For an item $g$ with endpoints $a,b$, every occupied bundle satisfies
$$
B_g\leq M_g:=
\left\lfloor
\min\left\{
\frac{V_a}{\mu_av_{a,g}},
\frac{V_b}{\mu_bv_{b,g}}
\right\}
\right\rfloor.
$$
Proof. The supply equations and nonnegativity give
$$
V_t=\sum_{s,B}x_{s,B}U_t(B).
$$
Nonnegativity justifies rearranging the sums, including before finite support has been established. By Lemma 1 and total population mass one,
$$
\mu_tu_t\leq V_t\leq u_t.
$$
These inequalities give the rounded bounds involving $V_t$.
Because $q_g>0$, some occupied bundle contains $g$. Each endpoint $t$ evaluates that bundle at least $v_{t,g}$, so $u_t\geq a_t$.
Finally, for either endpoint $t$ of $g$,
$$
v_{t,g}B_g\leq U_t(B)\leq u_t\leq \frac{V_t}{\mu_t}.
$$
Taking the minimum of the resulting coordinate bounds proves the claim. $\square$
The coordinate bounds have polynomial binary encoding length. Indeed,
$$
M_g\leq
\frac{d\sum_hq_h}{\min_t\mu_t},
$$
and the logarithm of the right-hand side is polynomially bounded by the input length.
Consequently, every feasible assignment uses bundles from a finite box, although that box can contain exponentially many bundles.
Every feasible instance has an envy-free assignment with at most $m+\tau$ occupied pairs and rational assignment masses of polynomial binary encoding length. Therefore the decision problem belongs to $\mathrm{NP}$.
Proof. If no positive-supply items remain, assigning the empty bundle to every type solves the instance. Assume otherwise.
Fix the utility vector $u$ of an existing envy-free assignment. Call $(t,B)$ admissible when
$$
U_t(B)=u_t,
\qquad
U_s(B)\leq u_s\quad\text{for every }s,
$$
and $0\leq B_g\leq M_g$ for every item. There are finitely many admissible pairs.
Associate the integer column
$$
a_{t,B}:=(e_t,B)\in\mathbb Z^{\tau+m}
$$
with each admissible pair. The assignment equations become
$$
\sum_{(t,B)}x_{t,B}a_{t,B}
=(\mu,q),
\qquad x_{t,B}\geq 0.
$$
If the currently positive columns are linearly dependent, choose a nonzero dependence
$$
\sum_i z_i a_i=0.
$$
Summing its type coordinates gives $\sum_i z_i=0$, so $z$ has both positive and negative entries. Set
$$
\eta:=\min_{i:z_i>0}\frac{x_i}{z_i},
\qquad
x'_i:=x_i-\eta z_i.
$$
The new coefficients remain nonnegative, satisfy the same equations, and eliminate at least one positive coefficient. Repeating this finite process leaves linearly independent positive columns. Their number $k$ is at most $m+\tau$.
Choose $k$ rows giving a nonsingular integer matrix $A_0$. The retained coefficients uniquely solve
$$
A_0x=b_0.
$$
They are therefore rational.
To bound their encoding lengths, put
$$
H:=\max\bigl(\{1\}\cup\{M_g:g\in G\}\bigr),
$$
and let $D$ be the product of the input denominators of the masses and supplies. Both $\log H$ and $\log D$ are polynomially bounded. Cramer's rule, applied after multiplying the right-hand side by $D$, gives denominators dividing $D\det A_0$. Moreover,
$$
|\det A_0|\leq k!H^k.
$$
The numerator determinants have polynomial binary encoding length as well, since the entries of $Db_0$ do. Thus the retained masses have polynomial encoding length.
All retained pairs remain admissible, so the assignment remains envy-free.
A certificate lists these pairs, their integer bundles, and their rational masses. Exact arithmetic verifies the mass equations, supply equations, positivity, and all pairwise envy comparisons in polynomial time. $\square$
For each item, let
$$
w_g:=\max\{v_{a,g},v_{b,g}\},
$$
where $a,b$ are its endpoints. Define the maximum available welfare and the minimum required welfare by
$$
W:=\sum_g w_gq_g,
\qquad
R:=\sum_t\mu_t\ell_t.
$$
Both quantities are computable in polynomial time.
The following statements hold for the unrestricted model.
The second statement eliminates assignments to zero-value recipients as a consequence of the input condition, rather than as an additional assumption.
For any assignment, its total welfare is at most $W$, because the recipient's value for each item is at most $w_g$. For an envy-free assignment, this gives
$$
\sum_t\mu_tu_t
=
\sum_{t,B}x_{t,B}U_t(B)
\leq W.
$$
By Lemma 2,
$$
R=\sum_t\mu_t\ell_t
\leq\sum_t\mu_tu_t.
$$
Thus $W<R$ is impossible.
Suppose $W=R$. Both inequalities must be equalities. Since $\mu_t>0$ and $u_t-\ell_t\geq 0$, equality implies $u_t=\ell_t$ for every $t$.
The welfare loss is
$$
W-\sum_t\mu_tu_t
=
\sum_{t,B,g}x_{t,B}(w_g-v_{t,g})B_g.
$$
Every summand is nonnegative. Its sum is zero, so an occupied pair containing $g$ must have $v_{t,g}=w_g$. In particular, its recipient is an endpoint. $\square$
I give the algorithm and its justification rather than assuming the endpoint-only result from the notes.
Prescribe $u_t=\ell_t$. A type $t$ may receive only items in
$$
E_t:=\{g:v_{t,g}=w_g\}.
$$
For an eligible incident item $g=\{t,s\}$, define
$$
C_{t,g}:=
\min\left\{
\left\lfloor\frac{u_t}{v_{t,g}}\right\rfloor,
\left\lfloor\frac{u_s}{v_{s,g}}\right\rfloor
\right\}.
$$
Let $S_t$ consist of the integer bundles satisfying
$$
B_g=0\quad\text{for }g\notin E_t,
\qquad
0\leq B_g\leq C_{t,g}\quad\text{for }g\in E_t,
\qquad
\sum_{g\in E_t}v_{t,g}B_g=u_t.
$$
These are exactly the allowable bundles of type $t$. The equality enforces its own utility. A different type $s$ values at most one item type in a bundle supported on $E_t$, because the graph is simple. The corresponding coordinate cap therefore enforces its entire envy inequality.
Feasibility is consequently equivalent to
$$
(\mu,q)\in P,
\qquad
P:=\operatorname{conv}\{(e_t,B):t\in T,\ B\in S_t\}.
$$
Indeed, the convex coefficients are precisely assignment masses: their sum is one because the type coordinates of every generating point sum to one.
It remains to optimize linear functions over $P$ in polynomial time.
Fix $t$ and rational item costs $c_g$. Divide its eligible items into the groups valued at one and at $d$. Let their total capacities be $C_1,C_d$. If $h$ is the number of $d$-valued units, the number of one-valued units must be $u_t-dh$. The feasible integer values of $h$ are exactly those in
$$
\max\left\{0,\left\lceil\frac{u_t-C_1}{d}\right\rceil\right\}
\leq h\leq
\min\left\{C_d,\left\lfloor\frac{u_t}{d}\right\rfloor\right\}.
$$
Within either group, a specified number of units can be obtained at minimum cost by filling capacities in increasing cost order. To justify this, if a more expensive coordinate is positive while a cheaper coordinate has unused capacity, shifting units from the former to the latter weakly decreases cost. Repeating yields the greedy allocation. For integer total counts, all its coordinates are integers.
Allowing real total counts gives piecewise-linear cost functions $F_1,F_d$. Their breakpoints are cumulative capacities in cost order. The optimal cost for an integer $h$ is therefore
$$
F_d(h)+F_1(u_t-dh).
$$
This expression has polynomially many breakpoints. Between consecutive breakpoints it is affine, so an integer minimum occurs at a feasible interval endpoint or at an integer immediately adjacent to a breakpoint. Checking these candidates yields an optimizing bundle, or detects that $S_t$ is empty. All calculations use polynomial-length numbers; none enumerate up to the numerical value of $d$ or $u_t$.
Doing this for every type, and including the cost of $e_t$, gives an exact optimization oracle for $P$.
Finally, apply strong optimization–strong separation equivalence for well-described rational polyhedra. This theorem permits lower-dimensional polyhedra. Here the dimension is $m+\tau$, and all generating points are integral with coordinates bounded by
$$
H'=\max\bigl(\{1\}\cup\{u_t:t\in T\}\bigr).
$$
Determinant bounds for supporting hyperplanes and affine-hull equations give a polynomial bound on their coefficient encoding lengths. Thus $P$ is well described, with a known polynomial encoding bound. The oracle yields strong separation and hence exact membership testing. See [Grötschel–Lovász–Schrijver, Theorem 6.4.9](https://www.zib.de/userpage/groetschel/pubnew/paper/groetschellovaszschrijver1988.pdf).
This proves the polynomial-time claim. $\square$
For prescribed nonnegative integer caps $u$, define
$$
K(u):=
\{B\in\mathbb Z_{\geq 0}^{G}:U_t(B)\leq u_t\text{ for every }t\}.
$$
By Lemma 1, every occupied bundle of an envy-free assignment belongs to $K(u)$.
The following result concerns a single bundle, not assignment existence.
Given $u$ and a subset $D\subseteq T$, deciding whether there is a bundle $B\in K(u)$ satisfying
$$
U_t(B)=u_t\quad\text{for every }t\in D
$$
is $\mathrm{NP}$-complete even under all of these restrictions:
Consequently, exact linear optimization over $K(u)$ is $\mathrm{NP}$-hard under the same restrictions.
Use the standard $\mathrm{NP}$-completeness of $3$-SAT. First reduce it to satisfiability of clauses requiring exactly one of three Boolean literals to be true.
Write $E(p,q,r)$ for this requirement. Replace a $3$-SAT clause
$$
L_1\lor L_2\lor L_3
$$
by
$$
E(s_1,s_2,s_3),
\qquad
E(s_i,\neg L_i,z_i)\quad\text{for }i=1,2,3,
$$
using fresh variables.
Let $b_i$ be the truth value of $L_i$. The latter three equations say
$$
s_i+(1-b_i)+z_i=1,
\qquad\text{equivalently}\qquad
z_i=b_i-s_i.
$$
A Boolean $z_i$ exists exactly when $s_i\leq b_i$.
If the original clause is satisfied, choose exactly one true literal as the selector with $s_i=1$, set the other selectors to zero, and take $z_i=b_i-s_i$. Conversely, exactly one selector is true, and its associated literal must be true. The replacement is therefore equivalent and has polynomial size.
It suffices to reduce this exactly-one satisfiability problem to the bundle problem.
Create the following kinds of vertices. All edges are distinct item types.
Clause vertex. Give it cap two and three incident literal edges, each valued at two at this vertex. Saturation requires
$$
2b_1+2b_2+2b_3=2,
$$
which expresses exactly one true literal when the edge coordinates are Boolean.
Inverter vertex. Give it cap one and two incident edges valued at one. Saturation requires
$$
a+b=1,
$$
so its output is the complement of its input.
Splitter vertex. Give it cap two, an input edge valued at two, and two output edges valued at one. Saturation requires
$$
2a+b+c=2.
$$
For Boolean coordinates, this forces
$$
b=c=1-a.
$$
Following each output with an inverter therefore produces two copies of the input.
Root sink. Give it cap one and a single incident edge valued at one. It will not be required to saturate. Its edge supplies a free Boolean input.
Every vertex except the root sinks belongs to $D$.
For each Boolean variable with $k$ occurrences, create a separate root sink.
If $k=1$, route its edge directly to the occurrence's clause vertex, inserting one inverter if the literal is negative.
If $k\geq 2$, use a rooted binary tree with $k$ leaves. Each internal vertex is a splitter. Place an inverter immediately after each of its two output edges. The resulting output is routed either to the next splitter's input or to a leaf occurrence.
Thus, before handling the literal's sign, every leaf carries the root's truth value. For a negative occurrence, insert one additional inverter before its clause vertex.
All newly introduced vertices are distinct. The construction is polynomial: a binary tree with $k$ leaves has $k-1$ splitters, two mandatory inverters per splitter, and at most one additional inverter per occurrence.
The graph is simple. In particular, different branches have different inverter vertices, and each root sink belongs to only one variable. Its maximum degree is three: splitters and clauses have degree three, inverters degree two, and root sinks degree one.
Every endpoint value is one or two.
Every edge touches either an inverter or a root sink where its value and the utility cap are both one. Therefore every $B\in K(u)$ satisfies
$$
0\leq B_g\leq 1.
$$
Since coordinates are integral, they are Boolean. This conclusion follows from the caps, rather than from a separate restriction on the bundle format.
Suppose the exactly-one formula is satisfiable. Give each root edge its variable's truth value. Propagate through splitters and inverters using their displayed equations. Every clause then receives its three literal truth values, exactly one of which is true. All vertices in $D$ saturate, and every root sink respects its cap.
Conversely, suppose a bundle respects all caps and saturates every vertex in $D$. Its coordinates are Boolean by Section 4.4. At each splitter, the two outputs complement the input; the following inverters restore that input value. Induction through each variable tree shows that all positive literal occurrences equal their root value, and all negative occurrences equal its complement. Saturation at a clause vertex then requires exactly one of its literals to be true.
Hence the bundle exists exactly when the Boolean formula is satisfiable.
The problem is in $\mathrm{NP}$ on these instances because the bundle is a binary vector and all constraints are directly verifiable. This proves $\mathrm{NP}$-completeness. $\square$
Define the integer item costs
$$
c_g:=\sum_{t\in D}v_{t,g},
$$
and the threshold
$$
H_D:=\sum_{t\in D}u_t.
$$
For every $B\in K(u)$,
$$
\sum_gc_gB_g
=
\sum_{t\in D}U_t(B)
\leq H_D.
$$
Equality holds exactly when every vertex in $D$ saturates, because each difference $u_t-U_t(B)$ is nonnegative.
Thus deciding whether the maximum reaches $H_D$ solves the preceding $\mathrm{NP}$-complete problem. The costs have constant encoding length.
Theorem 4 handles a class of the original instances without imposing any additional allocation rule. Its input condition forces both the utilities and the permitted recipients.
Theorem 5 identifies a difficulty in a different direction: an unrestricted individual bundle can encode Boolean branching and clauses through weighted endpoint constraints. Consequently, a general algorithm cannot obtain a polynomial-time optimization oracle for $K(u)$ unless $\mathrm{P}=\mathrm{NP}$.
However, Theorem 5 is not a hardness reduction for the user’s decision problem. It constructs neither type masses nor supplies. Moreover, its bundle must simultaneously saturate many types, whereas envy-freeness requires an occupied bundle to saturate its recipient's utility and merely respect the other types' caps. Assignment feasibility also concerns a mixture of bundles with prescribed marginals.
The remaining task is therefore to obtain a polynomial-time method outside the tight welfare case, or to turn a combinatorial construction into a reduction that survives type splitting, repeated units, and endogenous utilities.
⟨structured verdict parsed — rendered above⟩
The output establishes substantial partial results, but it does not settle the decision problem in USER_TASK. Its claim of partial progress is accurate. I found no false central step in the three substantive results. The polynomial-time special case has one minor omission concerning the encoding bound required by the cited polyhedral theorem.
The unrestricted mass problem remains unclassified: membership in $\mathrm{NP}$, a polynomial-time special case, and hardness of an auxiliary bundle problem do not establish either requested alternative.
This is valid. For an item with zero supply, the supply equation is a sum of nonnegative terms. Any occupied bundle with a positive coordinate for that item would contribute a positive term, contradicting zero supply.
Removing these coordinates preserves feasibility and envy comparisons.
The argument is correct.
The lemma correctly uses the task’s requirement that envy comparisons also include individuals of the same type.
The identity
$$
V_t=\sum_{s,B}x_{s,B}U_t(B)
$$
is valid. Expanding additive utility and rearranging nonnegative sums is justified even before finite support is established.
The inequalities
$$
\mu_tu_t\leq V_t\leq u_t
$$
follow respectively from retaining the contributions of type $t$, and from bounding every occupied bundle’s evaluation by $u_t$ and using total mass one. The rounding is correct.
The additional lower bound $u_t\geq a_t$ is also valid: every positive-supply item occurs in some occupied bundle, and each endpoint must evaluate that bundle at least as highly as its value for one unit of the item.
The coordinate bound follows from applying the utility upper bound at both endpoints. Positive masses and positive endpoint valuations make all displayed divisions legitimate.
The polynomial encoding claim is sound. Products, sums, and ratios of the input rationals have polynomial binary encoding length. The coordinate bounds therefore establish a finite universe of possible occupied bundles.
Assessment: Correct.
Theorem 3 is correct.
Fixing the utility vector of an existing assignment is legitimate for an existence proof about certificates. Lemma 2 places every occupied pair in the stated finite admissible set.
The columns $(e_t,B)$ encode exactly the type-mass and item-supply equations.
The dependence argument is valid. Summing the type coordinates of a linear dependence gives
$$
\sum_i z_i=0.
$$
A nonzero dependence must therefore contain both positive and negative coefficients.
The specified choice of $\eta$ preserves nonnegativity and eliminates at least one positive coefficient. It introduces no new column. Since the initial admissible universe is finite, repetition terminates with linearly independent positive columns, numbering at most $m+\tau$.
This procedure is used only to prove existence of a small certificate; the argument does not incorrectly claim that enumerating the admissible universe is polynomial-time.
Linearly independent columns admit a nonsingular square row submatrix. The retained coefficients uniquely solve its rational system, so they are rational.
The denominator-clearing and determinant bounds are sufficient. In particular:
The proposed certificate can be checked using exact rational arithmetic. Pairwise envy comparisons between all listed occupied pairs include comparisons within a type. The certificate size and the number of comparisons are polynomial.
The no-positive-supply case is correctly handled by empty bundles.
Assessment: Correct; the original decision problem belongs to $\mathrm{NP}$.
Both inequalities are valid:
$$
R\leq\sum_t\mu_tu_t\leq W.
$$
Consequently, $W<R$ rules out an assignment.
When $W=R$, positivity of every $\mu_t$ forces $u_t=\ell_t$ for every type. The welfare-loss expression is a sum of nonnegative terms, so every item occurring in an occupied bundle must be assigned to a recipient attaining its maximum endpoint value.
This correctly derives the recipient restriction from the input condition. It does not silently impose an additional allocation rule.
The characterization by $S_t$ is correct.
For a bundle supported on $E_t$, another type $s\neq t$ can value at most the single item joining $s$ and $t$. This uses precisely the simple-graph hypothesis. The coordinate cap therefore enforces the whole envy inequality for $s$.
The own-utility equality enforces saturation for the recipient. Empty bundles and types with no eligible items are covered by the displayed constraints.
The equivalence
$$
(\mu,q)\in P
$$
is valid. Every generating point has type coordinates summing to one, so convex coefficients have exactly the normalization required for assignment masses. Conversely, every allowable assignment gives the required convex combination.
The algorithm is sound.
Thus the algorithm avoids enumeration over the numerical magnitudes of $d$ and $u_t$.
The cited theorem does provide oracle-polynomial equivalence between strong optimization and strong separation for well-described rational polyhedra. Its statement does not require full dimensionality. The application is therefore appropriate. [Grötschel–Lovász–Schrijver, Theorem 6.4.9](https://www.zib.de/userpage/groetschel/pubnew/paper/groetschellovaszschrijver1988.pdf).
Minor issue: The write-up asserts, without displaying a bound, that determinant estimates provide a known polynomial encoding bound for supporting inequalities and affine-hull equations. This is a routine encoding justification, but it is the least explicit part of the theorem application.
Minimum clarification: State the definition of “well described” being used and give an explicit polynomial encoding bound, or a precise standard reference for the bounded-vertex-coordinate implication, including lower-dimensional polytopes.
Assessment: Sound in substance, with a minor expositional gap.
The reduction from $3$-SAT to exactly-one satisfiability is correct.
The equation
$$
z_i=b_i-s_i
$$
has a Boolean solution exactly when $s_i\leq b_i$. The selector clause chooses exactly one satisfied original literal. Fresh auxiliary variables prevent interference between clause replacements.
Each gadget has the claimed behavior once edge coordinates are Boolean:
The construction has polynomial size. Distinct intermediate inverter vertices prevent parallel edges, including when a variable occurs repeatedly in one clause. Endpoint types are distinct, and all degrees satisfy the claimed maximum of three.
Every edge touches an inverter or root sink with cap one and endpoint value one. Consequently, every bundle in $K(u)$ has Boolean coordinates. This correctly derives Booleanity from the constraints rather than assuming it.
Both directions are valid. A satisfying truth assignment propagates through the gadgets and saturates all vertices in $D$. Conversely, saturation and Booleanity force consistent literal values throughout each variable tree and exactly one true literal at each clause.
Verification of the resulting binary bundle is polynomial-time, establishing the claimed restricted $\mathrm{NP}$-completeness.
The objective identity and threshold argument are correct. Equality with $H_D$ occurs exactly when every required vertex saturates. Each item cost involves at most its two endpoint values, so the constant encoding-length assertion is also correct.
Assessment: Correct auxiliary hardness result.
Major completion issue: The output does not decide whether unrestricted envy-free assignment existence is polynomial-time solvable or $\mathrm{NP}$-hard.
This is not a hidden flaw in the auxiliary reduction: the prover explicitly acknowledges its limited scope. The reduction supplies neither masses nor supplies and requires one bundle to saturate multiple designated types. That requirement is different from the occupied-bundle conditions in the assignment problem.
Accordingly:
Resolving this completion issue requires a further result addressing the original assignment problem; it cannot be repaired by an expositional clarification.
⟨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.