← back to the atlas

Parameterized Guarantees for Almost Envy-Free Allocations (aamas24-00023)

Answer: —

The anchor (named result in the paper)

Theorem 3.8 — class: algorithmic

The continuous mirror question, as graded

Given a finite type set \(T\), rational masses \(\mu_t\), \(m\) indivisible good classes with rational per-agent supplies \(\rho_g\), additive values \(v_t(g)\), and \(\gamma=\min_g\frac{\min_{t:v_t(g)>0}v_t(g)}{\max_t v_t(g)}\), compute a finite-support mass distribution \(\pi_{t,B}\) over \(t\in T\) and \(B\in\mathbb{Z}_{\ge 0}^m\) satisfying \(\sum_B\pi_{t,B}=\mu_t\), \(\sum_{t,B}\pi_{t,B}B_g=\rho_g\), and \(v_t(B)\ge\alpha v_t(D-e_g)\) for every positive-mass pair \(\pi_{t,B},\pi_{u,D}\) and every \(g\) with \(D_g>0\) and \(v_t(g)>0\), at target \(\alpha=\frac{2\gamma}{\sqrt{5+4\gamma}-1}\).

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

A society is given by its support: the list of the \(\tau\ge1\) types with positive mass \(\mu_t\in\mathbb{Q}_{>0}\), with \(\sum_{t\in T}\mu_t=1\); \(\tau=|T|\) is the support size, not the number of possible types.
There are \(m\ge1\) indivisible good classes with per-agent supplies \(\rho_g\in\mathbb{Q}_{>0}\) and additive values \(v_t(g)\in\mathbb{Q}_{\ge0}\). Every type positively values some class, and every class is positively valued by some type. Let \(L\) be the total binary input length.
Define \(\gamma=\min_{g\in[m]}\frac{\min_{t:v_t(g)>0}v_t(g)}{\max_{t\in T}v_t(g)}\) and \(\alpha=\frac{2\gamma}{\sqrt{5+4\gamma}-1}\).
An allocation is an explicitly listed finite-support family of masses \(\pi_{t,B}\in\mathbb{Q}_{\ge0}\), with integer bundles \(B\in\mathbb{Z}_{\ge0}^m\), satisfying \(\sum_B\pi_{t,B}=\mu_t\) and \(\sum_{t,B}\pi_{t,B}B_g=\rho_g\) for every class \(g\).
It is \(\alpha\)-EFx if, for every ordered pair \((t,B),(u,D)\) of positive-mass entries, including entries of the same type, and every \(g\) with \(D_g>0\) and \(v_t(g)>0\), one has \(v_t(B)\ge\alpha v_t(D-e_g)\), where \(e_g\) is the unit vector for class \(g\).

Can an allocation with this \(\alpha\)-EFx guarantee always be computed in time polynomial in \(m,\tau,L\), or is achieving this guarantee NP-hard?

