Answer: —
Theorem 2 — class: other
PDF text-layer excerpt — equations and symbol order may be approximateThe matching Ωgenerated by the Hybrid Procedure is a strict core matching of the model M = (W ∪F, Ψ0, C0, ≻). Furthermore, the generated matching state (Ω, C(Ω)) is strongly stable with C(Ω) being a subset of C0.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given finite worker and firm type sets with rational masses, explicit contract menus, strict rankings, and initial partnership cohorts with matched mass on both sides, find a feasible matching flow and final commitment masses such that the resulting state has no blocking positive-mass chain or cycle and no implementable measurable coalition can weakly improve for all its members while strictly improving a positive mass. Types record all relevant preferences, initial contracts, partner cohorts, and commitment status; each unit of mass receives at most one contract.
A society is given by its support: the list of the \(\tau\) types with positive mass, each mass a binary rational; \(\tau\) counts supported types, not possible types. Both worker and firm sides are nonempty; their combined mass is \(1\), with no requirement that their masses coincide. Let \(m\) count explicitly listed contract labels, including being single, and \(L\) be the total input bit length.
Each type specifies its side, strict ranking of incident contract labels, initial contract, initial partner cohort, and initial commitment status. Bilateral labels specify worker and firm types and fixed terms; different individuals offering the same label are indifferent. No additional payments or contracts are available.
Represent types by atomless intervals with Lebesgue measure. Initial partnership cohorts are disjoint equal-length interval pairs, paired by translation; remaining individuals are single. Write \(\mu_0\), \(a_0(x)\), and \(C_0\) for initial partner map, contract, and committed set, with singles fixed by \(\mu_0\) and excluded from \(C_0\). Require \(\operatorname{single}(x)\succ_x a_0(x)\Rightarrow\mu_0(x)\notin C_0\).
A state specifies a measurable measure-preserving matching involution \(\mu\), bilateral contracts agreed by their endpoints, and a measurable committed set \(C\subseteq C_0\cap\{x:\mu(x)\ne x\}\); every individual has exactly one bilateral or single contract \(a(x)\). Its computational representation is a finite rational interval subdivision with partner translations, contract labels, and commitment flags; lengths give matching flows and commitment masses.
Call \(a\) acceptable to \(x\) when \(a\succeq_x\operatorname{single}(x)\), and relatively acceptable when \(a\succeq_x a_0(x)\). Feasibility requires each assigned contract to be acceptable or relatively acceptable, acceptable for every \(x\notin C_0\), and both acceptable and relatively acceptable whenever \(\mu_0(x)\in C_0\).
A positive-mass chain consists of disjoint measurable cohorts \(X_1,Y_1,\ldots,X_K,Y_K\) of equal positive mass, \(K\ge1\), with \(X_1,Y_K\) free under \(C\) and \(\mu(Y_k)=X_{k+1}\) for \(k<K\). A cycle instead requires these partner equalities cyclically, with \(X_{K+1}=X_1\). It blocks if each \(X_k\) can be measurably paired with \(Y_k\) through mutually acceptable contracts strictly improving every participating individual. A state is strongly stable if free individuals receive acceptable contracts and no such chain or cycle blocks.
A positive-measure measurable coalition \(S\) is implementable when \(\mu_0(S\cap C_0)\subseteq S\). It improves a matching if a measurable matching using only members of \(S\) and listed contracts weakly improves every member and strictly improves a positive mass. A feasible matching is in the strict core if no implementable coalition improves it. All conditions hold almost everywhere; blocking coalitions and pairings need not have rational subdivisions.
Is constructing a feasible, strongly stable strict-core state, or determining that none exists, solvable in polynomial time in \(m,\tau,L\), or is this computational problem NP-hard?
For finite individual agents, a hybrid procedure constructs a strongly stable strict-core matching state with final commitments contained in initial commitments; the published version retains this existence result, calling the state stable. [Sun–Yang, 2018](https://www.york.ac.uk/media/economics/documents/discussionpapers/2018/1820.pdf), [Sun–Yang, 2021](https://eprints.whiterose.ac.uk/175719/1/Senior_Level_Job_Matching_Sun_Yang_Complete.pdf).
No result settling this precise atomless, support-encoded computational problem was located.
I do not settle the problem for arbitrary initial commitments. I prove a stronger tractable case than the equal-mass case in the notes:
Theorem. If $C_0=\varnothing$, constructing a feasible, strongly stable strict-core state, or determining that none exists, is solvable in polynomial time in $m,\tau,L$, for arbitrary positive binary-rational type masses.
The proof gives an explicit linear-programming algorithm and handles parallel contract labels. I also give two examples explaining why the reduction does not extend directly to initial commitments.
Throughout Sections 1–5, assume $C_0=\varnothing$.
Let $W$ and $F$ be the supported worker and firm types. Write $q_t>0$ for the mass of type $t$, and $s_t$ for its single label. For a bilateral label $b$, write $w(b)$ and $f(b)$ for its endpoint types.
Because every individual lies outside $C_0$, feasibility requires every assigned contract to be acceptable. Conversely, an assignment using acceptable contracts satisfies all the task’s local feasibility conditions: the condition concerning an initially committed partner is vacuous. Also, every measurable coalition is implementable, and the final committed set must be empty.
Call a type uniformly assigned if almost all its members receive the same label.
Every feasible strict-core matching assigns each supported type uniformly.
Proof. Suppose a type $t$ receives distinct labels $b,d$ on positive masses, with $b\succ_t d$.
Both labels are acceptable. Therefore $b$ cannot be $s_t$: otherwise $d\prec_t s_t$, contradicting acceptability of $d$. Thus $b$ is bilateral.
Choose a positive number $\varepsilon$ no larger than either of the following masses:
Choose a measurable cohort $A$ of mass $\varepsilon$ from the first population. Choose a measurable cohort $B$ of mass $\varepsilon$ from the current partners of the second population. Measure preservation guarantees that the latter partner population has the requisite mass.
The cohorts $A,B$ lie on opposite sides and are disjoint. Match them through label $b$. Members of $A$ strictly improve, while members of $B$ retain their current label and are indifferent to the replacement individuals. Equal-mass measurable subsets of atomless intervals admit a measure-preserving pairing modulo null sets.
Since $C_0=\varnothing$, the coalition $A\cup B$ is implementable. It contradicts strict-core membership.
There are finitely many incident labels. Hence, if a type is not uniform almost everywhere, at least two distinct labels occur on positive masses, which we have excluded. $\square$
If a feasible strict-core matching uniformly assigns label $b$ to type $w(b)$, then type $f(b)$ is also uniformly assigned $b$, and
$$
q_{w(b)}=q_{f(b)}.
$$
Proof. Positive mass of type $w(b)$ is matched through $b$, so positive mass of type $f(b)$ receives $b$. Lemma 1 makes the latter type uniform, necessarily with label $b$. Both entire type populations therefore participate in $b$, and measure preservation gives equality of their masses. The argument is symmetric between the sides. $\square$
Construct a bipartite multigraph $G$ with vertex classes $W,F$. Each listed bilateral label acceptable to both endpoint types becomes a distinct edge. Parallel labels remain distinct edges, ranked according to the given strict preferences.
A type matching $M$ selects edges with no shared vertices. A matched type receives its selected edge label; an unmatched type receives its single label. Denote this label by $a_t(M)$.
Call $M$ stable if there is no edge $b$ satisfying
$$
b\succ_{w(b)}a_{w(b)}(M)
\qquad\text{and}\qquad
b\succ_{f(b)}a_{f(b)}(M).
$$
Define the forbidden edge set
$$
P=\{b\in E(G):q_{w(b)}\ne q_{f(b)}\}.
$$
Edges in $P$ remain potential blocking edges; they are forbidden only as assignments.
A requested state exists if and only if $G$ has a stable type matching avoiding $P$.
Moreover, every such type matching yields a requested state by assigning its labels uniformly.
Proof: necessity. Lemmas 1 and 2 turn any feasible strict-core matching into a type matching avoiding $P$.
If some edge $b$ strictly improved both endpoint types over their uniform assignments, choose equal positive masses from those types and match them through $b$. Both cohorts strictly improve, and the coalition is implementable. This contradicts strict-core membership. Thus the type matching is stable.
Proof: sufficiency. Let $M$ be stable and avoid $P$. For every selected edge, its endpoint types have equal masses. Match their intervals by translation, assigning the selected label. Leave unmatched types single. All assigned labels are acceptable, so the resulting matching is feasible.
Suppose an improving measurable coalition existed. Since there are finitely many types and labels, some positive-mass category of its strictly improved members has one type $t$ and one new label $b$.
Their new label cannot be single, because their current assignment is acceptable. Thus $b$ is bilateral. Let $u$ be its other endpoint type. Weak improvement for their new partners gives
$$
b\succeq_u a_u(M).
$$
If $b=a_u(M)$, then type $u$ is uniformly assigned $b$ in the current matching. Since $b$ specifies endpoint types $t,u$, positive mass of type $t$ currently receives $b$. Uniformity would give $a_t(M)=b$, contradicting strict improvement of the selected type-$t$ members.
Consequently $b\ne a_u(M)$. Strict rankings imply
$$
b\succ_u a_u(M).
$$
Together with strict improvement for type $t$, this contradicts stability of $M$. Therefore no improving coalition exists, including one with an arbitrary measurable representation.
Finally, all individuals are free and receive acceptable contracts. Any blocking chain or cycle would use a bilateral label strictly improving both endpoint types over their uniform assignments. No such label exists. The state is strongly stable. $\square$
This reduction leads to stable marriage with forbidden edges, a known polynomially solvable problem; see [Cseh–Matuschke, Section 4.3](https://arxiv.org/pdf/1309.3701). The following construction supplies a direct proof for the multigraph formulation needed here.
Write
$$
n_W=|W|,\qquad n_F=|F|.
$$
Add a private dummy firm $\widehat w$ for each real worker type $w$, and a private dummy worker $\widehat f$ for each real firm type $f$. The auxiliary bipartition is
$$
U=W\cup\{\widehat f:f\in F\},
\qquad
V=F\cup\{\widehat w:w\in W\}.
$$
Both classes have size $\tau=n_W+n_F$.
Add the following edges:
Each real vertex retains its ordering of original acceptable labels and ranks its private edge last. Each dummy vertex ranks its private edge first and ranks its dummy–dummy edges in an arbitrary strict order.
Private edges represent single assignments. Dummy edges are solely computational devices; they will not be contracts in the output society.
The original graph has a stable matching avoiding $P$ if and only if the auxiliary graph has a stable perfect matching avoiding $P$.
Proof: restriction. Restrict an auxiliary perfect matching to its original edges. A real vertex not matched through an original edge is matched to its private dummy, and hence represents a single type.
If an original edge blocked the restriction, both real endpoints would prefer it to their auxiliary assignments, because private edges occupy the position of single. It would therefore block the auxiliary matching. Avoidance of $P$ is preserved.
Proof: extension. Start with a stable original matching $M$. Match each unmatched real vertex to its private dummy.
If $M$ contains $k$ original edges, exactly $k$ dummy workers and $k$ dummy firms remain unmatched. Their induced graph is complete bipartite. Run worker-proposing deferred acceptance on that graph.
For completeness, this procedure terminates because each edge is proposed at most once. It leaves a perfect matching: an unmatched worker who exhausted its complete list would imply that every firm holds a proposal, accounting for all $k$ workers and contradicting that worker’s unmatched status. It is stable because a worker preferring another firm to its final partner proposed to that firm, and the firm’s retained proposals only improved thereafter.
Combine these dummy matches with $M$ and the private matches. The result is perfect. It has no blocking edge:
Only original edges belong to $P$, so avoidance is preserved. $\square$
Let $H$ be the auxiliary multigraph. Write $\delta(v)$ for its incident edges, and $\succ_v$ for its strict edge ranking.
Introduce one real variable $x_e$ per edge. Consider the following feasibility system:
$$
x_e\ge 0
\qquad(e\in E(H)),
$$
$$
\sum_{e\in\delta(v)}x_e=1
\qquad(v\in U\cup V),
$$
$$
x_e+
\sum_{\substack{g\in\delta(u)\\g\succ_u e}}x_g+
\sum_{\substack{g\in\delta(v)\\g\succ_v e}}x_g
\ge 1
\qquad(e=uv\in E(H)),
$$
$$
x_e=0
\qquad(e\in P).
$$
For parallel edges, the two preference sums are separate: an edge preferred at both endpoints contributes twice. This is intentional.
The characteristic vector of a stable perfect matching avoiding $P$ satisfies the system.
Proof. Nonnegativity, degree equations, and forbidden-edge equations are immediate.
For the stability inequality of edge $e$, if $e$ is selected then $x_e=1$. Otherwise, stability and strict rankings imply that at least one endpoint is matched to an edge strictly preferred to $e$. The corresponding preference sum therefore contributes $1$. $\square$
Given any feasible $x$, let each vertex $u\in U$ select its most-preferred edge $e_u$ having $x_{e_u}>0$. These selected edges form a stable perfect matching avoiding $P$.
Proof. The degree equation ensures that every $u$ has a positive incident edge.
Fix $u$, and write $e_u=uv$. By its definition,
$$
\sum_{\substack{g\in\delta(u)\\g\succ_u e_u}}x_g=0.
$$
The stability inequality for $e_u$ gives
$$
x_{e_u}+
\sum_{\substack{g\in\delta(v)\\g\succ_v e_u}}x_g
\ge 1.
$$
The degree equation at $v$ is
$$
\sum_{g\in\delta(v)}x_g=1.
$$
Nonnegativity now implies that every edge strictly worse than $e_u$ at $v$ has zero weight. Since $x_{e_u}>0$, the edge $e_u$ is exactly the least-preferred positive edge at $v$.
Two different vertices of $U$ cannot select edges incident to the same $v$: each selected edge would have to be the unique least-preferred positive edge at $v$. Thus the selected edges match all vertices of $U$ to distinct vertices of $V$. Because $|U|=|V|$, they form a perfect matching $N$. Its edges have positive weight, so none belongs to $P$.
It remains to prove stability. Suppose an edge $e=uv$ blocked $N$. Then
$$
e\succ_u e_u.
$$
Because $e_u$ is the most-preferred positive edge at $u$, both $x_e$ and every weight on an edge preferred to $e$ at $u$ are zero. The stability inequality for $e$ therefore becomes
$$
\sum_{\substack{g\in\delta(v)\\g\succ_v e}}x_g\ge 1.
$$
The degree equation at $v$ forces all its positive edges to be strictly preferred to $e$. In particular, the edge assigned to $v$ by $N$ is strictly preferred to $e$. This contradicts blocking. Hence $N$ is stable. $\square$
The extraction requires neither an integral LP solution nor a polyhedral integrality theorem.
The algorithm is now explicit:
Correctness follows from Proposition 3 and Lemmas 4–6.
The auxiliary graph has $2\tau$ vertices and at most
$$
m+\tau+n_Wn_F
$$
edges. The linear program therefore has polynomially many variables and constraints. Its coefficients have bounded bit length, and exact comparisons of the input rational masses take polynomial time.
We use the standard rational-linear-programming theorem: feasibility of a system with rational coefficients can be decided in time polynomial in its encoding length, and a rational feasible point can be returned with polynomial encoding length. Its hypotheses hold here. In addition, the degree equations and nonnegativity imply $x_e\le 1$, so the feasible region is bounded.
The extracted type matching uses only equal-mass original edges. Each matched pair of type intervals can consequently be paired by translation. If the input represents a type through several interval pieces, split and pair those pieces greedily; each pairing exhausts at least one piece. This produces polynomially many pieces.
All lengths and translations are rational combinations of input interval coordinates, with polynomial bit length. Set $C=\varnothing$. Thus the algorithm constructs the required computational representation in polynomial time.
This proves the announced theorem for arbitrary type masses, without requiring equal total masses on the two sides.
The uniformity lemma does not extend to arbitrary initial commitments.
Consider one worker type $w$ and one firm type $f$, each of mass $1/2$. There are three bilateral labels $r,b,c$ between them, with rankings
$$
b\succ_w c\succ_w r\succ_w s_w,
$$
$$
c\succ_f b\succ_f r\succ_f s_f.
$$
Initially, the entire populations are paired through $r$, and everyone is committed. Divide the initial parameter interval into two pieces of length $1/4$. Retain the initial partners, assigning $b$ on one piece and $c$ on the other. Set $C=C_0$.
The state has a rational interval representation. It is feasible because both $b$ and $c$ are acceptable and relatively acceptable to both types.
Let $S$ be an implementable coalition. Since both endpoints of every initial pair are committed, $S$ selects either both endpoints of an initial pair or neither, modulo null sets.
Let $\alpha$ be the selected mass on each side from the $b$ piece, and $\beta$ the selected mass on each side from the $c$ piece.
In any weakly improving coalition matching:
If $B,D$ are the new matching masses through $b,c$, respectively, these observations give
$$
B\ge\alpha,\qquad D\ge\beta,\qquad B+D=\alpha+\beta.
$$
Therefore
$$
B=\alpha,\qquad D=\beta.
$$
The selected workers originally receiving $b$ exhaust all new $b$ matches, so the other workers retain $c$. The selected firms originally receiving $c$ exhaust all new $c$ matches, so the other firms retain $b$. Everyone retains their current label, and nobody strictly improves.
Thus the state belongs to the strict core.
No available label strictly improves both endpoints of a prospective pair:
Consequently no blocking chain or cycle exists. The free-individual condition is vacuous because everyone is committed.
This is a feasible, strongly stable strict-core state in which both supported types receive two labels on positive masses.
Even restricting attention to uniform states, ordinary pairwise stability is not necessary once commitments are present.
Take worker types $w_1,w_2$ and firm types $f_1,f_2$, each of mass $1/4$. The bilateral labels are
$$
r_1:w_1\text{--}f_1,\qquad
r_2:w_2\text{--}f_2,\qquad
b:w_1\text{--}f_2.
$$
Rankings are
$$
b\succ_{w_1}r_1\succ_{w_1}s_{w_1},
\qquad
r_2\succ_{w_2}s_{w_2},
$$
$$
r_1\succ_{f_1}s_{f_1},
\qquad
b\succ_{f_2}r_2\succ_{f_2}s_{f_2}.
$$
Initially, the populations are paired through $r_1,r_2$, and everyone is committed. Retain the initial matching, labels, and commitments. This state is feasible.
An implementable coalition selects equal masses $\alpha$ from each endpoint of the first initial cohort and equal masses $\beta$ from each endpoint of the second.
Every selected member of $f_1$ must retain $r_1$ to weakly improve. This consumes all $\alpha$ selected workers of type $w_1$. Every selected member of $w_2$ must retain $r_2$, consuming all $\beta$ selected firms of type $f_2$.
Hence the coalition cannot use $b$, and all selected members retain their labels. No improving coalition exists.
There are no free individuals, so no chain can block. The only bilateral label strictly improving both of its endpoints is $b$.
A blocking cycle containing an $f_2$ cohort would also contain its current $w_2$ partners: the cyclic partner equalities include every participant’s current partner. But $w_2$ has no strictly improving label. Thus no cycle blocks.
Nevertheless, $b$ strictly improves both $w_1$ and $f_2$ over their assignments. The state therefore fails ordinary pairwise stability.
Indeed, every feasible matching has the same assigned labels: feasibility requires members of $f_1$ and $w_2$ to receive contracts relatively acceptable to their initial contracts, forcing all of $f_1$ to receive $r_1$ and all of $w_2$ to receive $r_2$. Equal type masses then exhaust $w_1$ and $f_2$. Thus this instance has a requested state but no feasible ordinarily pairwise-stable matching.
The unrestricted polynomial-time versus $\mathrm{NP}$-hardness question remains open in this write-up.
The arbitrary-mass case without commitments is completely resolved above. The two commitment examples identify obstacles to extending that result: initial commitments can permit nonuniform strict-core allocations, and they can protect a state against a mutually improving pair.
A general algorithm must account for initial-partner inclusion in coalitions and the commitment restrictions on blocking-chain endpoints. I have neither proved such an algorithm nor supplied an applicable hardness reduction.
⟨structured verdict parsed — rendered above⟩
The output establishes a correct polynomial-time result for the restricted case $C_0=\varnothing$, including arbitrary positive rational masses and parallel contract labels. It does not settle USER_TASK for arbitrary initial commitments.
I found no mathematical error or substantive gap in the restricted theorem or the two commitment examples. The appropriate overall classification is partial, consistent with the prover’s own claim.
Correct. Every individual lies outside $C_0$, so feasibility requires acceptable assignments. The additional requirement involving an initially committed partner is vacuous. Also, $C=\varnothing$, and the implementability condition imposes no restriction on measurable coalitions.
This correctly removes initial partnerships from the restricted problem’s feasibility and coalition constraints.
Correct.
The measurable-pairing assertion applies to positive, equal-measure measurable subsets of the Lebesgue interval populations, modulo null sets. Rational subdivisions are unnecessary for this contradiction, as USER_TASK explicitly permits arbitrary measurable blocking coalitions.
Finally, finiteness of the label set ensures that failure of almost-everywhere uniformity produces two labels occurring on positive masses.
Correct. A uniformly assigned bilateral label at one endpoint creates positive mass receiving that same label at the other endpoint. Lemma 1 forces uniformity there as well. Consequently, the entire populations are matched through that label, and measure preservation yields equal type masses.
The conclusion uses supported types with positive masses, as required.
Both directions are correct.
Necessity. Uniformity and equal endpoint masses produce a type matching avoiding $P$. An edge strictly preferred by both endpoint types would yield an implementable improving coalition of equal positive masses. Thus the resulting type matching is stable.
Sufficiency. Avoiding $P$ permits uniform realization of every selected bilateral edge. Unmatched individuals receive single, so feasibility holds.
The strict-core argument correctly handles weak improvement:
This argument covers arbitrary measurable coalitions, rather than merely finitely represented ones.
Strong stability follows because every proposed blocking pair in a chain or cycle would require a label strictly improving both participating endpoint types. Stability excludes every such label. The free-individual acceptability condition also holds.
Correct.
Restriction preserves original-edge stability because private edges occupy the position of single in the acceptable-label ranking.
For extension, an original matching with $k$ edges leaves exactly $k$ unmatched dummy vertices on each side. Their complete bipartite graph admits the perfect stable matching produced by the stated deferred-acceptance procedure.
The proof checks all auxiliary edge classes:
The case $k=0$ is covered by the empty dummy matching. Forbidden edges remain available as potential blockers throughout.
The contextual citation to polynomial solvability of stable marriage with forbidden edges is supported by [Cseh–Matuschke](https://arxiv.org/pdf/1309.3701). The write-up’s correctness does not depend on importing that algorithm, since it supplies its own proof.
Correct, including parallel edges.
Lemma 5 follows directly from stability of a perfect matching.
For Lemma 6, the degree equation at $u$ ensures a most-preferred positive edge $e_u=uv$ exists. Its stability inequality and the degree equation at $v$ force every edge worse than $e_u$ at $v$ to have zero weight. Therefore $e_u$ is the unique least-preferred positive edge at $v$.
This establishes that distinct vertices of $U$ cannot select edges incident to the same vertex of $V$. Equal bipartition sizes then give a perfect matching.
The final stability argument is also valid: if $e$ were preferred to $e_u$ at $u$, its weight and all weights on edges preferred to it at $u$ would vanish. Its LP inequality would force all positive edges at $v$ to be preferred to $e$, including the extracted assignment.
Parallel labels cause no error. Strict rankings distinguish their edges, and the two preference sums are correctly treated separately. No integrality theorem is needed.
Correct.
The auxiliary graph has $2\tau$ vertices and at most $m+\tau+n_Wn_F$ edges. The LP has polynomial encoding length, including the preference sums, and rational mass comparisons take polynomial time.
The stated rational-LP theorem supplies both feasibility detection and a polynomial-bit-length rational feasible point. Its hypotheses hold for this rational system. Exact support extraction is consequently computationally valid.
The interval construction also satisfies the requested representation:
Unequal total masses on the two sides introduce no omitted case; unmatched types remain single.
Correct.
Both proposed labels satisfy acceptability and relative acceptability. Full initial commitment makes implementability require inclusion of both endpoints of each initial pair.
The inequalities
$$
B\ge\alpha,\qquad D\ge\beta,\qquad B+D=\alpha+\beta
$$
indeed force $B=\alpha$ and $D=\beta$. The individuals already receiving their top labels exhaust the respective new contract capacities, leaving every other selected individual with its original label.
The strong-stability argument checks all potentially improving bilateral labels. Neither $b$ nor $c$ strictly improves both endpoints of any prospective pair. Thus no chain or cycle blocks.
This example genuinely disproves extension of the uniformity lemma to arbitrary commitments.
Correct.
Implementability supplies equal selected masses within each initial partnership cohort. Weak improvement forces selected $f_1$ members to retain $r_1$ and selected $w_2$ members to retain $r_2$, exhausting the available selected partners. Hence no coalition can use $b$.
Full final commitment rules out chains. In a cycle, the partner equalities force inclusion of the current partner of every participant. Any improving use of $b$ therefore brings in a $w_2$ cohort, whose members have no strictly improving label. This rules out cycles.
The final feasibility argument also holds: committed initial partners trigger relative acceptability, forcing all $f_1$ members to receive $r_1$ and all $w_2$ members to receive $r_2$. Equal masses exhaust the other types. Thus the example has a requested state but no feasible ordinarily pairwise-stable matching.
Major scope issue: USER_TASK asks for a complexity classification allowing arbitrary $C_0$. The restricted algorithm and counterexamples do not provide that classification.
No clarification alone repairs this omission. Resolving the target requires either a polynomial-time construction/nonexistence algorithm valid for arbitrary initial commitments or an applicable hardness reduction under the stated support encoding and measurable definitions.
The restricted theorem needs no substantive repair. The two examples establish obstacles to its extension, but establish no general complexity result.
⟨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.