Answer: —
Theorem 1 (Paths to stability result) — class: other
PDF text-layer excerpt — equations and symbol order may be approximateLet (PH, PC) be a problem such that for each c ∈C, Pc satisfies restricted complementarity. Let µ be an arbitrary matching for (PH, PC). 6We borrow the definition of satisfying blocking coalitions from Klaus and Klijn (2007, page 159).
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given couple types \(C\) with rational masses \(b_c\), hospital-slot types \(G\) with rational capacities \(q_g\), restricted-complementarity preferences, and an initial rational allocation \(x^0\), can one compute in time polynomial in the type support \(\tau\), input bit length \(L\), and explicit preference-list size a finite sequence of exact rational allocations from \(x^0\) to stability? Each allocation assigns mass of each couple type to ordered pairs of slot types or the outside option \(u\); each step moves positive mass from an assigned pair to a strictly preferred pair that the receiving slots can accept, displacing lower-priority incumbents as in the paper. Stability means there is no such positive-mass blocking move.
Let \(C\) be couple types with positive rational masses \(b_c\), and \(G\) hospital-slot types with positive rational capacities \(q_g\); put \(m=|G|\). A society is given by its support: the list of the \(\tau=|C|+|G|\) types with positive mass or capacity, each quantity a binary rational; \(\tau\) is the support size, not the number of possible types. Masses are not normalized. Let \(L\) be the total input bit length and \(S\) the explicit preference-list size.
Each couple has ordered spouse roles \((c,1),(c,2)\). The outside option \(u\) has unlimited capacity. Feasible pairs are \(F=(G\cup\{u\})^2\setminus\{(g,g):g\in G\}\). Each couple has a strict total order \(\succ_c\) on \(F\), and each slot type has a strict total priority order on spouse-role types and vacancy \(\varnothing\); these orders are supplied explicitly.
For \(A\subseteq F\), let \(\operatorname{Ch}_c(A)\) be the best pair in \(A\cup\{(u,u)\}\). Call \(A\) complete if it contains \((u,u)\) and, whenever \((a,b),(d,e)\in A\) and \((a,e)\in F\), it contains \((a,e)\).
Restricted complementarity means that for every complete \(A\), if \(\operatorname{Ch}_c(A)=(g_1,g_2)\), \((g_3,g_4)\in A\), and \(g_1,g_2\notin\{u,g_3,g_4\}\), then \([(g_1,g_4)\succ_c(g_3,g_4)\text{ or }(g_1,u)\succ_c(g_3,g_4)]\) and \([(g_3,g_2)\succ_c(g_3,g_4)\text{ or }(u,g_2)\succ_c(g_3,g_4)]\). All couple types satisfy this condition.
An allocation has rational entries \(x_{c,p}\geq0\), with \(\sum_{p\in F}x_{c,p}=b_c\), and total spouse mass at each \(g\) at most \(q_g\). The input includes any such initial allocation \(x^0\), possibly with unacceptable assignments.
A couple blocking move selects rational mass \(0<\delta\leq x_{c,p}\) and moves it to \(r\succ_c p\). A spouse may retain its position in the same role; otherwise each receiving position must be vacant with the incoming role ranked above \(\varnothing\), or occupied by a strictly lower-priority role. This comparison also applies when replacing the moving cohort's other spouse. Identical role types cannot displace one another. Partial moves and rational subdivision of cohorts are allowed.
The move releases the moving spouses' former positions and evicts only occupants whose positions it takes. Each evicted spouse goes to \(u\), while that spouse's partner retains its assignment; all other assignments stay fixed. Couple moves to \((u,u)\), \((p_1,u)\), or \((u,p_2)\) are included whenever strictly preferred. A hospital blocking move sends positive rational mass of an occupant ranked below \(\varnothing\) to \(u\), retaining its partner's assignment. An allocation is stable if neither kind of blocking move exists.
Does every such instance admit a finite sequence of exact rational allocations from \(x^0\) to stability, with each transition one blocking move? If so, can such a sequence be computed in time polynomial in \(m,\tau,L,S\), or is this path-construction problem NP-hard?
For finite couples and individual unit-capacity hospitals, restricted complementarity guarantees a finite blocking-coalition path from every initial matching to a stable matching ([Tello, 2023](https://www.sciencedirect.com/science/article/abs/pii/S016548962300080X)). No result settling this exact continuous path-construction problem was located.
I interpret path construction as explicitly outputting the allocations or blocking moves in the sequence.
Under this interpretation, polynomial-time path construction is impossible: the verified construction in the notes requires exponentially many moves, even with two couple types and two hospital types. I reproduce its proof below.
The new results established here are:
These results hold for arbitrary strict preference orders; restricted complementarity is not needed for them. They do not prove that every instance satisfying restricted complementarity has a path to stability, and they do not establish $\mathrm{NP}$-hardness.
Write $n=|C|$, and let
$$
R=C\times\{1,2\}
$$
be the set of spouse-role types. For an allocation $x$, define the load and vacancy at hospital type $g$ by
$$
\ell_g(x)=
\sum_{c\in C}\sum_{p\in F}\sum_{i=1}^{2}
\mathbf{1}_{\{p_i=g\}}x_{c,p},
\qquad
v_g(x)=q_g-\ell_g(x).
$$
For a role $a\in R$, say that $g$ admits $a$ at $x$ if at least one of the following holds:
This definition includes the moving cohort’s other spouse among the possible lower-priority occupants.
Lemma 1. A couple blocking move from $p$ to $r$ exists if and only if
$$
x_{c,p}>0,\qquad r\succ_c p,
$$
and, for every coordinate $i$ with $r_i\in G$ and $r_i\ne p_i$, hospital $r_i$ admits $(c,i)$.
Proof. Necessity follows from the receiving-position conditions in the task. A changed hospital assignment must use an admissible vacancy or replace a strictly lower-priority occupant.
For sufficiency, retain every hospital assignment whose coordinate is unchanged. For each changed receiving hospital, select either an admissible vacancy or one positive cohort containing a lower-priority occupant.
There are at most two receiving hospitals. Select the moving mass and, where necessary, victim masses as disjoint rational subdivisions. This is possible even when the same assignment variable supplies both the mover and victims: choose a positive rational $\delta$ smaller than one third of every positive cohort mass selected, and smaller than each selected vacancy. Distinct victim subdivisions may also be selected when both victims have the same couple type and assignment.
Move the selected source subdivision to $r$ and evict precisely the selected occupants. Every receiving comparison is strict, and retained positions require no comparison. Thus the move is legal. $\square$
Similarly, a hospital blocking move exists exactly when a positive cohort contains a spouse whom its hospital ranks below $\varnothing$.
Consequently, stability of a supplied rational allocation can be checked in polynomial time: scan its positive assignment variables, all preferred destinations, and the hospital occupancy records. This checks all one-spouse moves and all moves to the outside option.
A continuous Petri net consists of finitely many places and transitions. A marking is a nonnegative rational vector $z$. Each transition $t$ has nonnegative integer input and output vectors $\operatorname{Pre}_t$ and $\operatorname{Post}_t$. It can fire by rational amount $\delta>0$ when
$$
z\geq \delta\operatorname{Pre}_t,
$$
and then produces
$$
z+\delta(\operatorname{Post}_t-\operatorname{Pre}_t).
$$
Here the places are:
The marking corresponding to $x$ is
$$
z(x)=\bigl((x_{c,p})_{c,p},(v_g(x))_{g\in G}\bigr).
$$
Put
$$
f=|F|=m^2+m+1,\qquad d=nf.
$$
There are $d+m$ places.
For every cohort $(c,p)$ with $p_i=g$ and $(c,i)$ ranked below $\varnothing$ at $g$, include a transition consuming that cohort and producing:
Firing by amount $\delta$ is exactly a hospital blocking move of mass $\delta$.
Fix $c$, a source $p$, and a destination $r\succ_c p$. For every hospital coordinate of $r$, enumerate its possible receiving-position descriptions:
Retention is an option, not a requirement: an unchanged hospital coordinate may instead use a vacancy or replace a lower-priority occupant.
There are at most two receiving hospitals. When both victims are spouses from the same cohort, include both possibilities: they belong to one jointly evicted subdivision, or to two disjoint subdivisions.
A resulting transition consumes:
It produces:
Repeated occurrences of the same assignment place are counted with multiplicity. Thus, for example, a source subdivision and a separate victim subdivision from the same assignment variable require two units of that place.
All coefficients are at most three. There are
$$
O\bigl(nf^2(d+1)^2\bigr)
$$
couple transitions: there are at most $nf^2$ source-destination choices, at most $2d+2$ descriptions for each receiver, and only a constant number of ways to group two victims. The net therefore has polynomial size.
Lemma 2. Every firing of this net from a feasible marking is one legal blocking move. Every rational blocking move can be replaced by finitely many firings with the same final allocation.
Proof. For the first assertion, the input inequalities provide the moving subdivision, all disjoint victim subdivisions, and all required initial vacancies. Every retention or replacement comparison was checked when constructing the transition. The output records exactly the prescribed destination, victim downgrades, and released positions.
For the second assertion, consider a specified blocking move. Subdivide its moving mass according to the receiving-position descriptions just listed. Subdivide the victim masses by their couple types, assignments, and whether one or both spouses are evicted.
Because all movers have the same type, source, and destination, their selected receiving positions can be paired so that two evicted spouses who are partners are handled in the same subdivision. Positions reused from the moving mass can likewise be assigned to the corresponding homogeneous source subdivisions. These rearrangements preserve the aggregate final allocation and all priority comparisons.
Take a finite rational common refinement of these subdivisions. Each part is one enumerated transition. Process the parts in any order while reserving their originally selected vacancies and victim positions. The parts have disjoint moving and victim subdivisions; jointly evicted partners are processed together. Hence an earlier part does not remove a source or victim reserved for a later part. Every firing is legal, and their aggregate effect is the original move.
Finally, all transitions preserve couple masses and the identities
$$
v_g+\ell_g=q_g.
$$
Nonnegative reachable markings therefore correspond to feasible allocations. $\square$
By Lemma 1, a feasible allocation is stable exactly when its marking enables no net transition. Thus the original question becomes finite rational reachability to a deadlock in a polynomial-size continuous Petri net.
Write
$$
D=\operatorname{Post}-\operatorname{Pre}
$$
for the incidence matrix.
For a set $U$ of transitions and a set $H$ of places, define the forward support closure as follows. Start with $H$. Whenever a transition in $U$ has all its input places in the current set, add all its output places. Continue until no more places can be added.
Call $U$ forward fireable from $a$ if every transition in $U$ has its input support contained in the closure starting from $\operatorname{supp}(a)$.
For reverse fireability, interchange $\operatorname{Pre}$ and $\operatorname{Post}$ and start from the target support.
The following is the usual support-and-state-equation characterization of continuous reachability; it also appears as Proposition 3.4 in [Blondin and Haase](https://www.cs.ox.ac.uk/people/christoph.haase/home/publication/bh-17/bh-17.pdf). A proof is included to make the application self-contained.
Lemma 3. For nonnegative rational markings $a,b$, a finite rational firing sequence from $a$ to $b$ exists if and only if there is a nonnegative rational vector $y$, with $U=\operatorname{supp}(y)$, such that:
Proof. Necessity follows by summing the firing amounts of an actual sequence. Its used transitions pass the forward closure test; reversing the sequence passes the reverse test.
For sufficiency, first construct a forward sequence using every transition in $U$ once. Use a sufficiently small positive rational amount at each firing so that no currently positive place becomes zero. The closure condition guarantees an order in which this is possible. Its final marking is positive on every input and output place of $U$. Let its total firing vector be $\alpha$.
Construct a corresponding support-building sequence in the reverse net from $b$, with total firing vector $\beta$.
Choose rational $0<\varepsilon\leq1$ so small that
$$
\varepsilon(\alpha_t+\beta_t)<y_t
\quad\text{for every }t\in U.
$$
Scaling the forward and reverse sequences by $\varepsilon$ preserves their legality: every intermediate marking becomes a convex combination of its original marking and its starting marking.
The resulting markings
$$
A=a+\varepsilon D\alpha,\qquad
B=b-\varepsilon D\beta
$$
are positive on every place incident to $U$. Put
$$
h=y-\varepsilon(\alpha+\beta).
$$
Then $h$ is positive on $U$ and
$$
B-A=Dh.
$$
Let $I$ be the places incident to $U$, and define
$$
\eta=\min_{i\in I}\min\{A_i,B_i\}>0.
$$
Choose a positive integer $N$ such that, for every $i\in I$,
$$
\frac{
\sum_{t\in U}|D_{it}|h_t+
\max_{t\in U}\operatorname{Pre}_{it}h_t
}{N}<\eta.
$$
Starting from $A$, repeat $N$ times the same list of transitions in $U$, firing transition $t$ by $h_t/N$ each time. At the beginning of repetition $j$, the marking is
$$
A+\frac{j}{N}Dh
=
\left(1-\frac{j}{N}\right)A+\frac{j}{N}B.
$$
Every coordinate in $I$ is therefore at least $\eta$. Within a repetition, the total possible decrease before a transition, together with that transition’s required input, is bounded by the numerator in the displayed inequality divided by $N$. Every firing is consequently legal.
These repetitions reach $B$. Reversing the scaled reverse sequence then reaches $b$. All amounts are rational, and the sequence is finite. The case $U=\varnothing$ simply gives $a=b$. $\square$
The support conditions cannot be dropped. In the lower-bound construction below, setting $\varepsilon=0$ leaves no vacancy and no enabled move. The state equation nevertheless permits the flux that exchanges the two assignments.
Let $Q$ be a convex rational polyhedron of possible target markings, given by polynomially many rational linear constraints. Assume $Q$ includes nonnegativity.
Lemma 4. Whether some marking in $Q$ is finitely rationally reachable from $a$ can be decided in polynomial time.
Proof. Maintain an allowed transition set $U$, initially all transitions. Solve
$$
b\in Q,\qquad b=a+Dy,\qquad y\geq0,\qquad y_t=0\text{ for }t\notin U.
$$
If this system is infeasible, answer no.
Otherwise find a feasible pair $(\bar b,\bar y)$ whose positive support is maximal simultaneously among the coordinates of $b$ and $y$. This takes polynomially many linear programs: for each coordinate, test whether it can be positive and obtain a witness if so; average the witnesses. Nonnegativity prevents cancellation, and convexity preserves feasibility.
Put
$$
U_0=\operatorname{supp}(\bar y),\qquad
B_0=\operatorname{supp}(\bar b).
$$
Replace $U$ by the transitions in $U_0$ whose inputs pass both:
If this replacement removes no transition, Lemma 3 applies to $(\bar b,\bar y)$, so answer yes. Otherwise repeat. Every unsuccessful iteration removes a transition, so there are only polynomially many iterations.
To prove that pruning is sound, suppose an actual path to some $b^*\in Q$ uses transition set $V\subseteq U$. Its total firing vector is feasible in the linear system. Maximality of support gives
$$
V\subseteq U_0,\qquad
\operatorname{supp}(b^*)\subseteq B_0.
$$
The actual path passes the forward test, and its reversal passes the reverse test. Enlarging the transition set and starting support cannot invalidate either test. Hence no transition of $V$ is removed.
All linear programs have polynomial dimension and rational encoding length. Standard polynomial-time rational linear programming therefore gives the claimed running time. $\square$
This proof is constructive. A successful test supplies $(\bar b,\bar y)$, and Lemma 3 constructs a finite exact path.
Every stable allocation assigns zero hospital mass to roles below $\varnothing$, since otherwise a hospital blocking move exists.
For each hospital $g$, choose one of the following descriptions:
For a vector $\theta$ of such descriptions, define admission sets
$$
E_g^\theta=
\begin{cases}
\{a\in R:a\succ_g\varnothing\},&\theta_g=\star,\\
\{a\in R:a\succ_g a_g\},&\theta_g=a_g.
\end{cases}
$$
Construct a rational polyhedron $Q_\theta$ by imposing feasibility and the following conditions:
$$ r_i=u,\quad\text{or}\quad r_i=p_i,\quad\text{or}\quad (c,i)\in E_{r_i}^\theta. $$
The third condition is computed from the preference lists and $\theta$; it introduces only zero constraints.
Lemma 5.
$$
\{\text{stable allocations}\}=\bigcup_\theta Q_\theta.
$$
Proof. First let $x\in Q_\theta$. There is no hospital blocking move by condition 1.
At a hospital with description $\star$, every role actually admitted belongs to $E_g^\theta$: all occupants are acceptable, so a role that can replace one must also be acceptable.
At a hospital with threshold $a_g$, it is full and every occupant ranks at least as high as $a_g$. Any role that can replace an occupant therefore ranks strictly above $a_g$ and belongs to $E_g^\theta$.
Thus any couple blocking move from a positive source assignment would satisfy the test in condition 3, contradicting that condition. Hence $x$ is stable.
Conversely, let $x$ be stable. Use $\star$ at a hospital with positive vacancy. At a full hospital, choose $a_g$ to be its worst positive occupant role. This role exists because $q_g>0$.
For these choices, $E_g^\theta$ is exactly the set of roles admitted at $g$. Conditions 1 and 2 hold. If condition 3 failed at a positive source assignment, Lemma 1 would produce a couple blocking move. Therefore $x\in Q_\theta$. $\square$
There are at most
$$
(2n+1)^m
$$
description vectors. Each $Q_\theta$ has polynomial encoding size and can be constructed in polynomial time.
Combine Lemmas 2, 4, and 5.
For each $\theta$, test whether the marking of $x^0$ can reach $Q_\theta$. This gives a terminating decision algorithm. If any test succeeds, the constructive proof of Lemma 3 produces an exact rational blocking-move path to stability.
For fixed $m$, the number $(2n+1)^m$ of tests is polynomial. Thus finite reachability to stability is polynomial-time decidable for every fixed $m$.
For arbitrary $m$, nondeterministically guess $\theta$, using polynomially many bits, and run its polynomial-time test. Therefore the decision problem belongs to $\mathrm{NP}$.
There is also a quantitative path bound. Rational linear programming supplies the successful markings and fluxes with polynomial bit length. In Lemma 3, support-building prefixes need at most one firing per used transition. Their amounts can be chosen by repeatedly taking a fixed rational fraction of the smallest currently available input amount; this increases bit length only polynomially over the polynomially many prefix steps.
Consequently, $\varepsilon$, $A$, $B$, $h$, and $\eta$ can all have polynomial bit length. The required integer $N$ then has polynomial bit length, although its value may be exponential. The resulting path has
$$
2^{\operatorname{poly}(m,\tau,L,S)}
$$
moves at most. Its intermediate allocations also have polynomial bit length: they are obtained from polynomially many rational quantities and a repetition counter of polynomial bit length.
These are conditional construction results: they construct a path when one exists. They do not show that the test always succeeds under restricted complementarity.
Here is a complete proof of the lower bound from the notes.
Fix $k\geq1$, and put
$$
N=2^k,\qquad \varepsilon=\frac1N.
$$
Take two couple types and two hospital types, with
$$
b_{c_1}=1-\varepsilon,\qquad b_{c_2}=1,\qquad q_A=q_B=1.
$$
The couple orders are
$$
(B,u)\succ_{c_1}(A,u)\succ_{c_1}(u,u)
\succ_{c_1}(A,B)\succ_{c_1}(B,A)
\succ_{c_1}(u,A)\succ_{c_1}(u,B),
$$
and
$$
(A,u)\succ_{c_2}(B,u)\succ_{c_2}(u,u)
\succ_{c_2}(A,B)\succ_{c_2}(B,A)
\succ_{c_2}(u,A)\succ_{c_2}(u,B).
$$
The hospital priorities are
$$
(c_1,1)\succ_A(c_2,1)\succ_A\varnothing
\succ_A(c_1,2)\succ_A(c_2,2),
$$
and
$$
(c_2,1)\succ_B(c_1,1)\succ_B\varnothing
\succ_B(c_1,2)\succ_B(c_2,2).
$$
Initially,
$$
x^0_{c_1,(A,u)}=1-\varepsilon,\qquad
x^0_{c_2,(B,u)}=1.
$$
All other entries are zero.
Every complete set contains $(u,u)$. Both double-hospital pairs rank below $(u,u)$ for each couple. Thus a chosen pair always has an outside-option coordinate, making the antecedent of restricted complementarity false.
The construction satisfies the promised condition.
Every reachable cohort remains at $(A,u)$ or $(B,u)$. Indeed:
Hence no eviction is possible, and every move uses vacancy.
Write
$$
\alpha=x_{c_1,(B,u)},\qquad
\beta=x_{c_2,(A,u)}.
$$
The vacancies are
$$
v_A=\varepsilon+\alpha-\beta,\qquad
v_B=\beta-\alpha.
$$
Feasibility gives
$$
0\leq\beta-\alpha\leq\varepsilon.
$$
Neither hospital has more than $\varepsilon$ vacancy, so every move has mass at most $\varepsilon$.
If $\beta<1$ and $v_A>0$, positive $c_2$ mass at $B$ can move to $A$.
If $\beta<1$ and $v_A=0$, then $\beta-\alpha=\varepsilon$. Consequently,
$$
\alpha=\beta-\varepsilon<1-\varepsilon,
$$
and $v_B=\varepsilon>0$. Positive $c_1$ mass at $A$ can move to $B$.
Thus a reachable stable allocation must have $\beta=1$. Feasibility and the mass bound on $\alpha$ then force
$$
\alpha=1-\varepsilon.
$$
This allocation is stable because every cohort has its top pair.
Reaching stability requires increasing $\alpha$ by $(N-1)\varepsilon$ and $\beta$ by $N\varepsilon$. Each move changes only one of these quantities, by at most $\varepsilon$. Hence every path needs at least
$$
(N-1)+N=2N-1=2^{k+1}-1
$$
moves.
This bound is attained. Repeat $N-1$ times:
Then make one final $c_2$ move of mass $\varepsilon$.
Before each repetition, $\alpha=\beta$ and $A$ has vacancy $\varepsilon$. The first move transfers that vacancy to $B$; the second transfers it back. The source masses remain sufficient. The final move reaches the stable allocation.
Here $m=2$, $\tau=4$, and $S$ is constant, while $L=\Theta(k)$. Therefore an explicitly enumerated path can require $2^{\Omega(L)}$ output transitions. Polynomial-time explicit path construction is impossible, independently of any hardness assumption.
The [unit-capacity path theorem of Tello](https://www.sciencedirect.com/science/article/abs/pii/S016548962300080X) does not immediately apply through capacity cloning.
For a concrete obstruction, take two hospital types $A,B$ and a couple order placing
$$
(A,B)\succ(B,A)
$$
above all four one-spouse assignments, with all four above $(u,u)$. This satisfies restricted complementarity: with only two hospital types, the only comparison pair disjoint from a chosen double-hospital pair is $(u,u)$, and the required one-spouse assignments are acceptable.
Now clone each hospital into two positions. Preserve the original ordering of type pairs and place pairs using two copies of the same hospital type below $(u,u)$, to preserve the original prohibition.
Consider the smallest complete set containing
$$
(A_1,B_1),\qquad (B_2,A_2),\qquad (u,u).
$$
Its chosen pair is $(A_1,B_1)$. The four hospital copies are distinct, so restricted complementarity would require
$$
(A_1,A_2)\succ(B_2,A_2)
\quad\text{or}\quad
(A_1,u)\succ(B_2,A_2).
$$
Both inequalities fail under the stipulated ordering. Thus the cloned preference order does not satisfy restricted complementarity.
This is an obstruction to that proof strategy, not a counterexample to continuous reachability.
The continuous Petri-net formulation reduces universal finite reachability to a precise question: must every initial marking arising from a restricted-complementarity instance reach one of the stable polyhedra $Q_\theta$?
No argument here proves that assertion or supplies a counterexample. The exponential explicit-output lower bound is established, and the new decision upper bounds substantially constrain the remaining computational question, but neither yields an $\mathrm{NP}$-hardness reduction.
⟨structured verdict parsed — rendered above⟩
The output establishes substantial partial results, but does not resolve the full task. The explicit-output lower bound is correct. The continuous Petri-net arguments support the claimed conditional reachability results, subject to two minor clarifications. Neither universal reachability under restricted complementarity nor $\mathrm{NP}$-hardness is established.
No central mathematical assertion has been refuted.
The prover distinguishes three questions correctly:
These questions are different. A polynomial-time decision algorithm can coexist with paths that require exponentially many transitions.
Section 7 settles the explicit-output obstruction: even among instances satisfying restricted complementarity, some require exponentially many blocking moves. It therefore rules out polynomial-time construction that explicitly outputs every transition.
It does not establish $\mathrm{NP}$-hardness. The prover expressly acknowledges this limitation.
The universal existence question remains unanswered. This is a major unresolved part of the assignment, rather than a concealed error in the prover’s stated partial conclusions.
The admission definition correctly distinguishes:
Identical roles are correctly excluded from displacement.
Necessity is valid. For a changed hospital coordinate, the move must satisfy one of these receiving conditions. An unchanged coordinate may be retained without a priority comparison.
The sufficiency argument also works. Because a destination has at most two hospital coordinates, choosing sufficiently small rational mass permits disjoint mover and victim subdivisions. If one assignment variable supplies the mover and two separate victims, the stated bound
$$
3\delta<x_{c,p}
$$
ensures enough mass. Choosing $\delta$ below each selected vacancy ensures that vacancy inputs are available.
Selecting victims disjoint from the mover avoids problems caused by overlapping subdivisions. The comparison with the moving cohort’s other spouse is included in the admission test.
The hospital-move criterion is exact. Consequently, the stated polynomial-time stability check is justified: there are polynomially many assignment variables and source-destination comparisons in the explicit input parameters.
Finding: Lemma 1 is correct.
The count
$$
|F|=(m+1)^2-m=m^2+m+1
$$
is correct. Hence the number of assignment and vacancy places is polynomial.
Hospital transitions have the prescribed effect: one spouse goes to $u$, the partner stays assigned, and one unit of hospital vacancy is created per unit fired.
The couple-transition descriptions cover the relevant possibilities:
The distinction between jointly evicted partners and disjoint victim subdivisions is necessary and is included. Counting repeated assignment-place inputs with multiplicity correctly prevents using the same mass twice.
The coefficient bound of three is consistent with one source subdivision and at most two separate victim subdivisions. The transition-count bound
$$
O\!\left(nf^2(d+1)^2\right)
$$
is polynomial and sufficient.
For the first direction of Lemma 2, input availability, priority checks, and the listed outputs give a legal blocking move. The vacancy accounting is consistent: a displaced victim’s hospital position is immediately taken, whereas an unused former mover position becomes vacant.
For the converse direction, rational subdivision by receiving descriptions and joint victim status is appropriate. However, the paragraph about rearranging positions reused from the moving mass is compressed.
Minor issue: Before invoking disjoint reservations, explicitly state how positions originally supplied by another moving subdivision are represented as reuse of the corresponding mover’s own other-spouse position. The write-up should explain why this preserves the aggregate allocation, including cases where only one receiving coordinate uses such a position. This is a clarification of the stated homogeneous-cohort rearrangement, not a request for an alternative construction.
Once this identification is made explicit, the finite common refinement and reservation argument support sequential execution.
The preserved identities
$$
v_g+\ell_g=q_g
$$
and preserved couple masses ensure that reachable nonnegative markings correspond to feasible allocations.
Combining the two directions with Lemma 1 justifies identifying stable allocations with deadlocks.
Finding: The representation is sound in substance, with a minor clarification needed in the converse of Lemma 2.
The cited [Proposition 3.4 of Blondin and Haase](https://www.cs.ox.ac.uk/people/christoph.haase/home/publication/bh-17/bh-17.pdf) gives the stated characterization: the state equation must hold, and the positive flux support must be a firing set from the initial marking and from the target in the reversed net. Its hypotheses match the rational nonnegative markings and integer transition matrices used here.
The included proof is valid:
$$
\varepsilon(\alpha_t+\beta_t)<y_t
$$
makes the remaining flux positive on its support.
Places outside the incident set are unchanged. The separate treatment of empty transition support is correct.
Finding: Lemma 3 is correct, including finite rather than merely limiting reachability.
The maximal-support construction is valid. Nonnegativity ensures that averaging feasible witnesses preserves every coordinate that is positive in some witness; convexity preserves feasibility.
The pruning argument correctly uses support maximality:
$$
V\subseteq U_0,\qquad \operatorname{supp}(b^*)\subseteq B_0.
$$
Enlarging the available transition set or initial support cannot invalidate a support-closure test. Thus transitions used by an actual successful path are not pruned.
An unsuccessful iteration removes at least one transition. A successful iteration satisfies the characterization in Lemma 3. Polynomially many rational linear programs suffice.
Minor issue: The phrase “transitions … whose inputs pass both” is ambiguous. The reverse test must use the inputs of the reversed net, namely the original output support:
$$
\operatorname{supp}(\operatorname{Post}_t).
$$
It must not test $\operatorname{supp}(\operatorname{Pre}_t)$ against the reverse closure. The earlier definition of reverse fireability indicates the intended correct interpretation, but the pruning instruction should state it explicitly.
Finding: Lemma 4 is correct under the reverse-net interpretation already defined in Section 3.
Both inclusions are justified.
For $x\in Q_\theta$, unacceptable hospital occupants are excluded. At a hospital described by $\star$, any admitted role must be acceptable, so actual admission is contained in $E_g^\theta$.
At a hospital described by $a_g$, vacancy is zero and every occupant ranks at least as high as $a_g$. A role admitted by displacement must therefore rank strictly above $a_g$.
These are containment arguments; the proof does not incorrectly assume that an arbitrary threshold description gives exact admission.
Conversely, in a stable allocation:
Condition 3 then follows from Lemma 1.
The bound
$$
(2n+1)^m
$$
is correct: each hospital has at most $2n$ acceptable role descriptions and one vacancy description. Each polyhedron uses polynomially many feasibility and zero constraints.
Finding: Lemma 5 is correct.
Subject to the minor representation and reverse-test clarifications, the conclusions follow:
The quantitative argument is sound in substance. Polynomial-size rational linear systems provide polynomial-bit witnesses. The support-building sequences have polynomially many firings, and sufficiently small rational amounts can be chosen with polynomial bit growth. The resulting integer $N$ can have exponential value while retaining polynomial bit length.
The repeated bridge uses a fixed finite list and a polynomial-bit repetition counter, so exponentially many intermediate allocations need not individually have exponential encoding length.
These conclusions concern existence and construction when a path exists. They do not show that restricted complementarity makes every test succeed.
This part checks out completely.
The displayed orders contain all seven feasible pairs for two hospitals. The masses are positive for every $k\geq1$, and the initial allocation is feasible.
Restricted complementarity holds because every complete set contains $(u,u)$, and both double-hospital pairs rank below it. Thus the chosen pair always contains $u$, making the antecedent false.
The reachable-state invariant is correct. Only spouse-role $1$ occupies hospitals, and both such roles are acceptable. The only improving moves are the stated transfers. At each destination, the incoming role cannot displace either the resident higher-priority role or an identical role. Therefore every move consumes vacancy and creates no victims.
The vacancy calculation is correct:
$$
v_A=\varepsilon+\alpha-\beta,\qquad
v_B=\beta-\alpha.
$$
Feasibility gives
$$
0\leq\beta-\alpha\leq\varepsilon,
$$
so every move has mass at most $\varepsilon$.
The stability argument covers both possible values of $v_A$ when $\beta<1$. Hence stability requires
$$
\beta=1,\qquad \alpha=1-\varepsilon.
$$
Both types then have their top pair.
The required total increases and per-move bounds yield
$$
2N-1=2^{k+1}-1
$$
moves. The alternating construction attains this bound, including the case $k=1$.
With constant support and preference sizes and $L=\Theta(k)$, the explicit-output lower bound is valid.
Finding: Polynomial-time explicit enumeration of a path is unconditionally impossible in general. This is an output-length lower bound, not a hardness reduction.
The original two-hospital preference order satisfies restricted complementarity for the reason stated: the only pair disjoint from a chosen double-hospital pair is $(u,u)$, and the relevant one-spouse pairs rank above it.
In the cloned complete set, the generated same-type cross pair is feasible at the clone level but ranks below $(u,u)$. The stated one-spouse alternative also ranks below the comparison double-hospital pair. Thus the required disjunction fails.
Finding: This correctly defeats the specified cloning strategy. It establishes neither failure of every cloning strategy nor a counterexample to continuous reachability, and the prover does not claim otherwise.
The next write-up should clarify the moving-subdivision rearrangement in Lemma 2 and explicitly use original output supports in the reverse pruning test.
To resolve USER_TASK, a further argument must establish universal finite reachability under restricted complementarity or provide a counterexample. The current output provides neither. Any $\mathrm{NP}$-hardness claim would also require a separate reduction; the exponential path-length example does not supply one.
⟨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.