Answer: —
Theorem 3.5 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateGiven a fair division instance with an identical mono- tone valuation 𝑣, and any near-EF1 allocation 𝑋, the EF1-Restoration problem always admits a positive solution. Moreover, it is possible to ensure that the unhappy agent 1 is the only recipient in each of these valid transfers, and the transfer is always made from an agent 𝑖 whom agent 1 EF1-envies (i.e., 𝜀1→𝑖> 0). Furthermore, if 𝑣 is additive, at most 𝑚/𝑛 valid transfers to agent 1 suffice to reach an EF1 allocation. This is tight in the worst case.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given finite \(Q\), common monotone valuation \(v:2^Q\to\mathbb{Q}_{\ge 0}\), per-capita copy supply \(\beta\in[0,1]^Q\), and masses \(\lambda^\sigma_B\) of agent types \((\sigma,B)\) with \(\sigma\in\{U,O\}\), decide whether a finite sequence of aggregate transfers of mass \(\delta\) can move an item class \(q\in D\setminus B\) from ordinary agents holding \(D\) to marked agents holding \(B\), preserve the copy-supply constraints, maintain near-EF1 at every intermediate state, and reach an EF1 state without increasing the marked cohort's EF1-envy.
Let \(Q\) be a set of \(m\) item classes; bundles are subsets of \(Q\), with at most one copy of each class per person. All people share a monotone valuation \(v:2^Q\to\mathbb{Q}_{\ge0}\), given by its complete binary-rational table, with \(v(\varnothing)=0\).
A society is given by its support: the list of the \(\tau\) types \((\sigma,B)\) with positive binary-rational mass \(\lambda_B^\sigma\), where \(\sigma\in\{U,O\}\) denotes a permanent marked or ordinary cohort. Here \(\tau\) is the support size, not the number of possible types. Masses sum to \(1\), and both cohorts have positive mass.
The binary-rational supply vector \(\beta\in[0,1]^Q\) satisfies \(\sum_{\sigma,B:q\in B}\lambda_B^\sigma=\beta_q\) for every \(q\); these equalities must hold throughout.
Define \(h(D)=\min_{q\in D}v(D\setminus\{q\})\) for nonempty \(D\), and \(h(\varnothing)=0\). For bundles \(B,D\), put \(e(B,D)=\max\{0,h(D)-v(B)\}\). Near-EF1 means \(e(B,D)=0\) whenever \((O,B)\) and either-cohort bundle \(D\) have positive mass; EF1 imposes this also on marked types. The initial state is promised near-EF1.
An aggregate transfer chooses \(q\in D\setminus B\) and a real \(0<\delta\le\min\{\lambda_D^O,\lambda_B^U\}\), replacing mass \(\delta\) of \((O,D)\) by \((O,D\setminus\{q\})\) and mass \(\delta\) of \((U,B)\) by \((U,B\cup\{q\})\).
Interpret masses as an atomless population with persistent individual identities; each transfer selects the indicated subcohorts. At every resulting state, require near-EF1 and, for almost every ordered pair of distinct individuals with marked first member, require their value of \(e\) not to increase from the preceding state. Comparisons include marked recipients as possible envied individuals.
The decision problem asks whether some finite sequence of these transfers reaches EF1; the empty sequence is allowed.
Is this continuous EF1-restoration decision problem in \(\mathrm{P}\), or is it \(\mathrm{NP}\)-hard? State running times in \(m\), initial support size \(\tau\), and total input bit length \(L\).
For discrete societies with identical monotone goods valuations, restoration from any near-EF1 allocation is polynomial-time computable using only transfers to the designated unhappy agent. [Source](https://ifaamas.csc.liv.ac.uk/Proceedings/aamas2025/pdfs/p472.pdf)
A later full version also establishes polynomial-time restoration from arbitrary discrete allocations under its clarified valid-transfer convention. No result settling this exact mass-transfer problem was located. [Source](https://arxiv.org/html/2410.14421v4)
The general classification remains unresolved here: I do not prove either membership in $\mathrm{P}$ or $\mathrm{NP}$-hardness.
I establish two additional results beyond the supplied notes:
All arguments below apply to the permanent cohorts and persistent identities specified in the question.
Put $N=2^m$. For a state $x$, write $x_A^\sigma$ for the mass of type $(\sigma,A)$, and define
$$
s(x)=\min\{v(A):x_A^U>0\},
\qquad
H(x)=\max\{h(A):x_A^U+x_A^O>0\}.
$$
Both extrema exist because both cohorts have positive mass.
Near-EF1 is equivalent to
$$
v(A)\ge H(x)
\quad\text{for every supported ordinary bundle }A.
$$
Indeed, the comparisons required of an ordinary holder of $A$ are exactly $v(A)\ge h(D)$ for every supported bundle $D$. Consequently, in a near-EF1 state,
$$
x\text{ is EF1}\quad\Longleftrightarrow\quad s(x)\ge H(x).
$$
For every bundle $A$, monotonicity of $v$ gives $h(A)\le v(A)$.
Also, $h$ is monotone under inclusion. To prove this, let $A\subseteq D$. The case $A=\varnothing$ follows from nonnegativity. Otherwise, for every $q\in D$:
$$ v(D\setminus\{q\})\ge v(A\setminus\{q\})\ge h(A). $$
$$ v(D\setminus\{q\})\ge v(A)\ge h(A). $$
Taking the minimum over $q\in D$ proves $h(D)\ge h(A)$.
For a proposed transfer of $q\in D\setminus B$, set
$$
E=D\setminus\{q\},
\qquad C=B\cup\{q\}.
$$
We have
$$
h(E)\le h(D),\qquad
h(B)\le h(C)\le v(B),\qquad
v(C)\ge v(B).
$$
The upper bound $h(C)\le v(B)$ follows by removing $q$ from $C$.
Proposition 1. Suppose $x$ is near-EF1 but not EF1. Write $s=s(x)$ and $H=H(x)$, so $s<H$. For every permitted positive amount, the proposed transfer is valid exactly when
$$
v(E)\ge H
\quad\text{and}\quad
\bigl(h(C)=h(B)\ \text{or}\ h(C)\le s\bigr).
$$
In particular, validity is independent of whether the amount exhausts either input type.
Proof: necessity of the recipient condition. Suppose
$$
h(C)>h(B)\quad\text{and}\quad h(C)>s.
$$
Since $h(C)\le v(B)$, necessarily $v(B)>s$. Choose a supported marked type $A$ with $v(A)=s$. Its individuals are not recipients because their bundle differs from $B$.
For every such individual and every selected recipient, envy changes from
$$
\max\{0,h(B)-s\}
\quad\text{to}\quad
\max\{0,h(C)-s\}.
$$
This is a strict increase. The two populations are disjoint and have positive mass, so these violating ordered pairs have positive product measure. Thus the required almost-everywhere condition fails.
Proof: necessity of the donor condition. If $h(D)=H$, the definition of $h$ directly gives
$$
v(E)\ge h(D)=H.
$$
If $h(D)<H$, some other supported type attains $H$. An ordinary maximizer is unchanged. A marked maximizer is either unchanged or receives an item; in the latter case its $h$ cannot decrease. Therefore the resulting maximum supported $h$ is at least $H$. The selected ordinary donors afterward hold $E$ with positive mass, so near-EF1 requires $v(E)\ge H$.
Proof: sufficiency. Assume both conditions hold. We check all comparisons with a marked first individual.
This covers every required ordered-pair case, including the case omitted in the supplied notes.
Every resulting bundle has $h$ at most $H$: this follows from monotonicity for donors and from the recipient condition for recipients. Every unchanged ordinary bundle retains value at least $H$, and selected donors have value $v(E)\ge H$. Thus near-EF1 is preserved. $\square$
Each transfer also preserves cohort masses and every supply equality: ownership of $q$ decreases by the same amount in the ordinary cohort as it increases in the marked cohort; other ownership quantities are unchanged.
Fix $s<H$. Call a state admissible for $(s,H)$ if:
$$ \begin{aligned} h(A)&\le H &&\text{for every supported bundle }A,\\ v(A)&\ge H &&\text{for every supported ordinary bundle }A,\\ v(A)&\ge s &&\text{for every supported marked bundle }A. \end{aligned} $$
Call a transfer a phase transfer for $(s,H)$ if it satisfies
$$
v(D\setminus\{q\})\ge H,
\qquad
h(B\cup\{q\})=h(B)\ \text{or}\ h(B\cup\{q\})\le s.
$$
The sufficiency proof above uses only these bounds, not equality with the actual extrema. Therefore:
Lemma 2. Every phase transfer from an admissible state is valid and leaves the state admissible.
This remains true if the actual state has already become EF1.
Define two relations on bundles:
$$
\mathcal R_U(s)=
\{(B,C): B\subseteq C,\
h(C)=h(B)\ \text{or}\ h(C)\le s\},
$$
and
$$
\mathcal R_O(H)=
\{(D,E): E\subseteq D,\ v(E)\ge H\}.
$$
The following theorem describes fixed-phase reachability solely through masses assigned to initial and final bundles.
Theorem 3. Let $x,y$ be admissible states for fixed $s<H$. A finite sequence of phase transfers takes $x$ to $y$ if and only if there are nonnegative arrays
$$
(\alpha_{BC})_{(B,C)\in\mathcal R_U(s)},
\qquad
(\gamma_{DE})_{(D,E)\in\mathcal R_O(H)}
$$
satisfying the marginal equations
$$
\begin{aligned}
\sum_{C:(B,C)\in\mathcal R_U(s)}\alpha_{BC}&=x_B^U,\\
\sum_{B:(B,C)\in\mathcal R_U(s)}\alpha_{BC}&=y_C^U,\\
\sum_{E:(D,E)\in\mathcal R_O(H)}\gamma_{DE}&=x_D^O,\\
\sum_{D:(D,E)\in\mathcal R_O(H)}\gamma_{DE}&=y_E^O,
\end{aligned}
$$
and, for every $q\in Q$, the item-balance equation
$$
\sum_{(B,C)\in\mathcal R_U(s):\,q\in C\setminus B}\alpha_{BC}
=
\sum_{(D,E)\in\mathcal R_O(H):\,q\in D\setminus E}\gamma_{DE}.
$$
Moreover, any feasible arrays can be implemented using at most $2m4^m$ transfers.
Take a finite phase-transfer sequence. Partition marked individuals according to their initial bundle $B$ and final bundle $C$, and let the mass of each part be $\alpha_{BC}$. Define $\gamma_{DE}$ similarly for ordinary individuals.
Marked bundles only grow, so $B\subseteq C$. If $h(B)>s$, every addition must preserve $h$, because an increase satisfying the phase rule would have to end at an $h$-value at most $s$. Thus $h(C)=h(B)$.
If $h(B)\le s$, every subsequent $h$-value remains at most $s$: the phase rule allows either no increase or an increase ending at most $s$. Thus $h(C)\le s$. This proves $(B,C)\in\mathcal R_U(s)$.
Ordinary bundles only shrink, so $E\subseteq D$. Their final values are at least $H$ by admissibility. Hence $(D,E)\in\mathcal R_O(H)$.
The marginal equations express the initial and final masses. For each item, the mass removed from ordinary individuals equals the mass added to marked individuals, proving the balance equations.
Use atomlessness to partition each initial marked type into groups of masses $\alpha_{BC}$, with assigned final bundle $C$. Partition each ordinary type using $\gamma_{DE}$, with assigned final bundle $E$.
Fix an order of the item classes. Process each class $q$ as follows:
The item-balance equation makes their total masses equal. Previous processing of other classes does not change whether $q$ is present, so every selected donor contains $q$ and every selected recipient lacks $q$.
It remains to verify validity. Consider a marked individual with initial bundle $B$, assigned final bundle $C$, and current bundle $A$. Throughout the construction,
$$
B\subseteq A\subseteq C.
$$
If $h(C)\le s$, then
$$
h(A\cup\{q\})\le h(C)\le s.
$$
If $h(C)=h(B)$, monotonicity gives
$$
h(B)\le h(A)\le h(A\cup\{q\})\le h(C)=h(B),
$$
so the addition preserves $h$.
Likewise, an ordinary individual with assigned final bundle $E$ and current bundle $F$ retains $E$ after any assigned removal. Hence
$$
v(F\setminus\{q\})\ge v(E)\ge H.
$$
Every constructed transfer is therefore a phase transfer. Lemma 2 proves validity and preservation of admissibility.
After all classes have been processed, every individual holds its assigned final bundle. The marginal equations then give exactly state $y$.
Groups may be tracked by their initial, current, and assigned final bundles.
For marked individuals these triples satisfy $B\subseteq A\subseteq C$. Each item has four possible positions in such a triple, so there are at most $4^m$ triples. Ordinary triples $E\subseteq F\subseteq D$ have the same bound. Groups with identical triples can be merged.
While processing a fixed class $q$, use the smaller of the two matched pending-group masses as the transfer amount. Each transfer exhausts at least one pending group. Its output groups no longer require processing $q$, so no new pending group for $q$ is created.
Thus at most $2\cdot4^m$ transfers process one class, and at most $2m4^m$ process the phase. $\square$
For prescribed rational endpoints, Theorem 3 is a rational linear feasibility problem with at most $2\cdot3^m$ transport variables: there are exactly $3^m$ ordered subset pairs.
During valid transfers before restoration, $s(x)$ cannot decrease because marked individuals only gain items. Proposition 1 shows that $H(x)$ cannot increase.
Let
$$
\mathcal V=\{v(A):A\subseteq Q\},
\qquad M=|\mathcal V|\le N.
$$
Both thresholds belong to this same set. For $s$ this is immediate. For nonempty $D$, the minimum defining $h(D)$ is attained at some table entry; also $h(\varnothing)=v(\varnothing)=0$.
Rank the distinct values increasingly, using integer ranks. In a non-EF1 state, the integer
$$
g(x)=\operatorname{rank}(H(x))-\operatorname{rank}(s(x))
$$
is positive. Whenever the threshold pair changes before restoration, $g$ decreases by at least one.
Stop a successful sequence at its first EF1 state and group transfers by the threshold pair in their preceding states. Therefore the number $K$ of phases satisfies
$$
K\le g(x_{\mathrm{initial}})\le M-1\le N-1.
$$
If the initial state is EF1, no phase is needed.
For a non-EF1 initial state, guess:
Check that both boundary supports of phase $i$ are admissible for $(s_i,H_i)$. Check that the terminal support is EF1:
$$
v(B)\ge h(D)
\quad\text{for every two supported terminal bundles }B,D.
$$
Now form one linear program. Its variables are the boundary states $x_0,\ldots,x_K$ and the transport arrays of Theorem 3 for each phase. Require:
To impose the last condition, introduce $0\le\varepsilon\le1$. Set absent coordinates to zero, require every designated present coordinate to be at least $\varepsilon$, and maximize $\varepsilon$.
The guessed strict-support system is feasible exactly when the optimum is positive. Indeed, finitely many positive coordinates have a positive minimum; conversely, positive $\varepsilon$ ensures every designated coordinate is positive.
All masses and transport variables are bounded by $1$ through their marginal equations, so this linear program has a bounded feasible region. Rational linear programming decides whether its optimum is positive in polynomial time and supplies a rational solution of polynomial bit length.
Suppose some finite real-amount sequence succeeds. Partition it into its threshold phases as above and guess their thresholds and boundary supports.
Proposition 1 places every transfer of a phase under its fixed phase rule. Theorem 3 supplies real transport arrays satisfying all phase equations. The boundary coordinates designated present are positive, so the linear program has positive optimum.
Thus the verifier accepts. No prior rationalization of the original sequence is needed.
If the verifier accepts, its rational solution gives admissible boundary states and feasible transport arrays. Theorem 3 constructs a valid finite sequence for each phase. Concatenation preserves the supply equalities, cohort identities, near-EF1, and every required marked-pair comparison. The terminal state is EF1.
The constructed sequence has at most
$$
2m4^mK\le 2m4^m(2^m-1)=O(m8^m)
$$
transfers.
These transfers can use rational amounts of polynomial bit length. To see this explicitly, put the finitely many rational transport entries over a common denominator. Its bit length is at most the sum of their denominator bit lengths, hence polynomial in the linear-program encoding size. The matching construction uses only minima, additions, and subtractions of these masses, so all resulting amounts retain this denominator and polynomial bit length.
Therefore:
$$
\boxed{\text{The general decision problem belongs to }\mathrm{NP}.}
$$
More strongly, every yes-instance has a polynomial-length rational restoration witness, measured in the complete-table input length.
Computing all $h$-values and sorting the valuation values takes $O(m2^m)$ rational comparisons and table operations. Reading bundle incidences in the initial support takes $O(m\tau)$ operations.
There are $O(2^m)$ phases and $O(3^m)$ transport variables per phase. Each transport variable occurs in two marginal equations and at most $m$ item-balance equations. A conservative bound for the linear-program encoding size is
$$
B=O\!\left(L+m\tau+m^2 6^m\right).
$$
Thresholds can be represented by table-value indices; their rational values need not be repeated in the linear-program coefficients.
The nondeterministic running time is
$$
\left(L+m\tau+m^2 6^m\right)^{O(1)}.
$$
Since the complete valuation table is supplied, $2^m\le O(L)$, making this polynomial in $L$.
The support guesses use $O(4^m)$ bits and the threshold guesses use $O(m2^m)$ bits. Exhaustive enumeration consequently gives the deterministic upper bound
$$
2^{O(4^m+m2^m)}
\left(L+m\tau+m^2 6^m\right)^{O(1)}.
$$
This is not a polynomial-time classification.
Assume additionally that
$$
v(A)=f(|A|),
\qquad
0=f(0)<f(1)<\cdots<f(m).
$$
The function values are rational. This includes equal positive additive item values.
Write the cardinality masses as
$$
\mu_j=\sum_{|B|=j}x_B^U,
\qquad
\nu_j=\sum_{|D|=j}x_D^O.
$$
Define
$$
r=\min\{j:\mu_j>0\},
\qquad
k=\max\{j:\mu_j+\nu_j>0\}.
$$
If $k=0$, the state is EF1. If $k\ge1$, then
$$
s=f(r),\qquad H=f(k-1),
$$
because every nonempty bundle of size $j$ has $h=f(j-1)$.
Strict increase gives
$$
\text{EF1}\quad\Longleftrightarrow\quad r\ge k-1.
$$
Suppose the state is not EF1. Then $k\ge2$ and $r\le k-2$.
Let a proposed donor have size $d$ and its recipient size $b$. The donor condition of Proposition 1 becomes
$$
f(d-1)\ge f(k-1),
$$
so $d\ge k$. Since $k$ is the largest supported size, necessarily $d=k$.
If $b\ge1$, then
$$
h(B\cup\{q\})=f(b)>f(b-1)=h(B).
$$
The recipient condition therefore requires $f(b)\le f(r)$, hence $b\le r$. Since every marked bundle has size at least $r$, necessarily $b=r$.
If $b=0$, then necessarily $r=0$, and the recipient condition holds because both the empty bundle and its singleton extension have $h=0$.
Thus every valid transfer has:
Conversely, every such pair permits a valid transfer. Since $k>r$, the donor has an item absent from the recipient. Its remainder has value $f(k-1)=H$, and the recipient’s new $h$ is $f(r)=s$.
Item identities therefore impose no additional restriction on the existence of a transfer in this case.
Repeat the following procedure.
$$
w=\min\{\mu_r,\nu_k\}
$$
and update
$$
\begin{aligned}
\mu_r&\gets\mu_r-w,&
\mu_{r+1}&\gets\mu_{r+1}+w,\\
\nu_k&\gets\nu_k-w,&
\nu_{k-1}&\gets\nu_{k-1}+w.
\end{aligned}
$$
Recompute $r,k$.
The update can be implemented by matching actual supported donor and recipient types and choosing any available item.
Fix a non-EF1 state with cardinalities $r,k$.
Every valid transfer must move mass from the same two cardinality bins, $\nu_k$ and $\mu_r$. Until their total transferred mass reaches
$$
w=\min\{\mu_r,\nu_k\},
$$
both source bins remain positive.
Throughout that interval, $r$ remains unchanged. Also, $k$ remains unchanged: the donor bin at size $k$ remains positive, and recipients acquire size
$$
r+1\le k-1,
$$
so they cannot create a larger size.
Consequently, the state cannot become EF1 before total amount $w$ has been transferred. At total amount $w$, the cardinality distribution is exactly the algorithm’s updated distribution, regardless of transfer amounts, item choices, and the selected identities.
If the state remains non-EF1 and $\nu_k=0$, no valid donor exists, so restoration is impossible. Otherwise, the same argument applies to the next update.
Induction proves that the algorithm accepts exactly the restorable instances in this subclass.
Each update exhausts at least one source bin.
The minimum marked size increases at most $m$ times, and the global maximum decreases at most $m$ times. Hence there are at most $2m+1$ updates.
Recognizing this valuation subclass and deciding its instances takes
$$
\left(L+m\tau+m2^m\right)^{O(1)}
$$
bit operations. After forming the cardinality masses, the decision procedure itself uses $O(m)$ rational updates.
A successful sequence can also be constructed. Within one update, no new source bundle of size $r$ or $k$ is created. Matching actual types while exhausting one source at each transfer therefore needs at most $2N+1$ transfers per update. The whole restoration uses $O(m2^m)$ transfers, with rational amounts of polynomial bit length.
Let $Q=\{a,b\}$, $v(A)=|A|$, and
$$
\lambda_\varnothing^U=\tfrac14,\qquad
\lambda_{\{a,b\}}^U=\tfrac14,\qquad
\lambda_{\{a\}}^O=\tfrac12.
$$
The supplies are
$$
\beta_a=\tfrac34,\qquad \beta_b=\tfrac14.
$$
Here $H=1$, and the ordinary singleton has value $1$, so the initial state is near-EF1. It is not EF1 because marked empty-bundle holders envy the marked full-bundle holders.
The cardinalities are $r=0$, $k=2$, and $\nu_2=0$. Thus the algorithm correctly rejects. Directly, the only possible donor is the ordinary singleton, whose transfer would leave value $0<H$.
This confirms that even the polynomially solvable subclass contains genuine negative instances.
The fixed-phase transport theorem removes the need to guess transition supports or verify continuous Petri-net fireability. It also proves that arbitrarily long real-amount sequences are unnecessary for witnessing restoration.
What remains is coordination across threshold phases. The certificate chooses their order and the boundary supports; the present argument enumerates those choices. I have not shown how to eliminate that enumeration in polynomial time, nor how to use it in an $\mathrm{NP}$-hardness reduction.
⟨structured verdict parsed — rendered above⟩
The output is a correct partial resolution. The transfer criterion, fixed-phase characterization, polynomial witness bound, and cardinality algorithm stand up to verification. However, the general classification requested in USER_TASK remains unresolved: membership in $\mathrm{NP}$ does not establish either membership in $\mathrm{P}$ or $\mathrm{NP}$-hardness.
The definitions of $s(x)$ and $H(x)$ are well posed. Both cohorts have positive mass, and there are finitely many possible bundles.
The equivalences
$$
\text{near-EF1}\iff v(A)\ge H(x)\text{ for every supported ordinary bundle }A
$$
and, in a near-EF1 state,
$$
\text{EF1}\iff s(x)\ge H(x)
$$
correctly capture the task’s comparisons, including comparisons against marked individuals.
The proof that $h(A)\le v(A)$ is correct, including the empty bundle.
The inclusion-monotonicity proof checks both possibilities for a removed item and handles the empty bundle separately. Consequently, all three bounds used for a transfer are justified:
$$
h(E)\le h(D),\qquad h(B)\le h(C)\le v(B),\qquad v(C)\ge v(B).
$$
The recipient-condition argument is sound. If
$$
h(C)>h(B)\quad\text{and}\quad h(C)>s,
$$
then $h(C)\le v(B)$ implies $v(B)>s$. Thus a marked type attaining $s$ differs from the recipient type. Its positive-mass population is disjoint from the positive-mass selected recipient population. The asserted strict increase therefore occurs on a positive-measure set of ordered pairs of distinct individuals.
The donor-condition argument also covers exhaustion correctly:
Thus the resulting maximum is at least $H$, and the positive-mass selected donors must have value at least $H$ afterward.
The listed cases exhaust the possible required comparisons. In particular, comparisons between selected marked recipients are correctly included: their common bundles before and after the transfer give zero envy.
The near-EF1 check is also valid. The recipient condition ensures $h(C)\le H$, and donor remainders have $h(E)\le H$. Every resulting ordinary bundle has value at least $H$.
Accordingly, the criterion is exact for a near-EF1, non-EF1 preceding state, and its independence from the transfer amount is established.
The supply and cohort-mass preservation statements are correct.
The extension to admissible states is justified. The sufficiency proof needs only the stated threshold bounds, rather than equality with the actual extrema. It therefore remains applicable when the actual state is already EF1.
Finding: No mathematical issue in Section 1.
The initial-to-final transport arrays are well defined by the finite sequence and persistent identities.
The marked relation is justified in both cases:
Ordinary bundles only shrink and retain value at least $H$. The marginal and item-balance equations follow from the individual trajectories and transfer conservation.
The construction respects the original transfer model. Atomlessness permits the finite partitions and subsequent subdivisions. Processing other items does not affect whether the current item is present.
For each selected marked group, its current bundle lies between its assigned endpoints. The two alternatives in $\mathcal R_U(s)$ therefore imply the required one-item phase condition. For each ordinary group, the assigned final bundle remains contained in the donor’s remainder, giving the donor-value bound.
Each matching operation selects subcohorts with definite current bundles. Lemma 2 establishes validity at every resulting state. The construction consequently implements the prescribed transport arrays with persistent identities.
The count of $4^m$ possible nested triples per cohort is correct. For each item, a transfer exhausts at least one pending group, and its outputs do not remain pending for that item. Hence the bound
$$
2m4^m
$$
is valid.
There are $3^m$ ordered subset pairs, so the stated upper bound of $2\cdot3^m$ transport variables is also correct.
Finding: Theorem 3 is established as written.
Marked values cannot decrease. Proposition 1 prevents $H(x)$ from increasing before restoration.
Both extrema are valuation-table values, including $h(\varnothing)=0$. Whenever the threshold pair changes and the resulting state remains non-EF1, the positive integer rank gap strictly decreases.
Stopping at the first EF1 state therefore gives
$$
K\le M-1\le 2^m-1.
$$
The initial-EF1 case is separately covered by the empty sequence.
The guessed supports and threshold pairs have polynomial size in the complete-table input length.
The common $\varepsilon$ construction correctly expresses exact support: finitely many strictly positive designated coordinates have a positive minimum. Conversely, a positive feasible $\varepsilon$ forces every designated coordinate to be positive.
The boundedness assertion is justified by the marginal equations and the initial total mass. These equations preserve cohort masses between boundaries and bound every transport entry by $1$.
The rational linear-programming claim applies to this finite system with rational coefficients and rational objective. Its feasibility and optimal-value comparison can be decided in polynomial time, with a polynomial-bit rational solution when the optimum is positive.
Completeness correctly uses the original real witness only to supply feasible boundary states and transport arrays. No unsupported rationalization of that witness is assumed.
Soundness follows from Theorem 3 and Lemma 2. Adjacent phases share boundary states, so their individual implementations concatenate. Supply equalities are preserved automatically.
The common-denominator argument establishes polynomial-bit rational transfer amounts. The transfer count
$$
O(m8^m)
$$
is polynomial in the complete-table input length.
The stated bounds are consistent:
Because the complete valuation table is supplied, these nondeterministic bounds are polynomial in $L$.
Finding: Membership in $\mathrm{NP}$ and the polynomial-size rational witness result are proved. They do not settle the requested general classification.
The identities
$$
s=f(r),\qquad H=f(k-1)
$$
are correct for $k\ge1$. The case $k=0$ is handled separately.
In a non-EF1 state, Proposition 1 forces every donor to have size $k$ and every marked recipient to have size $r$. The separate treatment of empty recipients correctly handles the equality
$$
h(\varnothing)=h(\{q\})=0.
$$
Conversely, every such donor-recipient pair admits an item transfer: $k>r$ ensures an available item, and the resulting bundles satisfy both validity conditions. Thus item identities introduce no additional feasibility restriction within this subclass.
Before either source bin is exhausted, both $r$ and $k$ remain unchanged. Hence restoration cannot occur before the accumulated transferred mass reaches
$$
w=\min\{\mu_r,\nu_k\}.
$$
At that point the updated cardinality distribution is independent of all transfer choices. This justifies the induction and the rejection condition when $\nu_k=0$.
Each update either increases the minimum marked size, decreases the maximum size, or leaves a marked maximum-size holder with no remaining ordinary donor at that size. The last case causes acceptance or rejection at the next iteration.
The update and transfer-count bounds are valid. Rational arithmetic remains of polynomial bit length.
The negative example satisfies the supply equalities and near-EF1 promise. Its non-restorability follows from the absence of an ordinary size-$2$ donor.
Finding: Polynomial-time solvability of the stated subclass is proved.
Major issue — the requested general classification is not supplied. This is an acknowledged incompleteness, rather than a false mathematical step. The polynomial algorithm requires strictly increasing cardinality valuations, while USER_TASK permits arbitrary identical monotone valuations.
To resolve the assignment, the prover must supply either a deterministic polynomial-time algorithm for the general input model, with its correctness and running-time proof, or an $\mathrm{NP}$-hardness reduction satisfying the task’s promises and transfer conventions. Neither follows from the current results.
No other major or minor mathematical issues were found. The established results are substantive, and the direction is worth another round.
⟨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.