Answer: —
Theorem 1 — class: algorithmic
Given finitely many valuation types \(T\), type masses \(\mu_t\), good categories \(G\), per-capita supplies \(\sigma_g\), and additive values \(v_t(g)\), compute a feasible bundle-mass plan \(\pi_{t,B}\) assigning integral bundles \(B\) to population mass while satisfying \(\sum_B\pi_{t,B}=\mu_t\) and \(\sum_{t,B}B_g\pi_{t,B}=\sigma_g\), maximizing or guaranteeing \(\alpha\) such that \(v_t(B)\ge\alpha R_t(B')\) whenever \(\pi_{t,B}>0\) and \(\pi_{u,B'}>0\), where \(R_t(B')\) is the expected value after uniformly deleting one good from \(B'\).
A society is given by its support: the list of the \(\tau\) valuation types with positive binary-rational masses \(\mu_t\), normalized by \(\sum_t\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types.
There are \(m\geq1\) good categories \(G\), with nonnegative binary-rational per-capita supplies \(\sigma_g\) and nonnegative binary-rational additive values \(v_t(g)\). Let \(L\) be the total input bit length.
An integral bundle is \(B\in\mathbb Z_{\geq0}^{m}\), allowing repeated copies of a category and the empty bundle; write \(|B|=\sum_g B_g\) and \(v_t(B)=\sum_g B_gv_t(g)\).
A bundle-mass plan has finitely many positive binary-rational entries \(\pi_{t,B}\), with \(\sum_B\pi_{t,B}=\mu_t\) and \(\sum_{t,B}B_g\pi_{t,B}=\sigma_g\) for every category. Bundle coordinates are encoded in binary.
Set \(R_t(0)=0\); for \(|B|>0\), set \(R_t(B)=\frac{|B|-1}{|B|}v_t(B)\), corresponding to uniformly deleting one individual copy, including copies of zero value.
For \(\alpha\in[0,1]\), a plan is \(\alpha\)-EFR if \(v_t(B)\geq\alpha R_t(B')\) whenever \(\pi_{t,B}>0\) and \(\pi_{u,B'}>0\), including comparisons within the same type.
Can a complete \(0.73\)-EFR bundle-mass plan always be computed in time polynomial in \(m,\tau,L\), or does this approximation guarantee fail through nonexistence or computational intractability?
For finitely many agents and individually listed indivisible goods with nonnegative additive valuations, a complete \(0.73\)-EFR allocation can be computed in polynomial time ([Farhadi et al.](https://ojs.aaai.org/index.php/AAAI/article/download/16675/16482)).
No result settling this precise bundle-mass approximation question was identified in the literature search.
Nonexistence is ruled out: every valid instance admits a complete $0.73$-EFR plan with polynomially many entries and polynomial-length encodings.
I do not resolve polynomial-time computability for arbitrary supported valuation types, or establish computational hardness. The new algorithmic result proved below covers arbitrary masses and supplies whenever, for each type, its smallest positive category value is at least $0.73$ times its largest positive category value. In particular, valuations taking values in $\{0,\lambda_t\}$ admit a polynomial-time complete $1$-EFR plan.
Write the input masses and supplies as
$$
\mu_t=\frac{p_t}{b_t},
\qquad
\sigma_g=\frac{q_g}{d_g},
$$
where all denominators are positive integers. Choose explicitly
$$
N=\prod_{t=1}^{\tau}b_t\prod_{g=1}^{m}d_g.
$$
Then
$$
n_t=N\mu_t,
\qquad
Q_g=N\sigma_g
$$
are integers, $n_t\geq1$, and
$$
\sum_t n_t=N.
$$
Moreover, $\log_2N\leq L$. If “binary-rational” means dyadic rational, this choice of $N$ is a power of two.
Let
$$
M=\sum_g Q_g.
$$
Construct a finite instance with $n_t$ agents of type $t$ and $Q_g$ individually listed copies of category $g$. There are $N$ agents and $M$ goods. Each copy has the corresponding nonnegative input value, and valuations are additive.
For $M>0$, the supplied finite-agent theorem gives a complete $0.73$-EFR allocation. Its deletion experiment chooses uniformly among individual copies. These are exactly the hypotheses and deletion convention of [Farhadi et al., Theorem 1 and Definition 3](https://ojs.aaai.org/index.php/AAAI/article/download/16675/16482). For $M=0$, allocate empty bundles.
For a multiplicity vector $B$ of cardinality $k>0$, uniform deletion leaves expected value
$$
v_t(B)-\frac{1}{k}\sum_g B_gv_t(g)
=
\frac{k-1}{k}v_t(B)
=
R_t(B).
$$
This includes repeated copies and zero-valued copies.
Let $c_{t,B}$ count the type-$t$ agents receiving bundle $B$. Define
$$
\pi_{t,B}=\frac{c_{t,B}}{N},
$$
omitting zero counts. Completeness gives
$$
\sum_B\pi_{t,B}=\mu_t,
\qquad
\sum_{t,B}B_g\pi_{t,B}=\sigma_g.
$$
Two distinct positive type-bundle entries have witnessing agents, so their required EFR comparison follows from the finite allocation. This includes distinct bundles assigned to the same type. An entry compared with itself satisfies
$$
v_t(B)\geq R_t(B)\geq0.73R_t(B).
$$
Comparisons against the empty bundle are immediate.
Thus every instance has a complete $0.73$-EFR plan. The construction above does not give the requested running time: the numerical values of $N$ and $M$ can be exponential in $L$.
The preceding existence proof can be sparsified while preserving the denominator $N$.
Set
$$
d=\tau+m,
\qquad
H=\max\{1,M\},
$$
and
$$
K=4d^2+2d\left\lceil\log_2(H+1)\right\rceil+1.
$$
Proposition. Every instance has a complete $0.73$-EFR plan with fewer than $K$ positive entries, each of the form $c_{t,B}/N$, where
$$
1\leq c_{t,B}\leq N,
\qquad
0\leq B_g\leq M.
$$
Proof. Start from the aggregated finite allocation. Index its positive entries by $i$, with type $t_i$, bundle $B_i$, and positive integer count $c_i$. Define
$$
a_i=(e_{t_i},B_i)\in\mathbb Z_{\geq0}^{d}.
$$
The required equations become
$$
\sum_i c_i a_i
=
(n_1,\ldots,n_\tau,Q_1,\ldots,Q_m).
$$
Every coordinate of $a_i$ is at most $H$.
Suppose the current support has $k\geq K$ entries. Its $2^k$ subsets have sums taking at most $(kH+1)^d$ different values. We verify that
$$
2^k>(kH+1)^d.
$$
For $k\geq4d^2$,
$$
\log_2k\leq\frac{k}{2d}.
$$
Indeed, $(\log_2x)/x$ decreases for $x\geq4$, and
$$
\log_2(4d^2)=2+2\log_2d\leq2d.
$$
Here the final inequality follows from $d\leq2^{d-1}$ for positive integer $d$. Consequently,
$$
d\log_2(kH+1)
\leq d\log_2k+d\log_2(H+1)
\leq\frac{k}{2}+d\log_2(H+1)
<k.
$$
The strict inequality follows from $k\geq K$.
Two distinct subsets therefore have equal sums. Subtracting their indicator vectors gives a nonzero vector
$$
y\in\{-1,0,1\}^{k},
\qquad
\sum_i y_i a_i=0.
$$
Each column’s type coordinates sum to one, so $\sum_i y_i=0$. Hence $y$ has both positive and negative entries.
Put
$$
\lambda=\min_{i:y_i=1}c_i
$$
and replace each count by $c_i-\lambda y_i$. The counts remain nonnegative integers, all equations are preserved, and at least one positive entry disappears.
Fairness persists because the new positive support is a subset of the old support. Repeat until fewer than $K$ entries remain. The type equations still imply $\sum_i c_i=N$, so every remaining count is at most $N$. The bundles are unchanged and retain their coordinate bound $M$. ∎
Since
$$
\log_2(M+1)=O(L+\log m),
$$
the proposition gives polynomial-length certificates. Such a certificate can be verified in polynomial time by checking the exact mass and supply equations and every ordered support-pair EFR inequality using rational arithmetic.
Thus the bounded search relation is total and polynomially verifiable: it belongs to $\mathrm{TFNP}$. Formally, malformed inputs can be assigned a distinguished “invalid input” witness, since validity is polynomial-time checkable.
This excludes an output-size obstruction. It supplies neither a polynomial-time construction nor a hardness result.
For a nonzero valuation type, define
$$
a_t=\min_{g:v_t(g)>0}v_t(g),
\qquad
b_t=\max_g v_t(g).
$$
Theorem. If
$$
a_t\geq\frac{73}{100}b_t
$$
for every nonzero type $t$, a complete $0.73$-EFR plan can be computed in time polynomial in $m,\tau,L$.
More generally, the algorithm guarantees $\rho$-EFR, where
$$
\rho=\min_{t:v_t\not\equiv0}\frac{a_t}{b_t}.
$$
When all valuations are zero, take $\rho=1$. The output has at most
$$
\tau(2m+1)+1
$$
positive entries, all with denominator $N$.
The main step is an exact result for the binary masks
$$
w_t(g)=\mathbf1_{\{v_t(g)>0\}}.
$$
We construct a complete plan satisfying, for every positive support pair and every individual copy $c$ in the compared bundle $C$,
$$
w_t(B)\geq w_t(C-c).
$$
Thus the construction removes envy after deleting any individual copy, including one valued at zero.
For now, ignore categories that nobody values. Also omit zero-supply categories. For each remaining category, let
$$
A_g=\{t:w_t(g)=1\},
$$
which is nonempty.
We use rational linear programming to compute nonnegative loads $\ell_t$ and a fractional assignment $x$ satisfying
$$
\sum_t x_{t,g}=Q_g,
\qquad
\sum_g x_{t,g}=n_t\ell_t,
$$
together with
$$
x_{t,g}>0,\ s\in A_g
\quad\Longrightarrow\quad
\ell_t\leq\ell_s.
$$
In words, a category is assigned only to types having the smallest load among the types that value it.
Here is an explicit polynomial-time construction and proof.
Maintain an active type set $S$ and an active category set $H$. Every active category has at least one active type that values it. At each stage solve the linear program
$$
\min z
$$
subject to
$$
\sum_{t\in A_g\cap S}x_{t,g}=Q_g
\quad(g\in H),
$$
$$
\sum_{g\in H:t\in A_g}x_{t,g}\leq n_tz
\quad(t\in S),
$$
$$
x_{t,g}\geq0,
\qquad
z\geq0.
$$
It is feasible: assign each category to any active type that values it, and choose a sufficiently large $z$. Its optimum $z^*$ is attained.
For each $t\in S$, minimize its load over the feasible solutions with $z=z^*$. Let $T$ be the types whose minimum load equals $n_tz^*$. Therefore every type in $T$ is saturated in every optimal solution.
First, $T$ is nonempty. Otherwise, for each active type there would be an optimal solution in which its load is strictly below its cap. Averaging these solutions would make every active type strictly below its cap. Their maximum normalized load would then be strictly below $z^*$, contradicting optimality.
Choose an optimal solution $x^0$ in which every type outside $T$ is strictly below its cap. Such a solution exists by averaging one suitable optimal solution for each type outside $T$.
Suppose $x^0_{t,g}>0$ for $t\in T$, and category $g$ is also valued by some $s\in S\setminus T$. A sufficiently small transfer of category $g$ from $t$ to $s$ preserves every supply equation and cap, but makes $t$ unsaturated. This contradicts the definition of $T$.
Consequently, $T$ receives goods only from
$$
H_T=\{g\in H:A_g\cap S\subseteq T\}.
$$
Every category in $H_T$ must be assigned within $T$. Since every member of $T$ is saturated,
$$
\sum_{g\in H_T}Q_g=z^*\sum_{t\in T}n_t.
$$
Assign $\ell_t=z^*$ to all $t\in T$, record the restriction of $x^0$ to $T$ and $H_T$, and remove those types and categories. Every remaining category still has an active type that values it. The residual assignment gives every remaining type a normalized load strictly below $z^*$, so the next optimum is strictly smaller.
At least one type disappears at each stage. Thus there are at most $\tau$ stages, using at most $O(\tau^2)$ linear programs.
The recorded assignments cover every category and give each type total load $n_t\ell_t$. If $x_{t,g}>0$, category $g$ was removed at the same stage as $t$. Any other original type valuing $g$ was removed either at that stage or earlier. Since stage loads strictly decrease, its load is at least $\ell_t$. This proves the desired load property.
All linear programs have polynomially many variables and constraints. Their coefficients have polynomial bit length. Moreover, each stage load has the explicit form
$$
z^*=
\frac{\sum_{g\in H_T}Q_g}{\sum_{t\in T}n_t},
$$
so its encoding has polynomial length. The standard polynomial-time theorem for rational linear programming therefore applies with all hypotheses satisfied.
Retain the category-type edges
$$
E=\{(g,t):t\in A_g,\ \ell_t=\min_{s\in A_g}\ell_s\}.
$$
The fractional assignment just constructed uses only these edges.
Set
$$
\underline{k}_t=\lfloor\ell_t\rfloor,
\qquad
\overline{k}_t=\lceil\ell_t\rceil.
$$
Consider a network with:
The fractional assignment is feasible in this network because
$$
n_t\underline{k}_t
\leq n_t\ell_t
\leq n_t\overline{k}_t.
$$
All capacities and lower bounds are integers. The integral-flow theorem, applied through the usual lower-bound reduction to maximum flow, gives an integral feasible flow. A polynomial-time maximum-flow algorithm finds it without expanding capacities into individual copies.
Let $X_{t,g}$ denote its category-to-type flows. Then
$$
\sum_tX_{t,g}=Q_g,
$$
and
$$
n_t\underline{k}_t
\leq \sum_gX_{t,g}
\leq n_t\overline{k}_t.
$$
Additionally,
$$
X_{t,g}>0,\ s\in A_g
\quad\Longrightarrow\quad
\ell_t\leq\ell_s.
$$
Fix a type $t$. Regard its $n_t$ hypothetical agents as cyclically indexed by
$$
0,1,\ldots,n_t-1.
$$
Process categories in a fixed order, assigning their $X_{t,g}$ copies cyclically and retaining the pointer between categories.
This produces balanced cardinalities: every type-$t$ agent receives either
$$
\left\lfloor\frac{\sum_gX_{t,g}}{n_t}\right\rfloor
\quad\text{or}\quad
\left\lceil\frac{\sum_gX_{t,g}}{n_t}\right\rceil
$$
goods. Therefore every resulting bundle $B$ satisfies
$$
\underline{k}_t\leq |B|\leq\overline{k}_t.
$$
Every assigned category is valued by its recipient type, so
$$
w_t(B)=|B|.
$$
The cyclic assignment has a polynomial-size implementation. Write
$$
X_{t,g}=n_th_{t,g}+r_{t,g},
\qquad
0\leq r_{t,g}<n_t.
$$
Every agent receives $h_{t,g}$ copies of category $g$, and agents in one cyclic interval receive an additional copy. That interval has at most two endpoints. The endpoints across all categories partition the indices into at most $2m+1$ intervals on each of which the entire bundle is constant.
Thus each type yields at most $2m+1$ bundle atoms. Their counts and coordinates are computed with binary integer arithmetic.
Consider a type-$t$ own bundle $B$ and a bundle $C$ assigned to type $u$, before adding globally unvalued categories.
If $w_t(C)=0$, every deletion comparison is immediate.
Otherwise, some category $g$ in $C$ is valued by $t$. Since $X_{u,g}>0$, the retained-edge property gives
$$
\ell_u\leq\ell_t.
$$
Hence
$$
|C|
\leq\lceil\ell_u\rceil
\leq\lfloor\ell_t\rfloor+1
\leq |B|+1.
$$
For any individual copy $c$ in $C$, the remaining bundle contains $|C|-1$ copies, each having mask value at most one. Therefore
$$
w_t(C-c)\leq |C|-1\leq |B|=w_t(B).
$$
This proof includes deletion of a copy that $t$ values at zero.
Choose an agent whose current bundle has globally minimum cardinality $k_{\min}$. Give that agent every copy of every category valued at zero by all types.
This is implemented by selecting a minimum-cardinality atom and, if necessary, splitting one agent from it. It increases the number of atoms by at most one.
Let $C^*$ be the padded bundle and $C^0$ its previous bundle. For every observer type $t$ and every own bundle $B$,
$$
w_t(C^*)=w_t(C^0)
\leq |C^0|
=k_{\min}
\leq w_t(B).
$$
The last inequality holds because own mask utilities equal the previous bundle cardinalities, and padding changes no utility.
Thus every observer is envy-free toward $C^*$ even before deletion. All other deletion comparisons persist because utilities are unchanged.
Aggregating atom counts and dividing by $N$ gives the exact prescribed masses and supplies, with at most $\tau(2m+1)+1$ entries. This completes the binary-mask construction.
For any nonzero type $t$ and any bundle $D$,
$$
a_tw_t(D)\leq v_t(D)\leq b_tw_t(D).
$$
Therefore, for every compared nonempty bundle $C$ and every individual copy $c$ in it,
$$
v_t(B)
\geq a_tw_t(B)
\geq a_tw_t(C-c)
\geq \frac{a_t}{b_t}v_t(C-c).
$$
Averaging over uniform deletion gives
$$
v_t(B)\geq\frac{a_t}{b_t}R_t(C)\geq\rho R_t(C).
$$
Zero valuation types and empty compared bundles satisfy the inequality directly.
This proves the theorem. In particular:
The algorithm uses polynomially many rational linear programs, one integral network-flow computation, and polynomially many binary arithmetic operations. It never lists the $N$ agents or the $M$ copies.
The proportional-types result from the notes also admits a fully specified compressed implementation.
Proposition. Suppose
$$
v_t(g)=\lambda_tw(g)
$$
for some nonnegative reference valuation $w$ and nonnegative scalars $\lambda_t$. A complete $1$-EFR plan can be computed in polynomial time, with at most $m+\tau$ entries and denominator $N$.
If some input row is nonzero, choose that row as $w$. Choose a category $g_0$ with $w(g_0)>0$ and compute
$$
\lambda_t=\frac{v_t(g_0)}{w(g_0)}.
$$
Under the proportionality hypothesis, these scalars satisfy every coordinate equality. They and $w$ have polynomial-length rational encodings. The hypothesis can also be checked by exact rational comparisons.
If all input rows are zero, use $w=0$. The zero-valued batching procedure below applies directly, and all fairness comparisons are automatic.
For $N$ hypothetical agents with common valuation $w$, process categories in nonincreasing order of $w(g)$. Give each copy to a minimum-utility agent.
This procedure maintains
$$
w(B)\geq w(C-c)
$$
for every pair of agents and every individual copy $c$ in the compared bundle $C$.
To prove the invariant, suppose a copy of value $c_0$ is given to a minimum-load agent whose previous load is $U$. Every other agent has load at least $U$. Every previously assigned copy has value at least $c_0$. Deleting any copy from the updated bundle therefore leaves value at most
$$
U+c_0-c_0=U.
$$
All comparisons toward that updated bundle hold. Comparisons toward unchanged bundles persist because the recipient’s utility increases and other utilities remain unchanged. The initial empty allocation satisfies the invariant.
This argument also covers $c_0=0$.
Represent the population by atoms $(c_i,B_i)$, where $c_i$ agents have bundle $B_i$. Initially there is one atom $(N,0)$.
For a category of value $c>0$ with $Q$ copies, write
$$
\frac{w(B_i)}{c}=a_i+r_i,
\qquad
a_i=\left\lfloor\frac{w(B_i)}{c}\right\rfloor,
\qquad
0\leq r_i<1.
$$
Each agent in atom $i$ has successive assignment events at normalized loads
$$
a_i+r_i,\ a_i+r_i+1,\ a_i+r_i+2,\ldots.
$$
The greedy procedure processes these events in nondecreasing order.
For an integer $q\geq0$, the number of events strictly below $q$ is
$$
C(q)=\sum_i c_i\max\{0,q-a_i\}.
$$
For $Q>0$, find the smallest integer $q\geq0$ satisfying
$$
C(q+1)\geq Q.
$$
Binary search suffices, using the upper bound $\max_i a_i+Q$. Minimality gives
$$
C(q)\leq Q\leq C(q+1).
$$
Give every agent in atom $i$ the first
$$
h_i=\max\{0,q-a_i\}
$$
copies. The remaining $Q-C(q)$ events occur in $[q,q+1)$: each active atom, with $a_i\leq q$, contributes one event per agent at $q+r_i$.
Sort active atoms by $r_i$ and process these events, breaking ties arbitrarily. At most one atom is processed partially and splits. This realizes a permissible greedy execution and increases the number of atoms by at most one.
Choose a minimum-load atom of count $c_i$. For a zero-valued category, write
$$
Q=c_ih+r,
\qquad
0\leq r<c_i.
$$
Give $h$ copies to every agent in that atom and one extra copy to $r$ of them. Every assignment is permitted by the greedy rule because utilities remain unchanged. Again, at most one atom splits.
Consequently there are at most $m+1$ atoms throughout. Counts are at most $N$, and coordinates are at most $M$. Loads, quotients, and search endpoints have polynomial bit length, so every category is processed in polynomial time.
Let the final atoms have counts $c_i$. Partition the integer interval $[0,N)$ into consecutive atom intervals of lengths $c_i$. Independently partition it into consecutive type intervals of lengths $n_t$.
For each nonempty intersection, assign its atom’s bundle to its type, with mass equal to the intersection length divided by $N$. This preserves all atom counts and all type counts, hence every mass and supply equation.
If there are $r\leq m+1$ atoms, the two interval partitions have at most $r+\tau-1$ nonempty intersections. Thus the output has at most $m+\tau$ entries, all with denominator $N$.
The common-reference invariant gives
$$
w(B)\geq w(C-c).
$$
Multiplication by $\lambda_t\geq0$ gives
$$
v_t(B)\geq v_t(C-c).
$$
Averaging over deletion proves $1$-EFR. This completes the proposition.
The results establish universal existence and polynomial-size verifiable witnesses. They also give polynomial-time constructions for two substantive regimes: proportional valuations, and valuations whose positive values have sufficiently small spread within each type.
They do not settle the general computational question. In particular, neither exponential finite replication nor the sparsification argument establishes computational intractability. A general polynomial-time construction or a justified search-complexity hardness result is still needed.
⟨structured verdict parsed — rendered above⟩
Overall assessment: partial, with sound substantive progress. The output establishes universal existence and polynomial-size certificates, and its two restricted polynomial-time constructions are sound apart from minor implementation clarifications. It does not settle the general computational question in USER_TASK. The prover accurately acknowledges that limitation.
I found no false central mathematical step.
The choice
$$
N=\prod_t b_t\prod_g d_g
$$
makes all $n_t=N\mu_t$ and $Q_g=N\sigma_g$ integers. Positivity of the masses gives $n_t\geq1$, and normalization gives
$$
\sum_t n_t=N.
$$
The bound $\log_2N\leq L$ is valid for explicitly binary-encoded numerators and denominators. Under the dyadic interpretation of “binary-rational,” $N$ is a power of two, so the constructed masses remain dyadic.
No divisibility or normalization hypothesis is missing.
The replicated instance has finitely many agents and individually distinguished goods, with normalized, nonnegative additive valuations. These match the finite-agent theorem supplied in USER_TASK. The cited paper defines deletion uniformly over the items in the compared bundle and requires complete final allocations. Thus repeated category copies and zero-valued copies have the intended interpretation. [Farhadi et al., Theorem 1 and Definitions 3 and 5](https://ojs.aaai.org/index.php/AAAI/article/download/16675/16482).
The calculation
$$
\mathbb E[v_t(B-c)]
=
v_t(B)-\frac{v_t(B)}{|B|}
=
R_t(B)
$$
is correct for every nonempty bundle. It does not discard zero-valued copies.
The counts $c_{t,B}$ yield the exact mass and supply equations after division by $N$.
Distinct positive type-bundle entries have distinct witnessing agents, so the finite allocation supplies every comparison between those entries, including distinct bundles assigned to the same type. Comparison of an entry with itself follows from
$$
v_t(B)\geq R_t(B)\geq0.73R_t(B).
$$
Empty compared bundles impose no additional condition.
The case $M=0$ is handled correctly.
Conclusion: Universal existence is established. The observation that replication may require exponentially many agents or goods is also correct; this existence argument does not establish polynomial-time construction in the compressed input model.
The columns
$$
a_i=(e_{t_i},B_i)
$$
correctly encode both the type-count and supply equations. Their coordinates are bounded by $H=\max\{1,M\}$, including when $M=0$.
For support size $k$, there are $2^k$ subsets and at most $(kH+1)^d$ possible sums. The stated inequalities establish the required strict excess:
$$ \frac{k}{2}+d\log_2(H+1)<k. $$
Thus the pigeonhole argument is valid, with the stated constants and ranges.
Equal subset sums produce a nonzero signed vector $y$ satisfying the column dependence. Since every column has type-coordinate sum one,
$$
\sum_i y_i=0,
$$
so $y$ has both signs.
The update $c_i-\lambda y_i$ preserves all equations and nonnegativity, and removes at least one positive entry. It introduces no new bundle. Consequently, all fairness comparisons required by the reduced support were already required before the update.
Iteration terminates because the support strictly decreases. The surviving counts satisfy $c_i\leq N$, and the surviving bundle coordinates remain bounded by $M$.
The bound
$$
\log_2(M+1)=O(L+\log m)
$$
is valid. Together with the support bound and $\log_2N\leq L$, it gives polynomial total certificate length.
Exact rational verification of all equations and all ordered support-pair inequalities is polynomial time. The claimed $\mathrm{TFNP}$ membership is justified for the bounded certificate relation described here, with malformed inputs handled by the distinguished witness.
Conclusion: Polynomial-size witnesses and polynomial-time verification are established. The sparsification proof gives no polynomial-time procedure for finding the necessary subset collisions; the prover correctly makes no such claim.
The stage linear program is feasible and has an attained optimum. Positivity of every $n_t$ makes the normalized-load arguments valid.
The proof that $T$ is nonempty is sound: averaging optimal solutions that separately leave each type unsaturated would leave every type unsaturated and contradict optimality.
The transfer argument is also sound. A positive assignment from a saturated type to a category with an unsaturated eligible recipient could be transferred in sufficiently small amount, contradicting saturation in every optimal solution.
It follows that the categories in $H_T$ account exactly for the saturated types’ loads. Removing them leaves a feasible residual assignment with strictly smaller maximum normalized load whenever types remain. The resulting stage ordering proves the retained-edge property.
The number and sizes of the linear programs are polynomial, and the displayed ratio for each stage load bounds its encoding length.
Minor issue: The averaging prescription does not explicitly define $x^0$ when $T=S$, because there are then no outside types to average over. The stopping condition when no active types remain is also implicit.
Minimum clarification: State how an optimal solution is selected when $T=S$, and state the loop’s termination condition explicitly. Neither requires additional mathematics.
The constructed fractional assignment satisfies every lower and upper bound. The capacities, supplies, and bounds are integers, so the integral-flow theorem applies to the lower-bound network.
The capacity $M$ on a category-to-type edge is sufficient because no category has more than $M$ copies. Binary capacity encoding avoids expansion into individual copies.
The resulting $X_{t,g}$ therefore has all the stated conservation, load, and retained-edge properties.
Retaining the cyclic pointer across categories balances total cardinalities. The network bounds imply that every resulting bundle has cardinality between $\lfloor\ell_t\rfloor$ and $\lceil\ell_t\rceil$.
Every assigned category is positively valued by its recipient type, so its own mask utility equals its cardinality.
For each category, division by $n_t$ gives a common multiplicity plus one cyclic interval of additional copies. The combined endpoints yield at most $2m+1$ constant-bundle intervals. Counts and coordinates can be computed in binary without listing agents.
If $w_t(C)>0$, some category in $C$ is valued by $t$. The retained-edge property gives $\ell_u\leq\ell_t$, and the displayed cardinality chain is valid:
$$
|C|
\leq\lceil\ell_u\rceil
\leq\lfloor\ell_t\rfloor+1
\leq|B|+1.
$$
Deleting any copy leaves mask value at most $|C|-1$. This includes deletion of a copy valued at zero by the observer.
The case $w_t(C)=0$ is immediate, as claimed.
Padding an agent whose previous bundle has minimum cardinality is justified by the displayed envy-free bound. That bound also covers the padded agent as observer, since padding changes no mask utility.
Splitting one agent from an atom increases the number of entries by at most one. Exact masses and supplies are preserved.
The inequalities
$$
a_tw_t(D)\leq v_t(D)\leq b_tw_t(D)
$$
hold for arbitrary bundles, including bundles containing zero-valued categories. Since $b_t>0$ for nonzero types, the ratio is defined.
The subsequent inequality chain has the correct direction, and averaging over deletion proves the stated $\rho$-EFR guarantee. Zero valuation types and empty compared bundles are covered.
Conclusion: The restricted polynomial-time theorem is sound, subject to the minor stage-selection clarification above.
Choosing a nonzero input row as $w$ and recovering the proportionality scalars from a positive coordinate is valid under the hypothesis. The encoding and exact-check claims are justified. The all-zero case is treated separately.
The invariant proof is correct. Because categories are processed in nonincreasing value order, deleting any copy from the updated bundle removes value at least that of the newly assigned copy. All other agents had utility at least the recipient’s previous utility. Comparisons toward unchanged bundles persist.
This reasoning covers zero-valued copies.
The successive event loads and the formula
$$
C(q)=\sum_i c_i\max\{0,q-a_i\}
$$
correctly count events strictly below integer $q$, including when a fractional part is zero.
The binary-search bound is valid. Minimality gives the stated bracketing, with $C(0)=0$ covering $q=0$.
After all events below $q$ are processed, ordering the remaining events by $r_i$ realizes a permissible greedy execution. Only one atom can be partially processed, so the atom-count bound follows.
Minor issue: This prescription defines $q$ only for $Q>0$, while the input permits zero-supply categories.
Minimum clarification: Explicitly specify the action for $Q=0$ before invoking the batching prescription.
Zero-valued copies can be assigned within a minimum-load atom because they never change utility. The division and possible split are correct.
The atom and type interval partitions have at most $r+\tau-1$ nonempty intersections. This preserves all counts and hence every mass and supply equation.
Multiplication by $\lambda_t\geq0$ preserves the common-reference deletion inequalities, including for zero types. Averaging proves $1$-EFR.
Conclusion: The proportional-types polynomial-time result is sound, subject to the minor zero-supply clarification.
The general algorithm-versus-intractability question is unanswered. This is a major target-level incompleteness, rather than an erroneous claim of success: the prover explicitly labels its resolution partial.
Universal existence eliminates nonexistence as an explanation for failure of the approximation guarantee. Polynomial-size certificates eliminate a certificate-size obstruction. Neither establishes an efficient general construction or computational hardness.
To resolve USER_TASK, additional substantive work is required: either a polynomial-time algorithm for arbitrary supported valuation types, or an applicable hardness result with a precisely specified computational problem and reduction.
⟨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.