Answer: An explicit finite improvement sequence to a stable competitive equilibrium is constructible in time polynomial in $m,\tau,K,L$, allowing the unilateral dissolutions expressly permitted in the task.
Proposition 1 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateConsider a labor market (F, W, V ) with an arbitrary initial market state (µ0, u0). There exists a finite sequence of successive pair improvements which leads (µ0, u0) to a competitive equilibrium.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given firm and worker type sets \(I,J\), rational type masses, integer pair surpluses and outside options, and a feasible initial matching represented by \(K\) state-cohort classes with integral payoffs, can an algorithm polynomial in \(|I|+|J|+K+L\) output a finite sequence of pair improvements ending in a stable competitive equilibrium? Here \(L\) is the input bit length; each move transfers equal rational mass between cohorts not currently paired with each other, gives the newly matched agents integral payoffs that weakly improve both and strictly improve one, and returns abandoned partners to their outside options.
Let \(I,J\) be disjoint, nonempty finite sets of firm and worker types. A society is given by its support: the \(\tau=|I|+|J|\) types with positive mass, each mass a binary rational; \(\tau\) counts supported types, not possible types. Masses need not sum to one, and the two sides may have unequal total mass. Each type is an atomless population. Pair surpluses \(v_{ij}\) and outside options \(a_i,b_j\) are arbitrary integers.
A state is a finite list of matched-cohort records \((i,j,h,p,q)\), with rational mass \(h>0\), integral per-agent payoffs \(p,q\), and \(p+q=v_{ij}\), together with unmatched-cohort records paying the relevant outside option. Records account for every type's full mass; each agent has at most one partner. The initial state has \(K\) records and need not be individually rational. Let \(L\) be the total binary input length.
A pair improvement selects equal positive rational masses from a firm cohort and a worker cohort whose selected agents are not currently partners, matches them with integral payoffs weakly improving both and strictly improving at least one, and returns their abandoned partners to their outside options. A unilateral improvement may instead dissolve positive rational mass of matches when the initiating cohort strictly prefers its outside option; both former partners become unmatched. Cohorts may split or merge, and all other agents retain their matches and payoffs.
A state is a stable competitive equilibrium if every cohort receives at least its outside option and \(p+q\ge v_{ij}\) for every positive-mass firm cohort of type \(i\) with payoff \(p\) and worker cohort of type \(j\) with payoff \(q\).
Can an explicit finite sequence of pair improvements from any feasible initial state to a stable competitive equilibrium be constructed in time polynomial in \(m,\tau,K,L\), where \(m=|I|+|J|\), or is this construction problem NP-hard?
For finite agents, [Chen, Fujishige and Yang (2016)](https://eprints.whiterose.ac.uk/id/eprint/99299/1/CFY_Jet_Publication_Version_2016.pdf) establish constructive finite reachability from any initial state; they do not establish a polynomial-time bound.
No result settling this exact rational-mass path-construction problem was located.
Under the intended interpretation, allowing the unilateral dissolutions expressly permitted in the question, the construction is polynomial-time solvable.
If unilateral moves were excluded, reachability could fail: take one type on each side, masses $1,1$, surplus $0$, outside options $1,0$, and an initial full matching paying $0,0$. No pair improvement is possible, although individual rationality fails. The proof below uses unilateral moves only to repair individual irrationality at the beginning.
The construction has two stages. First, a circulation decomposition allows us to reach a maximum-surplus matching using polynomially many cohort improvements. Second, short operations create and propagate cohorts receiving fixed equilibrium payoffs. All operations are described and verified below.
Let the type masses be $\alpha_i>0$ and $\beta_j>0$. Normalize payoffs and surpluses by
$$
s_{ij}=v_{ij}-a_i-b_j,\qquad P=p-a_i,\qquad Q=q-b_j.
$$
Outside options are now $0$. Matched payoffs satisfy $P+Q=s_{ij}$, and all improvement comparisons are preserved.
Dissolve every initial matched record having a negative normalized payoff. An endpoint receiving a negative payoff can initiate this unilateral improvement. At most $K$ dissolutions suffice, and the resulting state is individually rational. Every subsequent operation below preserves individual rationality.
Consider the transportation linear program
$$
\max \sum_{i,j}s_{ij}x_{ij}
$$
subject to
$$
x_{ij}\geq 0,\qquad
\sum_jx_{ij}\leq\alpha_i,\qquad
\sum_ix_{ij}\leq\beta_j.
$$
Its dual is
$$
\min \sum_i\alpha_i u_i+\sum_j\beta_j w_j
$$
subject to
$$
u_i,w_j\geq 0,\qquad u_i+w_j\geq s_{ij}.
$$
The primal is feasible and bounded. The dual is feasible by taking
$$
u_i=\max\{0,\max_{k,\ell}s_{k\ell}\},\qquad w_j=0.
$$
The standard polynomial-time theorem for rational linear programming therefore gives optimal rational solutions $x,u,w$, with polynomial encoding lengths.
Complementary slackness gives
$$
x_{ij}>0\ \Longrightarrow\ u_i+w_j=s_{ij},
$$
and positive unmatched reference mass forces the corresponding dual payoff to be $0$.
We can make the reference payoffs integral. Replace
$$
u_i\longleftarrow\lfloor u_i\rfloor,\qquad
w_j\longleftarrow\lceil w_j\rceil.
$$
To verify feasibility, write the unrounded values as $u_i^{\mathrm{old}},w_j^{\mathrm{old}}$. If the rounded sum were smaller than the integer $s_{ij}$, then
$$
u_i^{\mathrm{old}}+w_j^{\mathrm{old}}
<
\lfloor u_i^{\mathrm{old}}\rfloor+
\lceil w_j^{\mathrm{old}}\rceil+1
\leq s_{ij},
$$
a contradiction. On a tight edge, integrality of $s_{ij}$ gives
$$
\lfloor u_i^{\mathrm{old}}\rfloor+
\lceil w_j^{\mathrm{old}}\rceil=s_{ij}.
$$
Zero payoffs remain zero. Consequently, the rounded reference remains optimal and complementary to $x$.
Henceforth, $u_i,w_j$ denote these integral reference payoffs.
Call a cohort reference-paid if it receives its type’s reference payoff. A matched record is reference-paid when its payoffs are $(u_i,w_j)$.
We will repeatedly use the following property.
Lemma 1. In every individually rational state of maximum surplus:
Proof. Let $V^*$ be the optimal transportation value and $W(S)$ the surplus of the state. Accounting for all population mass gives
$$
V^*-W(S)
=
\sum_{\text{matched records }(i,j,h)}
h(u_i+w_j-s_{ij})
+
\sum_{\text{unmatched firm records }(i,h)}hu_i
+
\sum_{\text{unmatched worker records }(j,h)}hw_j.
$$
All summands are nonnegative. If $W(S)=V^*$, each positive-mass summand must vanish. $\square$
In particular, in such a state a matched record has one reference-paid endpoint if and only if both endpoints are reference-paid.
The reference-edge step below is related to the finite-agent construction of [Biró, Bomhoff, Golovach, Kern and Paulusma](https://durham-repository.worktribe.com/OutputFile/1456303). We prove everything needed here, including the rational-cohort compression.
Introduce one auxiliary vertex $z$. Construct a directed multigraph with the supported types and $z$ as vertices.
Its arcs, with rational amounts, are:
Omit zero-amount arcs.
At each firm vertex, the total outgoing amount is $\alpha_i$, and the total incoming amount is $\alpha_i$. At each worker vertex, both totals are $\beta_j$. Conservation also holds at $z$, either by summing these equalities or directly from the unmatched-mass identities. Thus the amounts form a circulation.
There are at most
$$
E=K+|I||J|+2\tau
$$
arcs: initial matched records remain at most $K$, and unmatched records can be merged by type.
Decompose the circulation into simple directed cycles. Repeatedly find a directed cycle, subtract the minimum amount on its arcs, and record that cycle with the subtracted amount. Each iteration exhausts an arc, so there are at most $E$ cycles. Each cycle contains at most $\tau$ type vertices.
A cycle of amount $d$ represents one population cohort of mass $d$ at each of its type vertices. Its current arcs specify a matching of these cohorts; its reference arcs specify another matching. Arcs incident with $z$ specify unmatched cohorts, and $z$ itself represents no population.
This interpretation is valid because, at a firm vertex, the outgoing arc is current and the incoming arc is reference; at a worker vertex, the incoming arc is current and the outgoing arc is reference. Thus each represented cohort has at most one partner in each matching.
The decomposition is only bookkeeping. Split each original matched record consistently at its two endpoints according to its cycle portions. Atomlessness permits these splits. No agent’s match or payoff changes.
Temporarily regard the cohorts of one cycle as finite vertices, all having mass $d$. Their current matching has nonnegative integral payoffs. Their reference matching has payoffs inherited from $u,w$.
While a reference-matching edge $ij$ is blocking, match its two cohorts. If their current payoffs are $P,Q$, use
$$
P'=P,\qquad Q'=s_{ij}-P.
$$
Because $P+Q<s_{ij}$, the firm retains its payoff and the worker strictly improves. Abandoned partners become unmatched.
Each reference edge can be satisfied at most once. After it is satisfied, its endpoints are matched to one another. Every other reference edge is disjoint from it, so later operations cannot disturb it. A currently matched reference edge cannot itself block because its payoffs sum to its surplus.
Therefore this cycle needs at most $\tau$ improvements.
At termination, let $M$ be its current matching, $M^*$ its reference matching, and $P_t$ its current payoff at vertex $t$. Write $r_t$ for its reference payoff. Since no reference edge blocks,
$$
\sum_{ij\in M^*}s_{ij}
\leq
\sum_{ij\in M^*}(P_i+P_j)
\leq
\sum_tP_t
=
\sum_{ij\in M}s_{ij}.
$$
Reference feasibility, and the fact that reference-unmatched vertices have reference payoff $0$, give
$$
\sum_{ij\in M}s_{ij}
\leq
\sum_t r_t
=
\sum_{ij\in M^*}s_{ij}.
$$
All inequalities are equalities. The cycle’s current matching therefore has the same surplus as its reference matching.
Process all cycles independently. Multiplying each cycle’s surplus equality by its amount $d$ and summing proves that the resulting society has surplus $V^*$.
This stage uses at most $E\tau$ pair improvements and polynomially many records. By Lemma 1, every resulting matched edge is reference-tight, and every unmatched agent’s reference payoff is $0$.
We now remain at maximum-surplus states between the short operations described below.
For each type $t$, let $B_t$ be the total mass currently receiving its reference payoff. Call a type seeded when $B_t>0$.
Suppose a non-reference matched record of types $i,j$ has mass $h$ and payoffs
$$
P+Q=s_{ij}=u_i+w_j.
$$
Assume first that firm type $i$ is seeded.
Merge reference-paid matched records having the same type pair, and merge unmatched records by type. A reference-paid firm cohort of type $i$ is then either unmatched or belongs to one of at most $|J|$ reference-paid matched records. Choose one such cohort, of mass $b>0$, and set
$$
d=\min\{h,b\}.
$$
Suppose the helper belongs to a reference-paid record of types $i,k$.
If $P>u_i$, then $Q<w_j$. Perform:
The second move is legal: both endpoints currently receive $0$, and their proposed payoffs are nonnegative and sum to $s_{ik}$. If $s_{ik}=0$, then $u_i=w_k=0$; leave both abandoned cohorts unmatched instead.
If $P<u_i$, perform:
Here $u_i>0$, so the second move strictly improves at least one endpoint.
In either case, the helper agents finish reference-paid, and mass $d$ of the original record becomes reference-paid. No new non-reference record is created.
An unmatched helper has $u_i=0$. Since $P\geq0$ and the original record is non-reference, necessarily $P>u_i$ and $Q<w_j$.
Match helper firms with mass $d$ of the original workers at $(u_i,w_j)$. The workers strictly improve. The abandoned original firms receive $0=u_i$.
Again, the original endpoints become reference-paid, and the helper retains its reference payoff.
The same construction applies when the seeded endpoint is a worker, by exchanging the two sides. The move rules, payoff identities, and stability inequalities are invariant under this exchange.
Call one of these one- or two-move operations a propagation batch. At its end:
Thus the state again has maximum surplus.
Choose a largest reference-paid cohort of the helper’s type. There are at most $\tau$ such records incident with that type, including its unmatched record, so
$$
b\geq \frac{B_t}{\tau}.
$$
Every batch either exhausts the selected non-reference record or, when $h>b$, increases
$$
B_t\longmapsto B_t+b
\geq
\left(1+\frac1\tau\right)B_t.
$$
For any invocation, the starting rational masses lie on a common rational grid. Propagation preserves that grid. Since $B_t$ is bounded by the total mass of type $t$, the multiplicative increases can occur only finitely many times; record exhaustions also occur only finitely many times.
Consequently, we can finish propagation until no non-reference record is incident with a seeded type. At that point,
$$
B_t>0\ \Longrightarrow\ \text{every agent of type }t
\text{ receives its reference payoff}.
$$
Unmatched cohorts cause no exception, by Lemma 1.
Suppose propagation has finished but the state remains unstable. Individual rationality already holds, so there are positive-mass firm and worker cohorts with
$$
P+Q<s_{ij}\leq u_i+w_j.
$$
At least one endpoint is underpaid relative to the reference. Assume first that
$$
Q<w_j.
$$
The worker cohort is matched: unmatched workers already receive their reference payoff. Let its record, called $B$, have types $l,j$ and mass $h_B$. Its edge is tight:
$$
s_{lj}=u_l+w_j.
$$
Moreover, $w_j>0$, hence $s_{lj}>0$.
Let $A$ be the selected firm cohort, of mass $h_A$; it may be matched or unmatched. If matched, its record differs from $B$, since endpoints of one matched record cannot block.
Choose
$$
d=\min\{h_A,h_B/2\}>0.
$$
Reserve two disjoint portions $B_1,B_2$, each of mass $d$, within $B$.
Set
$$
Y=\min\{s_{ij}-P,\ w_j-1\},\qquad X=s_{ij}-Y.
$$
All quantities are integral. Blocking and $Q<w_j$ imply
$$
s_{ij}-P\geq Q+1,\qquad w_j-1\geq Q.
$$
Therefore
$$
X\geq P,\qquad Y\geq Q,\qquad Y<w_j,\qquad X+Y=s_{ij}.
$$
Perform the following moves.
Move 1. Match mass $d$ of firms from $A$ with the workers of $B_1$, paying $(X,Y)$.
This is an improvement because both endpoints weakly improve and their previous payoff sum was strictly smaller than $s_{ij}$. The firms of $B_1$ become unmatched. If $A$ was matched, its selected workers also become unmatched.
Move 2. Match the abandoned firms of $B_1$ with the workers of $B_2$, paying $(u_l,w_j)$.
The firms start at $0$, and the workers strictly improve from $Q<w_j$. The firms of $B_2$ become unmatched.
Move 3. Match the abandoned firms of $B_2$ with the workers selected in Move 1, paying $(u_l,w_j)$.
The firms start at $0$, and the workers strictly improve from $Y<w_j$. The firms selected from $A$ become unmatched.
Move 4, when needed. If $A$ originally belonged to a matched record of types $i,k$ with positive surplus, match its abandoned firms and workers at $(u_i,w_k)$.
That original edge is reference-tight. Both cohorts currently receive $0$, so this is an improvement. If its surplus was $0$, both reference payoffs are $0$, and we leave those cohorts unmatched. If $A$ was originally unmatched, its reference payoff is $u_i=0$, so its firms already finish reference-paid.
Each move selects agents who are not currently partners: in Moves 2–4, one or both selected cohorts are unmatched. The two portions $B_1,B_2$ are disjoint.
At the end:
Thus maximum surplus is restored. Existing reference-paid mass has not decreased.
If instead the firm endpoint is underpaid, exchange the two sides and apply the same operation.
Crucially, the underpaid endpoint’s type was unseeded. Otherwise, completed propagation would force all its agents to receive their reference payoff. The operation therefore creates a seed in a previously unseeded type.
After normalization and the initial unilateral dissolutions:
Propagation terminates by Section 3.
Each seed-creating operation increases the number of seeded types. Existing seeded types remain seeded after every complete operation. Therefore there are at most $\tau$ seed-creating operations.
If all types become seeded, completed propagation makes every cohort reference-paid. Reference feasibility then gives
$$
u_i+w_j\geq s_{ij}
$$
for every firm-worker cohort pair, so the state is stable. The algorithm must consequently terminate, possibly earlier at another stable payoff vector.
All states are feasible. Every actual matching change is a permitted pair improvement, except for the initial individually irrational dissolutions.
It remains to bound the rational arithmetic and the explicit output.
Let $D$ be the product of the denominators of all input masses and all entries of the computed reference flow $x$. Its binary length is polynomial: the input denominators have total encoding length at most $L$, and $x$ has polynomial encoding length.
The circulation decomposition and its improvement operations use only additions, subtractions, and minima, so their masses remain multiples of $1/D$.
Each seed-creating operation may introduce one additional factor of $2$ into the common denominator. There are at most $\tau$ such operations. Propagation introduces no further denominator factors.
Hence every mass used anywhere is a multiple of
$$
\delta=\frac1{2^\tau D}.
$$
Every positive seed mass is at least $\delta$.
For a supported type $t$ with mass $M_t$, define
$$
R=\max_t\left\lceil\log_2(M_t/\delta)\right\rceil.
$$
This is polynomially bounded in the input parameters: the bit lengths of $D$ and the type masses are polynomial.
Let $H$ be the number of non-reference matched records immediately after the maximum-surplus stage. We have
$$
H=O(E\tau).
$$
Neither propagation nor a complete seed-creating operation creates a new non-reference record. Thus at most $H$ propagation batches exhaust a record.
In every other propagation batch, the helper type’s reference-paid mass increases by a factor at least $1+1/\tau$. Since
$$
\log_2(1+1/\tau)\geq\frac1{2\tau},
$$
there are $O(\tau(R+1))$ such batches for each type, and
$$
O\bigl(\tau^2(R+1)\bigr)
$$
over all types. Each batch uses at most two pair improvements.
The complete path therefore contains
$$
O\bigl(K+E\tau+\tau^2(R+1)\bigr)
$$
improvements, a polynomial bound.
Record counts are also polynomial. After merging identical reference-paid records, there are at most $|I||J|$ reference-paid matched records and $\tau$ unmatched records. Non-reference matched records never exceed $H$ after the maximum-surplus stage. Each short operation adds only constantly many temporary records.
All mass encodings are polynomially bounded by the grid $\delta$ and the total population mass. All payoffs are integral and have polynomial bit lengths. Finding a blocker, choosing a largest helper cohort, maintaining records, and performing each arithmetic operation therefore take polynomial time.
This also permits explicitly listing every intermediate state: both the number of states and the size of each state are polynomial.
Restoring the outside options completes the required construction.
⟨structured verdict parsed — rendered above⟩
Result: proved. The construction resolves the intended task, including the unilateral dissolutions expressly allowed for repairing an individually irrational initial state. I found no false step, missing substantive lemma, or defect in the polynomial bound.
The polynomial claim concerns binary input length, rather than the numerical sizes of masses or surpluses. The write-up supplies the necessary bounds on both the number of moves and the encodings of intermediate states.
The opening qualification about unilateral moves is appropriate. The task expressly permits unilateral dissolution, although its final question calls the requested sequence a sequence of pair improvements. The prover states its interpretation explicitly and uses unilateral moves only during initial repair.
The example showing failure when unilateral moves are excluded is correct. With surplus $0$, all initial payoffs $0$, and outside options $1$ and $0$, no pair can obtain a strictly improving feasible division of surplus. Individual rationality nevertheless fails.
The normalization
$$
s_{ij}=v_{ij}-a_i-b_j,\qquad P=p-a_i,\qquad Q=q-b_j
$$
preserves integrality, matching feasibility, payoff comparisons, and stability inequalities. Unmatched normalized payoffs are $0$.
Dissolving a matched record with a negative normalized endpoint payoff is a legal unilateral improvement: that endpoint strictly improves to $0$. Dissolving whole offending records requires at most $K$ moves. The resulting state is individually rational.
The transportation program correctly permits unmatched mass and unequal total masses on the two sides. It is feasible, since the zero flow is feasible, and bounded, since every variable is bounded by the corresponding finite type masses.
The displayed dual is correct. Its proposed feasible solution satisfies every constraint, including when all normalized surpluses are negative.
The invoked rational linear programming theorem applies: the programs have rational coefficients, polynomially many variables and constraints, and polynomial encoding length. Exact optimal solutions with polynomial encoding lengths can therefore be computed in polynomial time.
Complementary slackness gives both properties subsequently used:
The asymmetric rounding is valid. If
$$
\lfloor u_i^{\mathrm{old}}\rfloor+\lceil w_j^{\mathrm{old}}\rceil<s_{ij},
$$
integrality of $s_{ij}$ gives precisely the contradiction displayed in the proof. Nonnegativity is preserved.
On a tight edge, the identity
$$
\lfloor u_i^{\mathrm{old}}\rfloor+\lceil w_j^{\mathrm{old}}\rceil=s_{ij}
$$
holds because the unrounded sum is an integer. A zero payoff remains zero under its prescribed rounding.
Thus the rounded dual remains feasible and complementary to the same primal flow. The assertion that it remains optimal is justified.
The accounting identity is correct: the dual objective allocates each type’s reference payoff over its full mass, while the current surplus counts matched records only.
Every term on the right is nonnegative. Consequently, at maximum surplus, each positive-mass matched record must be tight, and each positive-mass unmatched cohort must have reference payoff $0$.
The ensuing assertion about reference-paid endpoints follows from tightness: if one endpoint receives its reference payoff, the matched-payoff identity forces the other endpoint to receive its reference payoff as well.
The arc orientations correctly represent current and reference matchings. At each supported type, incoming and outgoing amounts equal its full mass. Conservation at the auxiliary vertex follows from conservation at all other vertices.
The arc bound
$$
E=K+|I||J|+2\tau
$$
is valid for the graph constructed before splitting: current matched records number at most $K$, reference matching arcs number at most $|I||J|$, and the unmatched arcs contribute at most $2\tau$.
The cycle decomposition is finite and polynomial. Every iteration removes at least one positive residual arc and introduces none, so at most $E$ cycles are produced.
The interpretation of a simple cycle as equal-mass cohorts is valid. Each represented type occurs once on that cycle and has at most one current partner and one reference partner. Splitting the two endpoints of an original matched record consistently preserves its existing partnerships. Different cycles can then be processed independently.
For a blocking reference edge,
$$
P+Q<s_{ij},
$$
the proposed division
$$
P'=P,\qquad Q'=s_{ij}-P
$$
is integral, preserves the firm’s payoff, and strictly improves the worker’s payoff. Both selected endpoints remain individually rational. Abandoned partners receive $0$.
A blocking reference edge cannot already be the selected cohorts’ current matching edge, because currently partnered endpoints have payoff sum exactly equal to that edge’s surplus.
The assertion that each reference edge can be satisfied at most once is justified. Reference edges constitute a matching on the cycle’s cohorts. Once one is installed, later reference-edge moves select neither of its endpoints and therefore cannot disturb it.
Both displayed inequality chains are valid.
At termination, every reference edge has current endpoint payoff sum at least its surplus. Omitting reference-unmatched vertices from the payoff sum cannot increase it, because current payoffs are nonnegative.
Conversely, reference feasibility bounds the surplus of every current matching edge by its endpoints’ reference payoffs. Any current-unmatched reference payoffs omitted from this sum are nonnegative. Reference-unmatched vertices have reference payoff $0$, which justifies the final equality with reference matching surplus.
The two chains force equality of current and reference surplus on every cycle. Multiplication by cycle masses and summation correctly yields total surplus $V^*$.
The stage therefore uses at most $E\tau$ pair improvements and leaves a maximum-surplus state.
All cases are correctly separated.
If $P>u_i$, tightness implies $Q<w_j$. The first move preserves the helper firm’s reference payoff and strictly improves the original worker. Its selected agents come from distinct records.
The abandoned endpoints can be matched at $(u_i,w_k)$ whenever $s_{ik}>0$: both start at $0$, their proposed payoffs are nonnegative, and at least one is positive. If $s_{ik}=0$, nonnegativity and tightness force both reference payoffs to be $0$, so leaving them unmatched is valid.
If $P<u_i$, the first move strictly improves the original firm while preserving the helper worker’s payoff. The second move is strict because $u_i>0$.
In each case, the helper endpoints finish reference-paid, the selected original endpoints become reference-paid, and the original non-reference record has only its unselected residual mass remaining.
Lemma 1 gives $u_i=0$. Individual rationality and the original record’s failure to be reference-paid force $P>0$ and $Q<w_j$.
The proposed match strictly improves the original worker, preserves the helper firm’s payoff, and leaves the abandoned original firm receiving its reference payoff $0$.
The worker-helper version is justified by exchanging the two sides; the move rules and relevant identities are symmetric.
At the end of each batch, reference-paid mass does not decrease for any type. For the helper’s type it increases by exactly the converted mass $d$. Tightness and the reference payoffs of unmatched cohorts are restored, so Lemma 1’s accounting identity confirms restoration of maximum surplus.
Merging identical reference-paid records leaves at most $\tau$ eligible helper records for a type, including its unmatched record. Therefore the largest has mass at least $B_t/\tau$.
Every batch either exhausts a non-reference record or increases its helper type’s reference-paid mass by the stated multiplicative factor. This establishes the propagation progress measure used later.
A stability violation satisfies
$$
P+Q<s_{ij}\leq u_i+w_j.
$$
Thus at least one endpoint is underpaid relative to its reference payoff.
For the worker-underpaid case, Lemma 1 ensures the worker is matched. Also, $Q\geq0$ and $Q<w_j$ imply $w_j>0$, so its tight original edge has positive surplus.
The choice
$$
d=\min\{h_A,h_B/2\}
$$
permits two disjoint portions of the worker’s original record. If the firm cohort is matched, its record cannot equal that worker record: endpoints of the same record cannot violate their own surplus equality.
The definitions of $X$ and $Y$ satisfy all claimed inequalities. Integrality gives
$$
s_{ij}-P\geq Q+1,\qquad w_j-1\geq Q.
$$
Consequently, Move 1 weakly improves both endpoints and strictly improves at least one, while ensuring $Y<w_j$.
Moves 2 and 3 strictly improve their selected workers. Their selected firms are unmatched and receive nonnegative reference payoffs. The disjoint reserved portions ensure these moves use the intended agents.
Move 4 is legal when needed: the original firm-worker edge is tight, both selected endpoints are unmatched, and positive surplus guarantees strict improvement for at least one. For a zero-surplus original edge, both reference payoffs are $0$, so leaving its endpoints unmatched is valid. An originally unmatched firm likewise has reference payoff $0$.
The final-state assertions hold: both reserved portions of the worker record become reference-paid, the selected firm portion becomes reference-paid, no new non-reference record remains, and existing reference-paid mass is preserved.
The underpaid type was previously unseeded, because completed propagation makes every agent of a seeded type reference-paid. Hence each such operation creates a genuinely new seed.
Seeded types remain seeded between complete operations. Each seed-creating operation adds at least one previously unseeded type, so there are at most $\tau$ such operations.
After propagation, a seeded type has no non-reference matched record incident with it. Unmatched agents already receive their reference payoffs. Thus, if all types are seeded, every cohort receives its reference payoff.
Dual feasibility then gives every required stability inequality. Individual rationality holds throughout after the initial repair.
Stopping earlier upon a stability check is also valid; the algorithm need not force its chosen reference payoff vector when another stable vector has already been reached.
The denominator argument is correct.
The product $D$ includes the denominators of initial masses and computed reference-flow entries. Its binary length is polynomial because it is bounded by the sum of those denominator encoding lengths.
Cycle decomposition uses additions, subtractions, and minima, which preserve the grid of multiples of $1/D$. Each seed operation introduces at most one additional factor of $2$. Propagation introduces none. Therefore
$$
\delta=\frac{1}{2^\tau D}
$$
is a valid common grid for every mass occurring in the construction.
Every positive seed mass is at least $\delta$, and every type’s reference-paid mass is at most its full mass $M_t$. Thus $R$ has polynomial size.
The initial number $H$ of non-reference records is polynomial. Subsequent complete operations create no new non-reference record, so at most $H$ propagation batches exhaust such a record.
For every other batch, the helper type’s reference-paid mass grows by at least the stated factor. The logarithmic inequality used to bound the number of these increases holds for the admissible range $\tau\geq2$. Reference-paid masses remain nondecreasing across seed operations, so the per-type bound applies across the entire algorithm, rather than restarting at each propagation invocation.
The total move bound correctly absorbs the at most $4\tau$ seed-operation moves.
Record counts remain polynomial after merging identical reference-paid records. Temporary operations add only constantly many records. The common grid and bounded total population mass give polynomial mass encoding lengths. Payoff encodings are also polynomial: normalization, reference rounding, and every subsequent payoff calculation preserve polynomial bit length.
Finding violations and helpers requires searching polynomially many records. Thus both constructing the path and explicitly listing every intermediate state take polynomial time.
No substantive repair is required. The conclusion is valid under the explicitly stated interpretation allowing initial unilateral dissolutions.
⟨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.