Answer: —
Theorem 4.3 — class: algorithmic
Given item types \(G\), an independence-system oracle \(\mathcal F\), strict rankings for \(\tau\) agent types with rational masses \(\mu_t\) summing to \(1\), and rational per-capita supplies \(b_g\), find a polynomial-bit rational assignment \(x_{t,S}\geq 0\), or certify none exists. Require \(\sum_{S\in\mathcal F}x_{t,S}=\mu_t\) and \(\sum_{t,S:g\in S}x_{t,S}\leq b_g\), so each agent receives a whole feasible bundle. Every pair of bundles assigned positive mass must satisfy EF1 under the first bundle’s type ranking; the assignment must also admit no feasible reassignment of the same agents that weakly improves every agent and strictly improves a positive mass. Is this solvable in time and oracle calls polynomial in \(m,\tau,L\)?
Let \(G\) contain \(m\geq1\) item types. A common independence system \(\mathcal F\subseteq2^G\), containing \(\emptyset\) and closed under subsets, is given by a membership oracle.
A society is given by its support: the list of \(\tau\) types with positive binary-rational masses \(\mu_t\), summing to \(1\). Here \(\tau\) is the support size, not the number of possible rankings. Each type supplies a strict ranking of \(G\); all items are desirable, and bundles are compared lexicographically by the highest-ranked item in their symmetric difference. Write \(\succeq_t\) for weak preference.
Supplies \(b_g\geq0\) are binary rationals; \(L\) is the total binary input length excluding the oracle. Each agent receives a whole bundle \(S\in\mathcal F\), hence at most one item of each type; unused supply is allowed.
An assignment consists of masses \(x_{t,S}\geq0\) satisfying \(\sum_{S\in\mathcal F}x_{t,S}=\mu_t\) and \(\sum_{t,S:g\in S}x_{t,S}\leq b_g\).
Require EF1: whenever \(x_{t,S}>0\) and \(x_{u,T}>0\), some \(Z\subseteq T\) with \(|Z|\leq1\) satisfies \(S\succeq_t T\setminus Z\).
Require Pareto optimality: no reassignment may split the mass of each current group \((t,S)\) among feasible bundles weakly preferred to \(S\), respect the same supplies, and strictly improve a positive total mass. Reassignments may use real masses and need not satisfy EF1.
The computational problem is to find an assignment as a sparse list of nonzero rational entries with polynomial total encoding length, or report that no EF1 and Pareto-optimal assignment exists.
Can this problem be solved with time and oracle calls polynomial in \(m,\tau,L\), or is it NP-hard?
Discrete: a polynomial-time round-robin algorithm is known to produce EF1 and Pareto-optimal allocations under a common independence system and lexicographic preferences. [Source](https://arxiv.org/html/2411.01462v2)
Continuous resources: an efficient envy-free and Pareto-efficient mechanism is known for divisible goods with lexicographic preferences; that model does not require whole feasible bundles. [Source](https://arxiv.org/abs/1206.4366) No result settling the mass-of-agents problem above was located.
I do not resolve the full polynomial-time versus NP-hardness question. I establish three results for arbitrary supported rankings:
The second result includes a self-contained proof of the sparse rational witness theorem from NOTES.
Write $g\succ_t h$ when type $t$ ranks item $g$ above item $h$. For an assignment $x$, define
$$
u_g(x)=\sum_{t,S:g\in S}x_{t,S}.
$$
Its positive support is
$$
J(x)=\{(t,S):x_{t,S}>0\}.
$$
For a supported group $(t,S)$ and an item $g\notin S$, define
$$
P_{t,g}(S)=\{h\in S:h\succ_t g\},
$$
$$
D_{t,g}(S)=\{h\in S:g\succ_t h\},
$$
and
$$
E_{t,g}(S)=P_{t,g}(S)\cup\{g\}.
$$
Thus $E_{t,g}(S)$ gains $g$, preserves every item of $S$ ranked above $g$, and discards every item of $S$ ranked below $g$. Whenever $E_{t,g}(S)\in\mathcal F$, call the replacement
$$
S\longrightarrow E_{t,g}(S)
$$
an elementary improvement. Its highest-ranked changed item is the gained item $g$, so it strictly improves type $t$.
Lemma 1. An assignment admits a Pareto improvement if and only if it admits one using only elementary improvements and unchanged bundles.
Proof. The reverse implication follows immediately from the definition of an elementary improvement.
For the forward implication, represent a Pareto improvement by transfer masses from supported groups $(t,S)$ to feasible destinations $R\succeq_t S$. There are finitely many possible transfer coordinates, because both the type set and $\mathcal F$ are finite.
Consider a positive transfer with $R\ne S$. Lexicographic preferences are a strict total order on distinct bundles, so $R\succ_t S$. Let $g$ be the highest-ranked item in $R\triangle S$, according to type $t$. Because the transfer is an improvement,
$$
g\in R\setminus S.
$$
Every item of $S$ ranked above $g$ also belongs to $R$. Consequently,
$$
E_{t,g}(S)\subseteq R.
$$
Heredity implies $E_{t,g}(S)\in\mathcal F$.
Replace this transfer’s destination by $E_{t,g}(S)$, keeping its mass unchanged. The replacement remains a strict improvement from $S$. Moreover, it consumes no more of any item than destination $R$.
Perform this replacement for every changed positive transfer and leave unchanged transfers intact. Source-group masses are preserved, aggregate consumption can only decrease relative to the proposed reassignment, and a positive mass remains strictly improved. The resulting reassignment is therefore a feasible Pareto improvement of the required form. $\square$
For an assignment $x$, define its set of elementary gain items by
$$
A(x)=
\left\{
g\in G:
\begin{array}{l}
\text{there exists }(t,S)\in J(x)\text{ with }g\notin S\\
\text{and }E_{t,g}(S)\in\mathcal F
\end{array}
\right\}.
$$
Define a directed graph $\Gamma(x)$ on vertex set $G$. It has an edge
$$
g\longrightarrow h
$$
if some supported group $(t,S)$ admits the elementary improvement gaining $g$ and
$$
h\in D_{t,g}(S).
$$
An edge records an elementary improvement that gains its initial vertex and releases its terminal vertex. Each edge can be stored together with one witnessing group and elementary improvement.
Theorem 2. An assignment $x$ is Pareto optimal if and only if both conditions hold:
$$ u_g(x)=b_g\qquad\text{for every }g\in A(x). $$
Suppose $g\in A(x)$ and $u_g(x)<b_g$. Choose a witnessing supported group $(t,S)$. For
$$
0<\delta\leq\min\{x_{t,S},\,b_g-u_g(x)\},
$$
move mass $\delta$ from $S$ to $E_{t,g}(S)$.
The move gains only $g$ and releases the items in $D_{t,g}(S)$. It respects all supplies and strictly improves positive mass. Thus $x$ is not Pareto optimal.
Suppose $\Gamma(x)$ has a directed cycle with distinct vertices
$$
g_1\longrightarrow g_2\longrightarrow\cdots
\longrightarrow g_\ell\longrightarrow g_1.
$$
For each edge $g_i\longrightarrow g_{i+1}$, with indices interpreted cyclically, choose a witnessing elementary improvement from a group $j_i$. This improvement gains $g_i$ and releases $g_{i+1}$, possibly releasing other items as well.
A group may witness several cycle edges. Let $c_j$ be the number of selected moves whose source is group $j$, and choose
$$
\delta=\frac12\min_{j:c_j>0}\frac{x_j}{c_j}.
$$
All groups in this minimum have positive mass, so $\delta>0$. Split off mass $\delta$ for each selected move. Their total source mass from group $j$ is $c_j\delta\leq x_j$.
Each cycle item is gained once, by mass $\delta$, and released at least once, by its predecessor’s move. Items outside the cycle are never gained. Thus aggregate consumption of every item weakly decreases.
All selected transfers strictly improve their recipients, so this is a Pareto improvement. Therefore a Pareto-optimal assignment cannot have a directed cycle.
This construction uses precisely the permission to split a current group among multiple destinations.
Assume all items in $A(x)$ have exhausted supply and $\Gamma(x)$ is acyclic. Suppose, for contradiction, that a Pareto improvement exists.
By Lemma 1, replace it by a reassignment using elementary improvements and unchanged bundles. Let $B$ be the nonempty set of items gained by elementary improvements carrying positive mass.
Since $\Gamma(x)$ is acyclic, it has a topological ordering $\pi$ such that
$$
g\longrightarrow h\quad\Longrightarrow\quad \pi(g)<\pi(h).
$$
Choose $g\in B$ minimizing $\pi(g)$.
No positive elementary transfer can release $g$. Indeed, such a transfer would gain some $a\in B$ and create an edge $a\longrightarrow g$, giving
$$
\pi(a)<\pi(g),
$$
contrary to the choice of $g$.
At least one positive transfer gains $g$, and none releases it. Its aggregate consumption therefore strictly increases. But $g\in A(x)$ and $u_g(x)=b_g$, so the reassignment violates its supply constraint. This contradiction proves sufficiency. $\square$
Suppose a rational candidate assignment has $k$ positive entries.
First verify bundle feasibility, type totals, and supply constraints. Next, for each supported group and each missing item $g$, query whether $E_{t,g}(S)\in\mathcal F$. These require at most $km$ additional oracle calls. The answers determine $A(x)$ and $\Gamma(x)$.
The graph has $m$ vertices and at most $m(m-1)$ distinct edges. Its construction, its acyclicity test, and the exact supply-equality checks all take polynomial time in $m$, $k$, and the rational encoding length.
Thus Pareto optimality is polynomially verifiable even though its definition quantifies over reassignments with real masses and potentially exponentially many destinations.
When Pareto optimality fails, the proof supplies an explicit improvement: either one elementary move using slack supply, or at most $m$ elementary moves witnessing a directed cycle.
The characterization also gives a succinct certificate excluding all Pareto improvements.
Corollary 3. If $x$ is Pareto optimal, there are nonnegative integer item prices $p_g$, each using $O(m\log(m+1))$ bits, such that:
$$ \sum_{g\in R}p_g>\sum_{g\in S}p_g. $$
Proof. Let $\pi$ be a topological ordering of $\Gamma(x)$, indexed from $1$ to $m$, and put
$$
p_g=
\begin{cases}
(m+1)^{m-\pi(g)},&g\in A(x),\\
0,&g\notin A(x).
\end{cases}
$$
Theorem 2 implies that every positive-price item has exhausted supply. The asserted bit bound follows directly from this formula.
For any elementary improvement gaining $g$, every released item $h$ has an edge $g\longrightarrow h$. If $p_h>0$, then
$$
p_h\leq\frac{p_g}{m+1}.
$$
There are at most $m$ released items, and hence
$$
\sum_{h\in D_{t,g}(S)}p_h
\leq\frac{m}{m+1}p_g<p_g.
$$
Therefore
$$
\sum_{h\in E_{t,g}(S)}p_h-\sum_{h\in S}p_h
=
p_g-\sum_{h\in D_{t,g}(S)}p_h>0.
$$
For an arbitrary feasible $R\succ_t S$, Lemma 1’s construction gives an elementary destination $E_{t,g}(S)\subseteq R$. Nonnegativity of prices yields
$$
\sum_{h\in R}p_h
\geq\sum_{h\in E_{t,g}(S)}p_h
>\sum_{h\in S}p_h.
$$
This proves the claim. $\square$
For completeness, these properties directly exclude a Pareto improvement. Every unchanged transfer preserves price expenditure, and every strictly improving transfer increases it. A positive strictly improved mass would therefore increase aggregate expenditure. Yet the original assignment already spends
$$
\sum_g p_g u_g(x)=\sum_g p_g b_g,
$$
which is the maximum expenditure compatible with the supplies.
I now reprove the sparse witness result using Theorem 2.
Theorem 4. If an EF1 and Pareto-optimal assignment exists with real masses, then one exists with at most $\tau+m$ positive rational entries. Each mass has encoding length
$$
O\bigl(L+(\tau+m)\log(\tau+m+1)\bigr).
$$
Let $x$ be a real-valued EF1 and Pareto-optimal assignment. Put
$$
J=J(x),\qquad A=A(x).
$$
Consider the polytope $K$ of assignments $y$ satisfying:
$$ u_g(y)=b_g\qquad(g\in A). $$
The polytope is nonempty because $x\in K$, by Theorem 2. It is bounded because each coordinate is nonnegative and at most its type’s mass.
Every $y\in K$ is EF1: its positive support is a subset of $J$, so all its required comparisons were already required and satisfied for $x$.
Every $y\in K$ is also Pareto optimal. Indeed,
$$
A(y)\subseteq A(x),\qquad
\Gamma(y)\subseteq\Gamma(x).
$$
The second inclusion means edge inclusion on the common vertex set. Thus $\Gamma(y)$ is acyclic, and every item in $A(y)$ has exhausted supply in $y$. Theorem 2 applies.
A nonempty bounded polytope in a finite-dimensional space has a vertex. Choose a vertex $y$ of $K$, and let $k$ be its number of positive coordinates.
Restrict the active type-total and supply equations to these $k$ coordinates. Their coefficient matrix must have column rank $k$. Otherwise, there would be a nonzero perturbation supported on the positive coordinates that preserves all these equations.
For sufficiently small perturbations in either direction:
Both perturbations would lie in $K$, contradicting that $y$ is a vertex.
There are only $\tau+m$ type-total and supply rows. Consequently,
$$
k\leq\tau+m.
$$
Select $k$ independent active equations determining the positive coordinates. Their coefficient matrix $M$ is a nonsingular $k\times k$ matrix with entries in $\{0,1\}$. Their right-hand sides are input masses or supplies.
Let $D$ be the product of the denominators of all input masses and supplies. Its binary length is $O(L)$. Multiplying the right-hand sides by $D$ gives integers of binary length $O(L)$.
By Cramer’s rule, each positive coordinate can be written with denominator $D\det M$. The determinant expansion gives
$$
|\det M|\leq k!.
$$
If $M_i$ is obtained by replacing one column of $M$ by the integer right-hand side vector $c$, then
$$
|\det M_i|\leq k!\max_j|c_j|.
$$
Thus each numerator and denominator has binary length
$$
O\bigl(L+k\log(k+1)\bigr).
$$
The selected vertex is EF1 and Pareto optimal, as proved above. Encoding its at most $\tau+m$ bundles and type indices also takes polynomial space. $\square$
EF1 is polynomially checkable on a sparse support. For a nonempty target bundle $T$, let $h_t(T)$ be its highest-ranked item according to the comparing type $t$. Among all permitted deletions, deleting $h_t(T)$ gives the least-preferred remainder: deleting any other item retains $h_t(T)$, which is the highest-ranked difference between the two remainders.
Therefore the required comparison is equivalent to
$$
S\succeq_t T\setminus\{h_t(T)\}.
$$
For an empty target bundle the comparison holds automatically, because every item is desirable.
There are at most $k^2$ support comparisons, each computable from the explicit rankings and bundles. Together with Theorems 2 and 4, this proves:
Corollary 5. The decision problem asking whether an EF1 and Pareto-optimal assignment exists belongs to $\mathrm{NP}$ relative to the membership oracle. For any representation of $\mathcal F$ with polynomial-time membership testing, it belongs to ordinary $\mathrm{NP}$.
This is a certificate result. It does not provide a polynomial algorithm for discovering a suitable support.
Call an item partially supplied if
$$
0<b_g<1.
$$
The threshold $1$ is the population mass. Since a bundle contains at most one copy of each item,
$$
u_g(x)\leq\sum_t\mu_t=1
$$
for every assignment. Thus supplies at least $1$ never restrict feasibility.
Theorem 6. Suppose at most one item is partially supplied. Then an EF1 and Pareto-optimal assignment exists and can be computed in polynomial time, using at most $2\tau m$ membership-oracle calls. It has at most $\tau+1$ positive entries.
We first record the greedy fact used by the algorithm.
Fix a type, an available item set $H$, and a mandatory feasible set $Q\subseteq H$. Start with $Q$, inspect the items of $H\setminus Q$ in the type’s ranking order, and add an item whenever the resulting set belongs to $\mathcal F$.
The output is the lexicographically best feasible subset of $H$ containing $Q$.
To prove this, suppose a feasible candidate containing $Q$ were better than the greedy output. Let $h$ be their highest-ranked differing item. The candidate contains $h$, while the greedy output does not. At the step when $h$ was rejected, the current set consisted of $Q$ and the previously accepted items. The candidate contains all those items, because it agrees with the output above $h$ and contains $Q$. The candidate also contains $h$.
Heredity would therefore make the rejected extension feasible, a contradiction.
This algorithm uses at most $m$ membership queries, including a feasibility check of $Q$ if needed.
Let
$$
H=\{h:b_h\geq1\}.
$$
Every positively allocated bundle must avoid zero-supply items. Give each type its lexicographically best feasible subset of $H$, computed greedily.
This assignment is feasible because each item’s usage is at most $1$. It is envy-free: every target bundle is a feasible subset of $H$, and each type receives its best such bundle. It is Pareto optimal because no positive group has any strictly preferred feasible destination using available items.
Let $g$ be the unique partially supplied item and write
$$
q=b_g,\qquad 0<q<1.
$$
Put
$$
H=\{h:b_h\geq1\}.
$$
For each type $t$, compute:
Compute $U_t$ with mandatory set $\emptyset$, and $V_t$ with mandatory set $\{g\}$. If $\{g\}\notin\mathcal F$, heredity implies that no feasible bundle contains $g$.
Call type $t$ favorable if $V_t$ exists and
$$
V_t\succ_t U_t.
$$
Let its total favorable mass be
$$
d=\sum_{t:\,V_t\succ_t U_t}\mu_t.
$$
Choose any fixed order of favorable types. Give $V_t$ to their mass in that order, up to total mass $\min\{q,d\}$. Give $U_t$ to everyone else.
At most one type is split between the two bundles. Thus the output has at most $\tau+1$ positive entries. It is feasible: the usage of $g$ is $\min\{q,d\}$, every other positively used item has supply at least $1$, and zero-supply items are absent.
Every recipient of $V_t$ is favorable. Its bundle is its global best feasible bundle within $H\cup\{g\}$, because $U_t$ and $V_t$ are respectively the best bundles excluding and including $g$. Such a recipient does not envy any allocated bundle.
A nonfavorable type receiving $U_t$ likewise receives its global best bundle within $H\cup\{g\}$.
It remains to consider an unserved favorable group receiving $U_t$. Let $T$ be any positively allocated target bundle.
If $g\notin T$, then $T$ is a feasible subset of $H$, and hence
$$
U_t\succeq_t T.
$$
If $g\in T$, heredity gives
$$
T\setminus\{g\}\in\mathcal F,
$$
and this remainder is contained in $H$. Therefore
$$
U_t\succeq_t T\setminus\{g\}.
$$
Deleting at most $g$ establishes EF1 in every case.
If $d\leq q$, every type receives its global best feasible bundle using the positive-supply items. No Pareto improvement exists.
Suppose $d>q$. Then the recipients of $V_t$ consume exactly mass $q$ of item $g$.
Each such recipient holds its unique global best feasible bundle within $H\cup\{g\}$. In any weakly improving reassignment, all of that recipient’s mass must therefore retain exactly $V_t$. This fixes consumption of all supply $q$ of item $g$.
Consequently, no other positive source group can receive $g$ in a supply-feasible reassignment. All remaining groups hold $U_t$, their best feasible bundles excluding $g$. Their only weakly preferred destinations excluding $g$ are those same bundles, by strictness of the bundle order.
Zero-supply items cannot appear in any positive transfer. Hence every positive source group must retain its bundle, even when splitting among destinations is permitted. A strict improvement of positive mass is impossible.
Computing both candidate bundles for every type uses at most $2\tau m$ oracle calls. Preference comparisons and allocation in the fixed type order take polynomial time.
Only one cutoff can split a type. The resulting masses are obtained from input masses and $q$ by additions, subtractions, comparisons, and minima. Using the common denominator $D$ from Theorem 4, all output masses are integer multiples of $1/D$ and have polynomial encoding length. This completes the algorithmic proof. $\square$
Theorem 2 identifies the general search problem precisely: find an EF1-compatible positive support whose elementary-improvement graph is acyclic, together with feasible masses exhausting every elementary gain item.
I have not proved that such a support always exists, found a polynomial method to construct it, or established hardness of finding it. The polynomial verification result and the algorithm with one partially supplied item do not settle instances with different rankings and multiple partially supplied items.
⟨structured verdict parsed — rendered above⟩
The output is correct as a collection of partial results, but it does not resolve the general computational problem in USER_TASK. I found no false statement or substantive proof gap in the six numbered results. The prover accurately acknowledges the remaining limitation.
The verification below assumes throughout the input conditions in USER_TASK: finitely many item types, strict lexicographic bundle preferences, a common hereditary feasibility system, positive supported type masses, and nonnegative rational supplies.
Every reassignment can be described using finitely many transfer coordinates: there are finitely many supported source groups and finitely many feasible destination bundles. Allowing real transfer masses does not affect this finiteness.
For a changed weakly preferred destination $R$, strictness of the bundle order implies $R\succ_t S$. Its highest-ranked symmetric-difference item $g$ must belong to $R\setminus S$. Every item of $S$ ranked above $g$ belongs to $R$, so the stated inclusion
$$
E_{t,g}(S)\subseteq R
$$
is valid. Heredity establishes feasibility of the elementary destination.
Replacing $R$ by this destination preserves the source-group mass, preserves a strict improvement relative to $S$, and weakly decreases consumption of every item relative to $R$. Thus the replacement preserves aggregate supply feasibility and positive strictly improved mass.
Both directions of the lemma are established. No additional clarification is needed.
The slack-supply argument is valid. A supported elementary move has positive source mass, and the assumed slack is positive. The selected $\delta$ is therefore positive. The move gains only $g$ and releases lower-ranked source items, so the supply check is complete.
The cycle argument correctly handles repeated source groups. With $c_j$ selected moves from group $j$, the definition of $\delta$ gives
$$
c_j\delta\leq \frac{x_j}{2}\leq x_j.
$$
Consequently, all selected transfers can be made simultaneously.
Each cycle vertex is gained by exactly one selected move and released by at least its predecessor’s move, with equal transfer mass. Additional releases only decrease consumption further. Items outside the cycle are never gained. Hence all supply constraints remain satisfied, and the reassignment strictly improves positive mass.
For sufficiency, the set $B$ is nonempty because a Pareto improvement must contain a positive strictly improving transfer. Every such elementary transfer originates in the original positive support, so its gain and release relations occur in $\Gamma(x)$.
Choosing the earliest gain item $g$ in a topological ordering ensures that no positive elementary transfer releases $g$: any such transfer would gain an earlier item in $B$. Thus its consumption strictly increases from its exhausted level
$$
u_g(x)=b_g,
$$
contradicting feasibility.
The characterization covers gains that release no items, zero supplies, and arbitrary real transfer masses. No missing edge case affects the conclusion.
For a candidate with $k$ positive entries, feasibility requires checking its supported bundles, type totals, and item consumption. These checks use polynomial time in the candidate encoding length and polynomially many membership queries.
There are at most $km$ candidate elementary moves. Their feasibility answers determine both $A(x)$ and all graph edges. Recording release items may require additional polynomial computation, but no additional membership queries.
The graph has at most $m(m-1)$ distinct edges because a gained item cannot also be a released item in the same elementary move. Exact rational equality checks and directed-cycle detection take polynomial time.
When verification fails, the described constructions provide a feasible improvement using either one move or at most $m$ moves. For rational input assignments, the selected transfer masses also have polynomial encoding length.
Thus the claimed polynomial Pareto-optimality check is established.
Every elementary gain item receives positive price. By Theorem 2, such an item has exhausted supply, which proves the required implication for slack items.
For an edge $g\longrightarrow h$ with positive $p_h$, the topological ordering gives
$$
p_h\leq \frac{p_g}{m+1}.
$$
Summing over at most $m$ released items gives the stated strict positive expenditure increase. Released items outside $A(x)$ have zero price and do not invalidate the bound.
For an arbitrary feasible $R\succ_t S$, the elementary destination contained in $R$ has greater expenditure than $S$. Nonnegative prices then establish the same strict inequality for $R$.
The largest price is at most $(m+1)^{m-1}$, so the asserted per-price bit bound is valid, including the case $m=1$.
Finally, the aggregate expenditure argument correctly excludes real-valued Pareto improvements: positive strictly improved mass produces a strictly positive expenditure increase, whereas the original assignment already attains
$$
\sum_g p_gb_g.
$$
No additional clarification is needed.
The support-restricted polytope is finite-dimensional even if the original support is exponentially large. It is nonempty because it contains $x$, and it is bounded because each coordinate lies between zero and its type’s mass.
EF1 depends only on which groups have positive mass. Therefore restricting the support preserves every required EF1 comparison.
The inclusions
$$
A(y)\subseteq A(x),\qquad \Gamma(y)\subseteq\Gamma(x)
$$
follow directly from support containment. The additional equalities exhaust every item in $A(x)$, hence every item in $A(y)$. Theorem 2 therefore establishes Pareto optimality throughout the polytope.
The invoked fact that a nonempty bounded polytope has a vertex applies here. At a vertex, the active type and supply rows restricted to positive coordinates must have full column rank. Otherwise, a nonzero kernel direction gives sufficiently small feasible perturbations in both directions: positive coordinates remain positive, inactive supply inequalities retain slack, and all required equalities remain satisfied. This contradicts extremality.
There are at most $\tau+m$ such rows, so
$$
k\leq \tau+m.
$$
The rational encoding argument is also correct. The selected square matrix has entries in $\{0,1\}$, and its right-hand sides are input masses or supplies. The denominator product $D$ and the integer vector obtained after scaling have bit lengths $O(L)$. Determinant expansion gives
$$
|\det M|\leq k!,\qquad
|\det M_i|\leq k!\max_j|c_j|.
$$
Cramer’s rule therefore yields the claimed encoding bound. Reducing the resulting fractions cannot increase that bound.
The theorem establishes a polynomial-size witness, without assuming that the original real witness is available algorithmically.
For a nonempty target bundle $T$, deleting its highest-ranked item according to the comparing type produces the least-preferred permitted remainder. Compared with deleting any other item, the highest-ranked difference is the retained highest-ranked item of $T$. Compared with deleting nothing, desirability makes the deletion weakly worse.
Hence the EF1 condition is equivalent to the stated single comparison. Empty target bundles cause no difficulty because $\emptyset$ is feasible and every bundle is weakly preferred to it.
There are at most $k^2$ required comparisons. Combining this verification with the sparse witness theorem and the Pareto-optimality check proves the stated oracle-relative $\mathrm{NP}$ membership. With polynomial-time membership testing for the chosen representation of $\mathcal F$, the same certificate gives ordinary $\mathrm{NP}$ membership.
This does not establish a polynomial search algorithm or hardness. The prover explicitly makes that distinction.
The preliminary supply observation is correct:
$$
u_g(x)\leq 1.
$$
Thus supplies at least one impose no additional restriction.
The mandatory-set greedy argument is valid for an arbitrary hereditary system. At the first differing item $h$ of a purportedly better candidate, that candidate contains the mandatory set, every previously accepted item, and $h$. Heredity would make the rejected extension feasible, contradicting rejection.
With no partially supplied item, every positively allocated bundle uses only items in $H$. Each type’s best feasible subset of $H$ weakly dominates every allocated target bundle. This proves envy-freeness and hence EF1. Zero-supply items cannot occur in any positive feasible transfer, so these best bundles also exclude every Pareto improvement.
With one partially supplied item, $U_t$ and $V_t$ exhaust the possibilities for the best bundle over positive-supply items. The favorable-type definition therefore identifies exactly those types whose best such bundle contains $g$.
The allocation consumes $\min\{q,d\}$ units of $g$. Processing favorable types in a fixed order splits at most one type, yielding at most $\tau+1$ positive entries.
The EF1 argument checks every recipient category. Recipients of their global best bundle envy no allocated bundle. An unserved favorable recipient holds the best bundle excluding $g$; deleting $g$ from any target that contains it leaves a feasible subset of $H$. The required comparison follows.
If $d\leq q$, every type receives its global best available bundle. If $d>q$, all mass receiving $V_t$ must retain exactly that bundle under any weak improvement, by strictness and global optimality. This fixes all consumption $q$ of $g$. Remaining groups cannot receive $g$ and already hold their unique best bundle excluding it. Real-valued splitting cannot circumvent these restrictions.
The oracle-call bound is valid. Computing $U_t$ needs at most $m$ queries. Computing $V_t$ needs at most one singleton feasibility query and at most $m-1$ extension queries. Thus the total is at most $2\tau m$, including infeasible singletons and $m=1$.
The allocation arithmetic uses rational input values, and the common denominator argument establishes polynomial output encoding length.
The genuine progress is a polynomial verification procedure, polynomial-size existence certificates, supporting prices, and a polynomial algorithm for the specified supply restriction.
The unrestricted search problem remains unanswered. In particular, polynomial verifiability does not supply a method for discovering the required support, and the special-case algorithm does not address multiple partially supplied items with arbitrary supported rankings.
To resolve USER_TASK, a further submission must establish either a polynomial algorithm for all allowed instances, including justified handling of nonexistence, or a hardness result applicable to the stated model. No repair to the existing partial proofs is required.
⟨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.