Answer: —
Theorem 5.9 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateSuppose that the valuations are $(2, \infty)$-bounded, and let $\alloc^*$ be the allocation returned by the Algorithm \ref{alg1}. Then, $\alloc^*$ is a $(\nicefrac{1}{\sqrt{2}})$-$\efx$ allocation.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given finite agent types \(T\) with masses \(\mu_t\ge0\) and \(\sum_t\mu_t=1\), finite good types \(E\) with per-capita supplies \(s_e\ge0\), additive values \(v_t(e)\ge0\), and \(|\{t:v_t(e)>0\}|\le2\) for every \(e\), output a complete mass allocation \(\lambda_{t,B}\ge0\) over integral multisets \(B\) satisfying \(\sum_B\lambda_{t,B}=\mu_t\) and \(\sum_{t,B}\lambda_{t,B}b_e(B)=s_e\), such that whenever \(\lambda_{t,B}>0\), \(\lambda_{u,C}>0\), and \(b_e(C)>0\), \(v_t(B)\ge \frac{1}{\sqrt{2}}v_t(C\setminus\{e\})\).
A society is given by its support: a nonempty list \(T\) of \(\tau\) types with positive binary rational masses \(\mu_t\), summing to \(1\). Here \(\tau\) is the support size, not the number of possible types.
There are \(m=|E|\) good types, with nonnegative binary rational per-capita supplies \(s_e\) and additive values \(v_t(e)\). Each good type has positive value for at most two supported agent types; there is no bound on how many good types a pair values. Let \(L\) be the total input bit length.
A bundle is an integral multiset \(B\), with multiplicities \(b_e(B)\in\mathbb Z_{\geq0}\) and value \(v_t(B)=\sum_{e\in E}b_e(B)v_t(e)\); empty bundles are allowed and multiplicities have no imposed upper bound.
A complete mass allocation is a finitely supported family of nonnegative rational masses \(\lambda_{t,B}\) satisfying \(\sum_B\lambda_{t,B}=\mu_t\) and \(\sum_{t,B}\lambda_{t,B}b_e(B)=s_e\).
It is \(1/\sqrt{2}\)-EFX if, for every \(t,u,B,C,e\) with \(\lambda_{t,B}>0\), \(\lambda_{u,C}>0\), and \(b_e(C)>0\), one has \(v_t(B)\geq v_t(C\setminus\{e\})/\sqrt{2}\). Removal deletes exactly one copy, including when its value to \(t\) is zero; comparisons include \(t=u\).
Does every such instance admit a complete \(1/\sqrt{2}\)-EFX mass allocation, and can such an allocation always be constructed in time polynomial in \(m,\tau,L\)?
For finitely many individual agents and goods, additive valuations with each good relevant to at most two agents admit a complete \(1/\sqrt{2}\)-EFX allocation via a terminating algorithm; no polynomial running-time bound is stated. [Source](https://arxiv.org/html/2506.09288v2).
No result settling this precise mass-allocation guarantee was located in the literature search.
I do not settle the unrestricted question. I prove two additional sufficient conditions under which the requested allocation can be constructed in polynomial time:
Both results allow unrestricted support size. In fact, their existence and construction arguments do not require the restriction to two relevant types per good. Their allocations can be compressed to at most $\tau+m$ supported type–bundle pairs.
I use the intended goods interpretation: all item values $v_t(e)$ are nonnegative binary rationals.
For an integral bundle $B$, write
$$
|B|=\sum_e b_e(B).
$$
A complete mass allocation is $\alpha$-EFX if every required comparison satisfies
$$
v_t(B)\geq \alpha\,v_t(C\setminus\{e\}).
$$
All proofs below include comparisons within a type and removal of copies worth zero to the comparing type.
Goods of zero supply can be ignored: completeness and nonnegativity imply that they occur in no positive-mass bundle. Among the remaining goods, let
$$
P=\{e:s_e>0\text{ and }v_t(e)>0\text{ for some }t\},
$$
and let $Z$ consist of the goods with positive supply that everybody values at zero.
A good is relevant to a type if that type values it positively.
Lemma 1. For any nonnegative rational vector $w=(w_1,\ldots,w_p)$, there is a polynomial-time constructible rational distribution over at most $p+1$ integral vectors $b$ such that
$$
\mathbb E[b_j]=w_j
$$
and every supported vector satisfies
$$
\sum_j b_j\in
\left\{
\left\lfloor\sum_jw_j\right\rfloor,
\left\lceil\sum_jw_j\right\rceil
\right\}.
$$
All multiplicities and distribution masses have polynomial encoding length.
Proof. Put
$$
c_0=0,\qquad c_j=\sum_{i=1}^j w_i,\qquad d=c_p.
$$
For $\theta\in[0,1)$, define
$$
b_j(\theta)
=
\#\{z\in\mathbb Z:c_{j-1}\leq z+\theta<c_j\}.
$$
Then
$$
\sum_j b_j(\theta)
=
\#\{z\in\mathbb Z:0\leq z+\theta<d\},
$$
which is either $\lfloor d\rfloor$ or $\lceil d\rceil$.
Furthermore,
$$
\int_0^1b_j(\theta)\,d\theta
=
\sum_{z\in\mathbb Z}
\operatorname{length}
\bigl([c_{j-1},c_j)\cap[z,z+1)\bigr)
=
c_j-c_{j-1}
=
w_j.
$$
Only finitely many summands are nonzero.
Partition $[0,1)$ at the distinct fractional parts of $c_1,\ldots,c_p$. On each resulting open interval, all $b_j(\theta)$ are constant. Give that vector mass equal to the interval length. Values at interval endpoints have measure zero and do not affect the distribution.
There are at most $p+1$ intervals. Their endpoints are rational, and the vectors can be computed using integer floor and ceiling operations; no copies are enumerated. Their encoding lengths are polynomial in the input length. If $p=0$, use the empty vector with mass $1$. $\square$
When $d$ is nonintegral, bundles of cardinality $\lfloor d\rfloor$ occur with mass $1-\{d\}>0$. When $d$ is integral, every bundle has cardinality $d$.
Lemma 2. Suppose a complete $\alpha$-EFX mass allocation is already given using polynomially many supported pairs, with polynomially encoded multiplicities. It can be replaced in polynomial time by one using at most $\tau+m$ pairs, still with polynomial encoding length.
Proof. For each existing pair $(t,B)$, form the integer column
$$
a_{t,B}
=
\bigl(\mathbf 1_{\{t=u\}}\bigr)_{u\in T}
\mathbin{\oplus}
\bigl(b_e(B)\bigr)_{e\in E}.
$$
The existing allocation makes the polytope
$$
\sum_{t,B}x_{t,B}a_{t,B}=(\mu,s),
\qquad x_{t,B}\geq0
$$
nonempty. The type equations imply $\sum_{t,B}x_{t,B}=1$, so the polytope is bounded.
At a vertex, its positive columns must be linearly independent. Otherwise, a nonzero dependence would permit a sufficiently small perturbation in both directions, preserving the equations and nonnegativity, contradicting extremality. Thus at most $\tau+m$ coordinates are positive.
For completeness, let $d=\tau+m$, let
$$
H=\max\bigl(\{1\}\cup\{b_e(B):\text{existing pairs and goods}\}\bigr),
$$
and let $D$ clear the denominators of $(\mu,s)$. If a vertex has $r$ positive coordinates, choose $r$ independent rows of its positive-column matrix. Cramer’s rule gives a common denominator bounded by
$$
D\,r!\,H^r\leq D\,d!\,H^d.
$$
The logarithm of this bound is polynomial. Each mass lies in $[0,1]$, so its numerator also has polynomial encoding length.
A basic feasible solution can be found by rational linear programming in polynomial time. Only existing pairs survive; hence no new EFX comparison is introduced. $\square$
The next lemma concerns quantities of goods, without using their positive values.
Lemma 3. One can construct in polynomial time nonnegative rational quantities $x_{t,e}$ satisfying
$$
\sum_t x_{t,e}=s_e
\quad(e\in P),
\qquad
x_{t,e}=0\quad\text{if }v_t(e)=0,
$$
such that, with
$$
d_t=\frac{\sum_{e\in P}x_{t,e}}{\mu_t},
$$
the following implication holds:
$$
x_{u,e}>0,\quad v_t(e)>0
\quad\Longrightarrow\quad
d_u\leq d_t.
$$
Thus a good allocated to a type is never allocated to a type with a larger average item count than another type that values it.
Consider a residual set $U$ of types and a residual set of goods, each relevant to at least one type in $U$. For $A\subseteq U$, let $N(A)$ be the residual goods relevant to some type in $A$, and put
$$
f(A)=\sum_{e\in N(A)}s_e,
\qquad
\mu(A)=\sum_{t\in A}\mu_t.
$$
For prescribed nonnegative demands $h_t$, a relevant assignment meeting every demand exists if and only if
$$
\sum_{t\in A}h_t\leq f(A)
\qquad\text{for every }A\subseteq U.
$$
Necessity follows because types in $A$ can receive goods only from $N(A)$.
For sufficiency, use a flow network with arcs from the source to each good of capacity $s_e$, from each good to its relevant types, and from each type to the sink of capacity $h_t$. Give the good-to-type arcs capacity larger than the total supply plus the total demand.
Let $D_h=\sum_t h_t$. A minimum cut has capacity at most $D_h$, so it cannot cross a good-to-type arc. If $A$ is its set of types on the sink side, the smallest such cut has capacity
$$
f(A)+\sum_{t\notin A}h_t.
$$
The displayed demand inequalities therefore ensure that every cut has capacity at least $D_h$. By the max-flow/min-cut theorem, a flow meeting every demand exists.
Any unused supply can then be assigned to an arbitrary relevant type. This produces a complete relevant assignment with loads at least the prescribed demands.
At a residual instance, maximize $\lambda$ subject to
$$
\sum_t x_{t,e}=s_e,\qquad x_{t,e}\geq0,
$$
using only relevant incidences, and
$$
\sum_e x_{t,e}\geq\mu_t\lambda
\qquad(t\in U).
$$
This is a feasible, bounded rational linear program. By the demand criterion, its optimum is
$$
\lambda
=
\min_{\varnothing\ne A\subseteq U}
\frac{f(A)}{\mu(A)}.
$$
Call $A$ tight if $f(A)=\lambda\mu(A)$. Let $A_*$ be the union of all nonempty tight sets.
The set $A_*$ is itself tight. Indeed, weighted neighborhood supply is submodular:
$$
f(A\cup B)+f(A\cap B)\leq f(A)+f(B).
$$
For tight $A,B$, the right-hand side equals
$$
\lambda\mu(A\cup B)+\lambda\mu(A\cap B).
$$
Each term on the left is at least its corresponding term on this last expression. Consequently both inequalities are equalities, and $A\cup B$ is tight. Repeated unions prove the assertion.
In every optimal assignment, every type in $A_*$ has average count exactly $\lambda$. To see this, sum its lower-bound constraints:
$$
\sum_{t\in A_*}\sum_e x_{t,e}
\geq
\lambda\mu(A_*)
=
f(A_*).
$$
The left-hand side cannot exceed $f(A_*)$. Hence equality holds, every individual lower bound is tight, and all supply in $N(A_*)$ is assigned to types in $A_*$.
Conversely, a type outside $A_*$ is not forced to have average count $\lambda$. If $t\notin A_*$, then every subset $A$ containing $t$ has positive slack
$$
f(A)-\lambda\mu(A)>0.
$$
There are finitely many such subsets, so choose $\varepsilon>0$ no larger than their minimum slack. The demands
$$
h_u=\lambda\mu_u+\varepsilon\mathbf 1_{\{u=t\}}
$$
satisfy the demand criterion. A complete relevant assignment meeting them gives type $t$ average count strictly greater than $\lambda$.
These observations give a polynomial way to identify $A_*$ without enumerating subsets. On the optimal face, separately maximize
$$
\frac{\sum_e x_{t,e}}{\mu_t}
$$
for each $t\in U$. Type $t$ belongs to $A_*$ exactly when this maximum equals $\lambda$.
Take any optimal assignment. Retain its quantities for types in $A_*$, and remove $A_*$ and all goods in $N(A_*)$. Recurse.
At least one type is removed per round. Remaining goods still have a relevant remaining type. Moreover, the residual part of the current optimal assignment gives every remaining type average count at least $\lambda$. Therefore successive levels are nondecreasing.
If $x_{u,e}>0$ was retained at level $\lambda$, any type $t$ valuing $e$ was still present at that round: otherwise $e$ would already have been removed. Type $t$ is finalized at the same or a later level. Consequently
$$
d_u=\lambda\leq d_t.
$$
Every good is removed once and all its supply is retained, proving completeness.
There are at most $\tau$ rounds and at most $\tau$ additional linear programs per round. Each level is a ratio of a sum of original supplies to a sum of original type masses, so it has polynomial binary length. The linear programs have at most $m\tau$ variables and polynomially many constraints, all of polynomial encoding length. Exact rational linear programming therefore gives polynomial running time and polynomially encoded quantities.
If $P$ is empty, the same construction gives $x=0$ and $d_t=0$ for all types. $\square$
For a type that values some good in $P$, define
$$
a_t=\min_{\substack{e\in P\\v_t(e)>0}}v_t(e),
\qquad
b_t=\max_{e\in P}v_t(e).
$$
Define
$$
R=
\max\left(
\{1\}\cup
\left\{
\frac{b_t}{a_t}:t\text{ values some good in }P
\right\}
\right).
$$
Theorem A. Every instance admits a polynomial-time constructible complete $1/R$-EFX mass allocation. In particular:
The output can have at most $\tau+m$ supported pairs.
Apply Lemma 3. For each type $t$, apply Lemma 1 to the normalized quantities
$$
w_{t,e}=\frac{x_{t,e}}{\mu_t}.
$$
Multiply the resulting distribution masses by $\mu_t$.
This allocates all goods in $P$. Every type receives only relevant goods, and each of its supported bundles satisfies
$$
|B|\in\{\lfloor d_t\rfloor,\lceil d_t\rceil\}.
$$
Initially there are polynomially many supported pairs. Their multiplicities have polynomial binary length because
$$
d_t\leq \frac{\sum_{e\in P}s_e}{\mu_t}.
$$
Choose a type $u$ minimizing $d_u$. Its rounded distribution has a positive-mass cohort whose bundle has cardinality
$$
k=\lfloor d_u\rfloor.
$$
Let the cohort mass be $q>0$.
Apply Lemma 1 to the vector $(s_e/q)_{e\in Z}$ and append those null bundles to this cohort. This consumes all null supplies and preserves the cohort’s positive-good core.
The resulting masses and multiplicities have polynomial encoding length: $q$ already has polynomial encoding length, and Lemma 1 performs only polynomially many rational operations.
For every type $t$,
$$
k\leq\lfloor d_t\rfloor.
$$
Consider any supported source bundle $B$ assigned to type $t$. If $t$ values no good in $P$, it values every allocated bundle at zero, and all its comparisons hold.
Otherwise, let $B^+$ denote its positive-good core. Since all its core goods are relevant to $t$,
$$
v_t(B)=v_t(B^+)
\geq a_t|B^+|
\geq a_t\lfloor d_t\rfloor.
$$
Consider a target bundle $C$ assigned to type $u$, and a permitted deletion.
First suppose the deleted copy belongs to its core $C^+$. If $t$ values no core good, the deletion value is zero. Otherwise, some $f$ occurring in $C^+$ satisfies
$$
v_t(f)>0,\qquad x_{u,f}>0.
$$
Lemma 3 gives $d_u\leq d_t$, and therefore
$$
|C^+|
\leq\lceil d_u\rceil
\leq\lfloor d_t\rfloor+1.
$$
After removing any core copy, at most $|C^+|-1$ relevant copies remain for type $t$. This holds also when the removed copy has value zero to $t$: that copy itself demonstrates that the original core contained at most $|C^+|-1$ relevant copies. Thus
$$
v_t(C\setminus\{e\})
\leq b_t(|C^+|-1)
\leq b_t\lfloor d_t\rfloor
\leq R\,v_t(B).
$$
Now suppose the deleted copy is globally valueless. Such copies occur only on the selected core of cardinality $k$. Consequently,
$$
v_t(C\setminus\{e\})
=
v_t(C^+)
\leq b_t k
\leq b_t\lfloor d_t\rfloor
\leq R\,v_t(B).
$$
These arguments quantify over all source and target pairs, including $t=u$. They prove complete $1/R$-EFX.
The construction has polynomial support and encoding length. Lemma 2 reduces its support to at most $\tau+m$. $\square$
The bound on $R$ is a genuine limitation of this construction.
For example, take one type of mass $1$, with goods $a,b$ satisfying
$$
s_a=1,\qquad s_b=\frac12,\qquad v(a)=1,\qquad v(b)=M>\sqrt{2}.
$$
The cardinality-rounding construction, ordering $a$ before $b$, gives mass $1/2$ to each of
$$
\{a\},\qquad \{a,b\}.
$$
Deleting $a$ from the second bundle leaves value $M$, whereas the first bundle has value $1$. Hence this allocation is not $1/\sqrt{2}$-EFX.
This is not a counterexample to existence. The same instance has an exact EFX allocation giving mass $1/2$ to each of
$$
\{b\},\qquad \{a,a\}.
$$
Indeed, the only nonzero deletion value is $1$, and both bundles have value at least $1$.
Thus balancing counts alone does not resolve instances with unrestricted variation in positive values.
The next construction uses the one-valuation method from the notes; the proof is included here.
Lemma 4. Given positive rational item weights $a_e$ and nonnegative rational supplies $r_e$ for a population of mass $1$, one can construct in polynomial time a complete exact EFX distribution for these weights, using at most one more cohort than the number of goods.
Let
$$
W=\sum_e r_ea_e,\qquad a_{\max}=\max_e a_e,
$$
and let $\ell$ be its minimum supported bundle weight. Then
$$
W-a_{\max}\leq\ell\leq W.
$$
If there are no goods, take the empty bundle and set $W=a_{\max}=\ell=0$.
Scale weights to positive integers and process goods in nonincreasing weight order.
Maintain cohorts of masses $q_i>0$, bundles $B_i$, and integer loads $l_i$. Initially there is one empty cohort of mass $1$.
For the next good, with integer weight $a$ and supply $r$, define
$$
n_i(h)=
\max\left\{0,\left\lceil\frac{h-l_i}{a}\right\rceil\right\},
\qquad
F(h)=\sum_i q_i n_i(h)
$$
for nonnegative integers $h$.
Choose the largest $h$ satisfying $F(h)\leq r$, and give cohort $i$ exactly $n_i(h)$ copies per member. Every resulting load is at least $h$.
Call a cohort active when its resulting load is exactly $h$. Then
$$
F(h+1)-F(h)=\sum_{\text{active }i}q_i.
$$
Indeed, raising an integer threshold from $h$ to $h+1$ requires an additional copy exactly for cohorts currently at load $h$.
Writing $\delta=r-F(h)$, maximality gives
$$
0\leq\delta<\sum_{\text{active }i}q_i.
$$
Give one further copy to active mass $\delta$, taking whole cohorts and splitting at most one cohort. The exact supply $r$ is consumed, and the number of cohorts increases by at most one.
Inductively maintain
$$
\operatorname{weight}(C\setminus\{e\})
\leq
\min_i l_i
$$
for every supported target bundle and every copy in it.
An unchanged bundle retains this property because the minimum load cannot decrease.
For an updated bundle of final load $L$:
Every old copy has weight at least $a$, by the processing order. Therefore deleting any copy from an updated bundle leaves weight at most
$$
L-a\leq h\leq\text{final minimum load}.
$$
This proves the invariant and exact EFX.
For every nonempty supported bundle of load $L$, deleting one of its copies also gives
$$
L\leq \ell+a_{\max}.
$$
Empty bundles satisfy this bound as well. Taking averages yields
$$
W\leq\ell+a_{\max}.
$$
The opposite bound $\ell\leq W$ follows because a minimum is at most an average.
A strictly infeasible integer upper threshold is
$$
H=\max_i l_i+a(\lceil r\rceil+1),
$$
since every cohort then requires at least $\lceil r\rceil+1$ copies. Binary search finds $h$ without enumerating copies.
At every completed stage, the average load is at most the final $W$, and the proved invariant bounds every load by $W+a_{\max}$. Thus multiplicities, loads, and search endpoints have polynomial binary length.
If $D$ clears all supply denominators, every cohort mass remains an integer multiple of $1/D$. Indeed, residual masses and cohort splits use supplies and integer combinations of existing masses. Consequently their encoding lengths remain polynomial.
There are at most one more cohort than processed goods, and polynomially many threshold searches and arithmetic operations. Scaling back proves the lemma. $\square$
Theorem B. If every good in $P$ has supply at least $4$, a complete $3/4$-EFX mass allocation can be constructed in time polynomial in $m,\tau,L$. Its support can be reduced to at most $\tau+m$ pairs.
More generally, the proof constructs a complete $(1-\delta)$-EFX allocation whenever the market-price quantity $\delta$ defined below is less than $1$.
I use the following established result: a finite linear Fisher market with positive budgets, nonnegative rational utilities, every buyer valuing some good positively, and every good valued positively by some buyer admits an exact rational equilibrium computable in polynomial time. At equilibrium, budgets are spent, goods clear, and purchases use only goods maximizing utility per unit of price. The rational output has polynomial encoding length. This follows from Orlin’s algorithm and its rationality analysis. [Orlin, Theorem 4.1, Section 1.1, and Lemma 2.1](https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol10171/DagSemProc.10171.2/DagSemProc.10171.2.pdf).
Assume first that $P$ is nonempty. Let
$$
T^+=\{t:v_t(e)>0\text{ for some }e\in P\},
\qquad
\beta=\sum_{t\in T^+}\mu_t.
$$
Give buyer $t\in T^+$ budget $\mu_t$, and give good $e\in P$ divisible supply $s_e$.
All budgets are positive. Every included buyer values an included good, and every included good is valued by an included buyer.
To put supplies in the unit-supply form of the market theorem, replace utility for one whole good by $s_ev_t(e)$. Rational budgets can be multiplied by a common denominator, and each buyer’s rational utilities can be scaled independently to integers. These transformations preserve demands after prices are scaled back and have polynomial encoding length.
Obtain equilibrium copy prices $p_e>0$ and quantities $x_{t,e}$ with
$$
\sum_t x_{t,e}=s_e,
\qquad
\sum_e p_ex_{t,e}=\mu_t.
$$
Define
$$
U_t=\frac{\sum_e x_{t,e}v_t(e)}{\mu_t}>0.
$$
The maximum utility-to-price ratio for buyer $t$ equals $U_t$, because its purchases use only maximizing goods and its budget is fully spent. Thus
$$
v_t(e)\leq U_tp_e
\qquad(e\in P),
$$
with equality whenever $x_{t,e}>0$.
Also,
$$
\sum_{e\in P}p_es_e=\beta\leq1.
$$
Let
$$
\delta=\max_{e\in P}p_e.
$$
Under the supply assumption,
$$
p_e\leq\frac{\beta}{s_e}\leq\frac14,
\qquad
\delta\leq\frac14.
$$
For each $t\in T^+$, apply Lemma 4 to weights $p_e$ and normalized supplies
$$
r_{t,e}=\frac{x_{t,e}}{\mu_t},
$$
omitting zero quantities. The average bundle price is
$$
\sum_e r_{t,e}p_e=1.
$$
Let $\ell_t$ be the minimum bundle price in its resulting distribution. Lemma 4 gives
$$
1-\delta\leq\ell_t\leq1.
$$
Write the price of a bundle as
$$
p(B)=\sum_e b_e(B)p_e.
$$
Every supported positive-good bundle of type $t$ uses only goods with $x_{t,e}>0$, so
$$
v_t(B)=U_tp(B).
$$
Moreover, for every supported bundle $C$ of type $u\in T^+$ and every positive-good copy in it,
$$
p(C\setminus\{e\})\leq\ell_u\leq1.
$$
Types outside $T^+$ receive empty bundles. They value every allocated positive-supply good at zero.
Choose a minimum-price cohort of one type in $T^+$ and append all goods in $Z$, using Lemma 1 normalized by that cohort’s mass. Assign price zero to these goods.
Removing a positive-good copy retains the previous price inequality. Removing a null copy leaves precisely the selected minimum core price, which is at most $1$. Therefore, after this step, every permitted deletion from every supported target bundle satisfies
$$
p(C\setminus\{e\})\leq1.
$$
No bundle value or source price changes.
For any active source type $t$ and supported source bundle $B$,
$$
v_t(B)=U_tp(B)\geq U_t(1-\delta).
$$
For any supported target bundle and any permitted deletion, the itemwise market inequalities give
$$
v_t(C\setminus\{e\})
\leq U_tp(C\setminus\{e\})
\leq U_t.
$$
Combining,
$$
v_t(B)\geq(1-\delta)v_t(C\setminus\{e\}).
$$
Inactive source types value all allocated bundles at zero, so their comparisons also hold.
Since $\delta\leq1/4$, the allocation is $3/4$-EFX. Finally,
$$
\frac34>\frac1{\sqrt2},
$$
as $9/16>1/2$, so it also satisfies the requested guarantee.
If $P$ is empty, all positive-supply goods are globally valueless. Apply Lemma 1 to their supplies normalized by one chosen type’s mass, and give the other types empty bundles. This is complete exact EFX.
The market computation, each application of Lemma 4, and null rounding are polynomial-time operations with polynomially encoded outputs. Lemma 2 gives the stated support bound. $\square$
The two theorems handle unrestricted support size, but impose different additional conditions: bounded variation in positive values, or sufficiently large supplies. Neither covers arbitrary scarce goods with unrestricted value ratios.
The supplied finite multigraph theorem still cannot be transferred by straightforward replication. If denominators are cleared using $Q$, a good valued by supported types $t,u$ is valued by
$$
Q(\mu_t+\mu_u)
$$
replicated individual agents, which can exceed two. Thus its individual-agent relevance hypothesis does not survive replication. [Finite multigraph theorem](https://arxiv.org/html/2506.09288v2).
No proof or counterexample for universal $1/\sqrt{2}$-EFX mass-allocation existence in the unrestricted two-relevant-types setting is established here. Polynomial-time construction in that setting also remains unresolved.
⟨structured verdict parsed — rendered above⟩
The output establishes rigorous conditional results, but does not resolve USER_TASK. I found no false central step in either conditional construction. The appropriate overall classification is partial, consistent with the prover’s own disclaimer.
The unresolved issue is substantive: the task permits both scarce goods and unrestricted ratios of positive values. Neither sufficient condition covers all such instances, even when every good is relevant to at most two supported types.
The prover explicitly assumes nonnegative binary rational valuations. This is a reasonable, explicitly stated interpretation of the intended goods setting. The conclusions below are verified under that convention.
Ignoring zero-supply goods is valid: their completeness equation is a sum of nonnegative terms equal to zero, so no positive-mass bundle can contain a copy.
The partition into positively valued positive-supply goods $P$ and globally valueless positive-supply goods $Z$ is exhaustive. The constructions address empty bundles, unbounded multiplicities, deletion of copies worth zero to the comparing type, and comparisons within a type.
The restriction to at most two relevant types per good is not used in the conditional proofs. This strengthens those conditional results, but does not remove their additional assumptions.
Verified.
The intervals $[c_{j-1},c_j)$ partition $[0,d)$, so the sum of the coordinate counts is exactly the count of shifted integers in $[0,d)$. Its cardinality is either $\lfloor d\rfloor$ or $\lceil d\rceil$.
The expectation calculation is correct. For each coordinate, the intersections with the unit intervals partition its defining interval, and only finitely many intersections have positive length.
All coordinate counts are constant between consecutive fractional-part breakpoints. Assigning interval lengths as probabilities therefore preserves every expectation; omitting the endpoints is legitimate because they have measure zero.
There are at most $p+1$ resulting intervals. Rational cumulative sums, fractional parts, interval lengths, and integer counts have polynomial encoding length. The construction requires no enumeration of individual copies.
The claims about minimum cardinality also follow: when $d$ is nonintegral, the expectation and the two possible cardinalities force total probability $1-\{d\}$ on cardinality $\lfloor d\rfloor$; when $d$ is integral, every supported vector has cardinality $d$.
The case $p=0$ is explicitly covered.
Verified.
The equality constraints reproduce exactly the type masses and good supplies. Summing the type constraints gives total mass $1$, so the nonnegative feasible polytope is bounded.
At a vertex, dependence among positive columns would allow sufficiently small perturbations in both directions while retaining nonnegativity. Thus its positive columns are independent, and their number is at most $\tau+m$.
The denominator estimate is valid. The selected square integer matrix has determinant of absolute value at most $r!H^r$. Clearing the right-hand-side denominators by $D$ gives a common denominator bounded by $Dr!H^r$. The bound has polynomial logarithm, and the coordinate bounds $0\leq x_{t,B}\leq1$ control numerator lengths.
Polynomial-time computation of a basic feasible solution applies to this explicitly represented rational system.
Finally, removing supported pairs cannot introduce an EFX comparison. This preservation argument applies to every comparison required in the task.
Verified.
Necessity is correct: types in $A$ can receive supply only from $N(A)$.
The flow network correctly represents assignments meeting the prescribed demands. A minimum cut cannot cross a good-to-type arc because that arc exceeds the capacity of the cut placing all types on the source side.
For a fixed set $A$ of sink-side types, the least possible finite cut capacity is
$$
f(A)+\sum_{t\notin A}h_t.
$$
The stated inequalities therefore ensure that a flow saturates every demand arc. Assigning unused supply to relevant types is legitimate under the residual-instance hypothesis.
The characterization
$$
\lambda=\min_{\varnothing\ne A\subseteq U}\frac{f(A)}{\mu(A)}
$$
follows from the demand criterion. Every denominator is positive.
The neighborhood-supply function is submodular. The union argument for tight sets is correct, including disjoint sets, for which the intersection contributes zero. A nonempty tight set exists because the minimum is attained over finitely many nonempty subsets.
For $A_*$, its aggregate lower bound equals the entire supply available to it. Consequently every individual lower bound is tight, and all supply in $N(A_*)$ is assigned inside $A_*$. This justifies removing both the types and their entire neighborhood.
For a type outside $A_*$, every subset containing it has strictly positive slack. The finite minimum-slack argument validates the increased demand. Hence the auxiliary optimization identifies exactly the types whose load is forced to equal $\lambda$.
The residual assignment remains feasible with every remaining load at least the current level. Successive levels are therefore nondecreasing.
A type valuing a retained good cannot have been removed earlier: its earlier removal would already have removed that good. This proves the required implication
$$
x_{u,e}>0,\quad v_t(e)>0
\quad\Longrightarrow\quad
d_u\leq d_t.
$$
Every good is removed once, and its full supply is retained. At least one type is removed per round.
The stated polynomial bounds on the number and size of rational linear programs are valid. Residual goods retain their original supplies, and residual types retain their original masses, so the level ratios have polynomial encoding length.
The empty-$P$ case is consistent with zero quantities and zero levels.
Verified under its stated condition.
Normalizing by $\mu_t$ is valid because every supported type has positive mass. Multiplying the rounded probabilities by $\mu_t$ restores the correct type mass and supply quantities.
Every rounded core uses only relevant goods. A coordinate with zero assigned quantity remains zero under Lemma 1.
The chosen minimum-count cohort exists with positive mass. Appending globally valueless goods to that cohort preserves its core and every source value. The normalized supplies and new masses have polynomial encoding length.
For an active comparing type, the source-value bound
$$
v_t(B)\geq a_t\lfloor d_t\rfloor
$$
is valid.
Whenever the target core contains a good relevant to $t$, Lemma 3 gives $d_u\leq d_t$, and hence
$$
|C^+|\leq\lceil d_u\rceil\leq\lfloor d_t\rfloor+1.
$$
The deletion argument correctly handles both possibilities:
Thus the target’s remaining value is bounded by $b_t\lfloor d_t\rfloor$. Deleting a globally valueless copy is also covered because such copies occur only on the selected core of cardinality $k\leq\lfloor d_t\rfloor$.
Types valuing no good in $P$ value every allocated bundle at zero. The argument therefore includes all types and comparisons within a type.
The transitions from $1/R$-EFX to exact EFX when $R=1$, and to $1/\sqrt2$-EFX when $R\leq\sqrt2$, are valid because remaining bundle values are nonnegative.
The example is correct. The stated rounding produces equal masses on $\{a\}$ and $\{a,b\}$, and deletion of $a$ from the latter requires
$$
1\geq\frac{M}{\sqrt2},
$$
which fails for $M>\sqrt2$.
The alternative equal-mass allocation on $\{b\}$ and $\{a,a\}$ has the required supplies and is exact EFX. The example demonstrates failure of that rounding construction, rather than failure of existence.
Verified.
After integer scaling, $F(h)$ is nondecreasing, $F(0)=0$, and the displayed $H$ is strictly infeasible. The largest feasible integer threshold therefore exists and can be found by binary search.
The identity
$$
F(h+1)-F(h)=\sum_{\text{active }i}q_i
$$
is correct: precisely the cohorts ending at load $h$ need another copy at the next threshold.
Maximality gives a residual supply strictly smaller than the active mass. Allocating one additional copy to that residual mass consumes exactly the supply and requires at most one cohort split.
The EFX invariant is valid:
Consequently every permitted deletion from an updated bundle leaves weight at most the final minimum load.
The bounds
$$
W-a_{\max}\leq\ell\leq W
$$
follow from the invariant and averaging as written.
The bit-complexity argument is also valid. Integer scaling has polynomial encoding length; loads and multiplicities have polynomial binary length; and cohort masses remain multiples of the reciprocal of a common supply denominator. Each processed good increases the cohort count by at most one.
Zero supplies cause no difficulty, and the case with no goods is explicitly handled.
Verified.
The cited source supports the required exact algorithm. Section $1.1$ states the market assumptions and equilibrium conditions, Theorem $4.1$ gives the polynomial algorithm, and Lemma $2.1$ supplies the rational reconstruction and denominator analysis. The source uses expenditure allocations; converting them to quantities at positive prices is consistent with the prover’s formulation. [Orlin’s paper](https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol10171/DagSemProc.10171.2/DagSemProc.10171.2.pdf).
The prover checks the relevant hypotheses: positive budgets, positive relevance for every included buyer, and positive relevance for every included good. Positive prices are consistent with positive supply and some buyer having positive linear utility for each included good.
The unit-supply conversion, budget scaling, and buyer-specific utility scaling preserve the required market behavior and have polynomial encoding length.
Full budget expenditure and purchase on maximizing goods justify
$$
v_t(e)\leq U_tp_e,
$$
with equality on purchased goods.
Market clearing gives
$$
\sum_{e\in P}p_es_e=\beta\leq1.
$$
Therefore $s_e\geq4$ implies $p_e\leq1/4$, with the stated constant correct.
Normalized purchases have average price $1$. Lemma 4 yields minimum price at least $1-\delta$, and every positive-good deletion has remaining price at most $1$.
Appending globally valueless goods to a minimum-price cohort preserves these bounds. Deleting a null copy leaves that cohort’s core price, which is at most $1$.
The final comparison
$$
v_t(B)\geq(1-\delta)v_t(C\setminus\{e\})
$$
follows because $\delta<1$ in the general stated version. Under the supply condition, this gives $3/4$-EFX.
The strict comparison
$$
\frac34>\frac1{\sqrt2}
$$
is correct. Inactive types and the empty-$P$ case are properly handled.
The polynomial output-size and support-compression claims follow from the preceding lemmas.
Major issue — target coverage. Neither universal existence nor polynomial-time construction for the unrestricted class is established. This is an acknowledged limitation, not a hidden error in the conditional proofs.
The replication objection is valid: replacing a supported type by many individual agents can make a single good relevant to more than two individuals. Thus the supplied finite-agent theorem cannot be applied directly through that replication.
For another round:
No additional clarification alone would close the remaining gap; resolving it requires new mathematics beyond this output.
⟨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.