For explicitly listed discrete agents and individual goods with nonnegative additive values, the same \(\alpha\)-EFx guarantee is achievable in polynomial time ([Barman, Kar, and Pathak](https://arxiv.org/pdf/2312.13791)).
No result settling this exact mass-distribution 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 progress: a polynomial-time rescaling criterion

The general complexity question remains unresolved. I prove a polynomial-time sufficient condition for computing the requested $\alpha$-EFx allocation, with at most $\tau+m$ positive-mass entries.

The condition can hold when the original $\gamma$ is arbitrarily small. In particular, I prove that exact EFx is polynomial-time achievable whenever the bipartite graph of positive valuations is a forest.

All constructions and proofs below concern the stated mass-distribution model.

1. Parameters and the new sufficient condition

For a bundle $B$, write
$$ v_t(B)=\sum_{g=1}^m v_t(g)B_g. $$

The assumptions imply $0<\gamma\le1$. Rationalizing the expression for $\alpha$ gives
$$ \alpha= \frac{\gamma\bigl(1+\sqrt{5+4\gamma}\bigr)}{2(1+\gamma)}. $$
Thus $\alpha$ is the positive root of
$$ f(x)=(1+\gamma)x^2-\gamma x-\gamma^2. $$
The other root is negative. Since
$$ f(\gamma)=\gamma^2(\gamma-1)\le0, \qquad f(1)=1-\gamma^2\ge0, $$
we have
$$ \gamma\le\alpha\le1. $$

Theorem. Suppose there exist positive factors $a_t$ such that, for every class $g$ and every two types $t,u$ positively valuing $g$,
$$ a_t v_t(g)\ge \alpha a_u v_u(g). $$
Then an $\alpha$-EFx allocation can be computed in time polynomial in $m,\tau,L$. The output has at most $\tau+m$ positive-mass entries and polynomial binary encoding length.

Moreover, whether such factors exist can be decided in polynomial time, and suitable factors can be constructed when they exist.

The factors may be irrational. Nevertheless, the allocation produced by the theorem has rational masses and integer bundles.

The rest of the document proves this theorem and its forest consequence.

2. An exact graph test for rescaling

Fix $c\in(0,1]$. Eventually we use $c=\alpha$ or $c=1$.

Construct a directed multigraph on the types. For every class $g$ and every ordered pair of distinct types $u,t$ positively valuing $g$, include an edge from $u$ to $t$ with weight
$$ q_{u,t,g}=c\frac{v_u(g)}{v_t(g)}. $$

The desired rescaling inequalities are precisely
$$ a_t\ge q_{u,t,g}a_u $$
on every edge.

2.1 Cycle characterization

Lemma. Positive factors satisfying these inequalities exist if and only if every directed cycle has edge-weight product at most $1$.

Proof. If the factors exist, multiplying their inequalities around a cycle cancels all factors and gives
$$ 1\ge\prod_{e\text{ in the cycle}}q_e. $$

Conversely, suppose every directed cycle has product at most $1$. For each type $t$, define $a_t$ as the maximum product of edge weights over all directed paths ending at $t$, allowing any starting vertex and allowing the empty path, whose product is $1$.

This maximum exists: removing a repeated-vertex segment removes a cycle of product at most $1$, so it does not decrease the path product. Therefore it suffices to consider paths of length at most $\tau-1$.

For an edge $u\to t$, append that edge to a maximizing path ending at $u$. Removing cycles if necessary gives a path ending at $t$ whose product is at least $q_{u,t,g}a_u$. Hence
$$ a_t\ge q_{u,t,g}a_u. $$
All factors are positive because the empty paths are permitted. $\square$

2.2 Polynomial-time construction

Initialize
$$ a_t^{(0)}=1 $$
and perform $\tau$ rounds of updates
$$ a_t^{(k+1)} = \max\left\{ a_t^{(k)}, \max_{u,g:\,u\to t}q_{u,t,g}a_u^{(k)} \right\}. $$
Induction shows that $a_t^{(k)}$ is the largest product of a path of length at most $k$ ending at $t$.

If every cycle has product at most $1$, the preceding cycle-removal argument gives
$$ a_t^{(\tau)}=a_t^{(\tau-1)} $$
for every $t$. These stable values satisfy every edge inequality.

Conversely, if these two vectors agree, the update equations themselves show that the stable vector satisfies every edge inequality. Consequently the cycle condition holds.

Thus comparing rounds $\tau-1$ and $\tau$ decides feasibility.

For $c=\alpha$, all calculations take place in the real field
$$ K=\mathbb Q(\alpha). $$
This field has degree at most two. When $\alpha$ is irrational, its elements can be represented as $A+B\alpha$, with rational $A,B$, using
$$ \alpha^2=\frac{\gamma\alpha+\gamma^2}{1+\gamma} $$
for multiplication.

Exact comparisons are polynomial-time: after substituting the expression for $\alpha$, determining a sign reduces to determining the sign of
$$ P+Q\sqrt{5+4\gamma}, $$
where $P,Q$ are rational. When the two summands have opposite signs, comparing their squared magnitudes determines the sign, including equality.

There are at most $m\tau(\tau-1)$ edges. Every selected path product uses at most $\tau$ factors, so its rational coefficients have polynomial encoding length. The test and construction therefore run in polynomial time.

For $c=1$, all these operations are rational.

3. A mass algorithm using the rescaled values

Suppose the graph test succeeds for some $c\in\{\alpha,1\}$. Define
$$ \widehat v_t(g)=a_t v_t(g), \qquad w_g=\max_t\widehat v_t(g). $$
The rescaling inequalities imply that whenever $v_t(g)>0$,
$$ c w_g\le\widehat v_t(g)\le w_g. $$
The upper bound also holds when $v_t(g)=0$.

Define a bundle’s load by
$$ s(B)=\sum_g w_gB_g. $$

Process classes in nonincreasing order of $w_g$. Initially, type $t$ has the single entry $(t,\mu_t,0)$. Assign copies of a class only to types positively valuing that class. Consequently, throughout the algorithm,
$$ \widehat v_t(B)\ge c\,s(B) $$
for every positive-mass entry $(t,B)$.

Here is an exact batch procedure for one class. It accommodates irrational weights without discretizing them.

3.1 Raising eligible loads

Consider the current class $g$, with weight $w=w_g$ and supply $C=\rho_g$.

Index the currently eligible entries by $i$. Write their masses, bundles, and loads as
$$ p_i,\qquad B_i,\qquad \ell_i=s(B_i). $$
Their total mass is
$$ E=\sum_i p_i=\sum_{t:v_t(g)>0}\mu_t>0. $$

For a real threshold $x$, define
$$ k_i(x)= \max\left\{0,\left\lceil\frac{x-\ell_i}{w}\right\rceil\right\}, \qquad F(x)=\sum_i p_i k_i(x). $$
Thus $k_i(x)$ is the least nonnegative integer number of copies needed to raise entry $i$ to load at least $x$. The quantity $F(x)$ is the required aggregate supply.

We will find a threshold $\lambda$ for which
$$ F(\lambda)\le C< F(\lambda)+ \sum_{i:\,\ell_i+k_i(\lambda)w=\lambda}p_i. $$

3.2 Finding the threshold in polynomially many operations

Put
$$ a=\min_i\ell_i, \qquad R=\max_i\ell_i, \qquad K_0= \left\lceil\frac{R-a}{w}\right\rceil+ \left\lceil\frac CE\right\rceil+1. $$
We have $F(a)=0$. Also,
$$ a+K_0w\ge R+w\left(\left\lceil\frac CE\right\rceil+1\right). $$
At this latter threshold, every eligible entry needs at least $\lceil C/E\rceil+1$ copies. Hence
$$ F(a+K_0w)>C. $$

Binary search finds the largest integer $k$ satisfying
$$ F(a+kw)\le C. $$
Let $x=a+kw$. Then
$$ F(x)\le C<F(x+w). $$

The function $F$ increases immediately to the right of thresholds of the form
$$ \ell_i+n w, \qquad n\in\mathbb Z_{\ge0}. $$
Each eligible entry contributes at most one such threshold in the interval $[x,x+w)$. Its candidate is
$$ d_i= \ell_i+ w\max\left\{0,\left\lceil\frac{x-\ell_i}{w}\right\rceil\right\}; $$
discard candidates outside that interval.

Sort these candidates. At a candidate $\lambda$, define
$$ J(\lambda)= \{i:\ell_i+k_i(\lambda)w=\lambda\}. $$
Immediately to the right of $\lambda$, $F$ increases by
$$ \sum_{i\in J(\lambda)}p_i. $$
Because $F(x)\le C<F(x+w)$, scanning the candidates finds one satisfying
$$ F(\lambda)\le C< F(\lambda)+\sum_{i\in J(\lambda)}p_i. $$

All thresholds lie in $K$, and their comparisons and ceilings can be computed exactly. The bit-complexity justification appears in Section 4.

3.3 Allocating exactly the supply

Give entry $i$ exactly $k_i(\lambda)$ copies. The remaining supply is
$$ \delta=C-F(\lambda), \qquad 0\le\delta<\sum_{i\in J(\lambda)}p_i. $$

Give one additional copy to total mass $\delta$ from entries in $J(\lambda)$. Taking entries in a fixed order requires whole entries followed by at most one partially selected entry. Split that entry if necessary.

This uses exactly $C$ copies in aggregate, preserves each type’s mass, and introduces at most one additional positive-mass entry.

The construction has two properties:

$$ s(D)-w\le\lambda. $$

For the second property, an entry receiving ordinary copies had load strictly below $\lambda$ before its last ordinary copy. An additional copy is given only to an entry whose ordinary post-allocation load equals $\lambda$.

4. Fairness and polynomial running time

4.1 Fairness invariant

Lemma. After every stage, the allocation is $c$-EFx under $\widehat v$.

Proof. Initially every bundle is empty, so the assertion holds. Assume it holds before processing class $g$.

Consider resulting entries $(t,B)$ and $(u,D)$.

If $\widehat v_t(g)=0$, additions of $g$ change neither relevant value and create no new positively valued removal condition. Previous fairness applies.

If $\widehat v_t(g)>0$ but $D$ gained no copies, the compared value is unchanged while the observer’s own value cannot decrease. Previous fairness again applies.

It remains to consider $\widehat v_t(g)>0$ and a bundle $D$ that gained copies. The observer is eligible, so its resulting load is at least $\lambda$. Every class $h$ present in $D$ has
$$ w_h\ge w_g=w, $$
because classes are processed in nonincreasing order of weight. Therefore, for every required removal $h$,
$$ \widehat v_t(D-e_h) \le s(D)-w_h \le s(D)-w \le\lambda. $$
Meanwhile,
$$ \widehat v_t(B) \ge c\,s(B) \ge c\lambda \ge c\,\widehat v_t(D-e_h). $$

These cases cover every required comparison. Each new entry descends from an earlier entry, so the same argument covers splits, same-type comparisons, and self-comparisons. $\square$

Since $\widehat v_t=a_tv_t$ with $a_t>0$, dividing an observer’s inequality by $a_t$ proves exactly the same $c$-EFx inequality under the original valuations.

In particular, using $c=\alpha$ proves the requested guarantee.

4.2 Support and rational masses

There is at most one split per class. Starting with $\tau$ entries, the algorithm therefore produces at most
$$ \tau+m $$
positive-mass entries.

Let $Q$ be the product of the denominators of the input masses and supplies. Its binary length is at most their total encoding length.

Every mass throughout the algorithm is an integer multiple of $1/Q$. Indeed, ordinary copy counts are integers, so
$$ \delta=\rho_g-\sum_i p_i k_i(\lambda) $$
is such a multiple. Whole-entry selections and the possible split preserve the same property.

Every mass lies between $0$ and $1$. Thus every output mass has polynomial binary encoding length, regardless of the auxiliary irrational thresholds.

4.3 Loads, bundle coordinates, and arithmetic

Let $R_j$ denote the maximum load after stage $j$. The search bound and the property $s(D)\le\lambda+w$ imply
$$ R_j \le R_{j-1} + w_{g_j} \left( \left\lceil\frac{\rho_{g_j}}{E_{g_j}}\right\rceil+3 \right). $$
Indeed, the selected threshold is strictly below $a+K_0w$, and
$$ a+K_0w < R+w\left(\left\lceil\frac CE\right\rceil+2\right). $$

Consequently all loads are bounded by
$$ \sum_g w_g \left( \left\lceil\frac{\rho_g}{E_g}\right\rceil+3 \right). $$

For the graph-constructed factors, each $a_t$ is at least $1$ and is a product along a path of length at most $\tau-1$. Every positive input rational is between $2^{-L}$ and $2^L$. Since $c\le1$, every edge weight is at most $2^{2L}$. Thus
$$ 1\le a_t\le 2^{2\tau L}, \qquad 2^{-L}\le w_g\le 2^{(2\tau+1)L}. $$
Also $E_g\ge2^{-L}$ and $\rho_g\le2^L$. The load bound is therefore at most $2^{P(m,\tau,L)}$ for a polynomial $P$.

Because every $w_g\ge2^{-L}$, the same conclusion bounds every bundle coordinate. Its binary length is polynomial.

For exact arithmetic, retain the fixed field representations of the $w_g$. A load can always be recomputed as
$$ s(B)=\sum_g w_gB_g. $$
This is a sum of at most $m$ fixed field elements multiplied by integers of polynomial binary length, so its rational coefficients have polynomial encoding length. Search thresholds have the same property.

Division by $w$ is exact in the degree-two field. To compute a ceiling, first bracket the quotient between integers of polynomial binary length using the magnitude bounds, then binary-search with exact comparisons.

Each stage uses a binary search with polynomially many iterations and a sort of at most $\tau+m$ candidates. There are $m$ stages. All field coefficients, integer counts, and rational masses have polynomial encoding length.

This completes the proof of the theorem.

5. A new exact-EFx case: forests of positive valuations

Define the positive-valuation incidence graph to be the bipartite graph with vertex sets $T$ and $[m]$, where $t$ is adjacent to $g$ exactly when $v_t(g)>0$.

Corollary. If this graph is a forest, an exact EFx allocation can be computed in polynomial time.

Proof. In each connected component, root the tree at a type and give that type factor $a_t=1$.

Traverse the tree. From an already assigned type $t$ to an unassigned neighboring class $g$, set
$$ w_g=a_tv_t(g). $$
From an already assigned class $g$ to an unassigned neighboring type $u$, set
$$ a_u=\frac{w_g}{v_u(g)}. $$

A forest gives each nonroot vertex a unique parent, so there are no conflicting assignments. Every quantity is positive. Every positive-valuation edge satisfies
$$ a_tv_t(g)=w_g. $$

Thus, for each class, all its positive rescaled values coincide. The rescaling inequalities hold with $c=1$. The graph test consequently succeeds at $c=1$, and the preceding mass algorithm produces exact EFx. $\square$

This case extends beyond types whose valuation profiles are proportional.

For example, take $H\in\mathbb Q$ with $H\ge1$ and valuations
$$ \begin{array}{c|ccc} & x & y & z\\ \hline a & 1 & 1 & 0\\ b & H & 0 & 1 \end{array} $$
with arbitrary positive rational type masses summing to $1$ and arbitrary positive rational supplies.

The incidence graph is the path
$$ y-a-x-b-z. $$
Here $\gamma=1/H$, which can be arbitrarily small. Factors $a_a=H$ and $a_b=1$ make the positive values classwise identical. Exact EFx is therefore polynomial-time achievable for every such instance.

6. The criterion does not settle all inputs

The rescaling condition is sufficient, but it is not necessary for an $\alpha$-EFx allocation to be computable.

Consider two types, each of mass $1/2$, and three classes, each of supply $1/2$:
$$ \begin{array}{c|ccc} & x & y & z\\ \hline a & 1 & 3 & 2\\ b & 4 & 1 & 2 \end{array} $$

Here $\gamma=1/4$. Rescaling to range at least $c$ would require, using class $x$,
$$ a_a\ge4c\,a_b, $$
and, using class $y$,
$$ a_b\ge3c\,a_a. $$
Multiplying gives
$$ 1\ge12c^2. $$
Thus no rescaling can achieve $c>1/\sqrt{12}$.

For this input,
$$ f(1/3)=-1/144<0, $$
so $\alpha>1/3$. Since $1/\sqrt{12}<1/3$, the rescaling test fails at $c=\alpha$.

Nevertheless, this instance has the explicit exact EFx allocation
$$ \pi_{a,(0,1,1)}=\frac12, \qquad \pi_{b,(1,0,0)}=\frac12. $$
The supply and mass equations hold directly. Type $a$ compares its bundle with a singleton, whose value after the required removal is zero. Type $b$ has own value $4$; removing either good from type $a$’s bundle leaves value $1$ or $2$. Self-comparisons hold by nonnegativity.

Therefore an amplified cycle in the rescaling graph is an obstruction to this particular method, not an obstruction to the requested allocation.

7. What remains open

The new results give:

They do not provide a polynomial-time construction for arbitrary inputs failing the rescaling test, and they do not establish hardness of constructing an allocation.

The [discrete-agent theorem](https://arxiv.org/pdf/2312.13791) supplies the guarantee for explicitly listed agents and goods. The unresolved issue remains how to achieve it efficiently under the binary-encoded masses and supplies of the present problem.

⟨structured verdict parsed — rendered above⟩

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

Assessment: valid partial progress. The output establishes its rescaling criterion and the forest corollary. I found no substantive error in those arguments. It does not settle the general polynomial-time-versus-hardness question in USER_TASK, and it explicitly acknowledges this limitation.

The distinction matters: failure of the rescaling test is only failure of this sufficient condition. Section 6 correctly demonstrates that it cannot be treated as an obstruction to the requested allocation.

Step-by-step verification

Every class has a positive valuation, so each ratio defining $\gamma$ is well-defined and belongs to $(0,1]$. Thus $0<\gamma\le1$.

The rationalization of $\alpha$ and its quadratic equation are correct:
$$ (1+\gamma)\alpha^2-\gamma\alpha-\gamma^2=0. $$
The other root is negative. The displayed evaluations
$$ f(\gamma)=\gamma^2(\gamma-1), \qquad f(1)=1-\gamma^2 $$
correctly imply $\gamma\le\alpha\le1$, including the endpoint $\gamma=1$.

For distinct types positively valuing the same class, the edge inequality is exactly the theorem’s required inequality. Omitting equal-type edges loses nothing because $c\le1$.

Necessity follows by multiplying positive-factor inequalities around a cycle. For sufficiency, the cycle-removal argument is valid: deleting a closed segment with positive product at most $1$ cannot decrease the remaining product. Consequently the maximum is attained among finitely many paths of length at most $\tau-1$.

Appending an edge to a maximizing path and then deleting cycles proves the required inequality for the resulting factors. Empty paths ensure that every factor is positive. Disconnected components and isolated vertices in the directed type graph cause no problem.

The update recurrence computes maximum products over walks of bounded length. Agreement between rounds $\tau-1$ and $\tau$ implies every edge inequality directly; feasibility implies that agreement by cycle removal. Thus the test has both required directions.

The arithmetic discussion correctly handles $c=\alpha$ and $c=1$. In the irrational case, the quadratic relation gives exact arithmetic in a fixed degree-two field. The stated sign test handles opposite-sign summands and equality correctly.

Each selected product contains at most $\tau$ edge weights. Its rational coefficients therefore have polynomial binary length. The polynomial edge count and number of rounds establish the claimed polynomial running time. The case $\tau=1$ is also covered: there are no edges, and the initial vector is already stable.

The definition of $k_i(x)$ gives exactly the least nonnegative integer number of copies needed to reach load at least $x$. Eligibility depends only on type, so its total mass remains
$$ E=\sum_{t:v_t(g)>0}\mu_t>0. $$

The upper search bound is valid. At $a+K_0w$, every eligible entry requires at least $\lceil C/E\rceil+1$ copies, so the aggregate requirement exceeds $C$.

Binary search consequently produces
$$ F(x)\le C<F(x+w). $$
For each entry, the candidate formula identifies its first threshold at or above $x$. There is at most one candidate from that entry in $[x,x+w)$. The use of this half-open interval is correct: a jump at $x+w$ occurs immediately to its right and is not included in $F(x+w)$.

At a candidate $\lambda$, the stated jump size is correct. Grouping equal candidates through $J(\lambda)$ therefore finds the required residual-capacity threshold.

After the ordinary copies, the residual satisfies
$$ 0\le\delta<\sum_{i\in J(\lambda)}p_i. $$
Selecting whole entries followed by at most one partial entry realizes exactly this mass. The procedure therefore consumes exactly the current supply.

Splitting preserves type mass and all previously allocated supplies because both descendants retain the parent’s previous bundle coordinates.

Both asserted load properties hold. Ordinary-copy recipients were strictly below $\lambda$ before their final ordinary copy. Additional-copy recipients have ordinary post-allocation load exactly $\lambda$. Hence every recipient satisfies
$$ s(D)-w\le\lambda, $$
while every eligible resulting entry has load at least $\lambda$. The case $\delta=0$ requires no additional selection or split and is covered.

Assigning classes only to types positively valuing them justifies
$$ \widehat v_t(B)\ge c\,s(B) $$
for every resulting entry.

The induction’s cases exhaust the required comparisons:

$$ \widehat v_t(D-e_h) \le s(D)-w_h \le s(D)-w \le\lambda $$
is valid for every required removal.

These inequalities establish $c$-EFx. Descendant entries inherit the necessary previous comparisons, so splitting, same-type comparisons, and self-comparisons are covered. Dividing by the observer’s positive factor correctly transfers the guarantee to the original valuations.

At most one split per class gives at most $\tau+m$ positive-mass entries.

The denominator argument is valid: all masses remain integer multiples of $1/Q$, because supplies and current masses have that property and copy counts are integers. Masses remain in $[0,1]$, giving polynomial encoding length.

The load recurrence follows from the threshold bound and the recipient-load property. Its additive constant $3$ is justified by the displayed inequalities.

The bounds on factors, weights, eligible masses, and supplies yield polynomial binary lengths for loads and bundle coordinates. Large numerical copy counts therefore do not imply large output encoding length.

Recomputing loads from fixed field representations avoids uncontrolled arithmetic-expression growth. Exact division and ceiling computation in the fixed degree field have polynomial bit complexity under the stated bounds. The searches and sorts consequently use polynomially many polynomial-cost operations.

Every connected component contains a type, since the task excludes isolated incidence vertices. Rooting at a type is therefore permitted.

Unique parents in a tree prevent conflicting assignments. The traversal assigns positive factors and establishes
$$ a_tv_t(g)=w_g $$
on every positive-valuation edge. Thus the rescaling condition holds with $c=1$, and the preceding algorithm supplies exact EFx.

The example’s incidence graph is indeed the stated path. Its parameter is $\gamma=1/H$, and the displayed factors make positive values coincide classwise.

The two necessary rescaling inequalities imply
$$ 1\ge12c^2. $$
The computation
$$ f(1/3)=-1/144 $$
is correct for $\gamma=1/4$, so $\alpha>1/3>1/\sqrt{12}$. The rescaling test therefore fails at the requested factor.

The proposed allocation satisfies all mass and supply equations. Its cross-type removal comparisons are exactly those described, and self-comparisons follow from nonnegative values. It is exact EFx.

The cited [Barman–Kar–Pathak paper](https://arxiv.org/pdf/2312.13791) states the displayed guarantee for explicitly listed discrete agents and goods. The partial construction does not depend on transferring that theorem to the mass model.

The output provides neither an algorithm covering arbitrary inputs that fail its criterion nor a hardness reduction. Accordingly, its proved special cases cannot answer the general question.

Issue and minimum required follow-up

Major — incomplete resolution of USER_TASK. Sections 6–7 leave the unrestricted problem unresolved. This is a scope limitation expressly acknowledged by the prover, rather than an error in its conditional theorem.

No clarification is needed to verify the conditional result. To complete the assignment, additional mathematics is required: either an unconditional polynomial-time construction for the stated model or a rigorously specified hardness result for achieving the requested guarantee. Failure of the rescaling condition alone supplies neither.

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