Answer: Polynomial-time solvable. The sequence always converges, and its exact rational limit is computable in polynomial time.
Theorem 3 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateThe nucleolus of a fractional matching game on weighted graphs can be computed in polynomial time. Vertex Cover Games Given a graph G = (V, E), for every vertex v ∈V there is a non-negative weight wv. In a vertex cover game, agents N = E correspond to edges. The function f : 2N →R gives the cost for each coalition: For any S ⊆N, f(S) is de- fined as the value of a minimum vertex cover in the subgraph induced by S. In contrast to matching games, in vertex cover games, agents want to minimize their assigned cost shares.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite type set \(T\), rational masses \(\mu_t=p_t/D>0\) with \(\sum_t p_t=D\), and symmetric nonnegative rational values \(w_{tu}\), form for each positive integer \(r\) the graph with \(rp_t\) vertices of type \(t\), joining every distinct pair of types \(t,u\) with weight \(w_{tu}\), including distinct same-type pairs with weight \(w_{tt}\). Compute the ordinary fractional-matching-game nucleolus at each \(r\); symmetry gives a common payoff \(a_t^{(r)}\) to each vertex of type \(t\). Determine whether \(a^{(r)}\) converges as \(r\) grows and, if it does, compute its exact limit; otherwise prove nonconvergence. State complexity in the number of types and binary input length.
A society is given by its support: a nonempty list \(T\) of \(\tau\) types with positive binary rational masses \(\mu_t=p_t/D\), where \(p_t,D\) are positive integers and \(\sum_t p_t=D\). Here \(\tau=|T|\) is the support size, not the number of possible types.
The input also gives symmetric weights \(w_{tu}\in\mathbb Q_{\geq0}\), including diagonal weights; \(L\) is the total binary input length, including the supplied common denominator \(D\).
For every integer \(r\geq1\), let \(G_r\) have \(rp_t\) vertices of type \(t\). Every pair of distinct vertices of types \(t,u\) has edge weight \(w_{tu}\), including pairs within one type; there are no loops.
For a coalition \(S\), its worth \(f_r(S)\) is the maximum weight of a fractional matching in \(G_r[S]\), with capacity one at each vertex and no odd-set constraints.
Let \(x^{(r)}\) be the ordinary nucleolus over imputations \(x\geq0\) satisfying \(\sum_i x_i=f_r(V(G_r))\). Symmetry gives a common per-vertex payoff \(a_t^{(r)}\) within each type; these payoffs are not rescaled with \(r\). A one-vertex game has payoff zero.
The computational problem is to determine whether \(a^{(r)}\) converges as \(r\to\infty\), and, when it does, compute its exact limit.
Is this convergence-and-exact-limit problem solvable in polynomial time in \(\tau\) and \(L\), or is it NP-hard?
For explicitly listed finite weighted graphs, the fractional-matching-game nucleolus is computable in polynomial time ([Chen, Lu and Zhang](https://ojs.aaai.org/index.php/AAAI/article/download/8242/8101)).
No result settling this exact replication-limit problem was located in the literature search.
The problem is solvable in polynomial time in \(\tau\) and \(L\). In fact, a stronger statement holds:
Theorem. For every valid input, there is a rational vector \(a^*\), computable exactly in polynomial time, such that
\[
a^{(r)}=a^*\qquad\text{for every integer }r\geq2.
\]
Thus the sequence always converges, and its limit is \(a^*\).
The proof compresses the use of fixed edges and shortest paths in the finite-graph algorithm of [Chen, Lu and Zhang](https://ojs.aaai.org/index.php/AAAI/article/download/8242/8101). The reduction and the bit-complexity argument are proved below; the algorithm never expands a graph with a number of vertices proportional to \(D\).
Write \(p=(p_t)_{t\in T}\). Consider the following linear program, with one nonnegative variable \(b_{tu}\) for every unordered type pair, including diagonal pairs:
\[ F=\max\left\{ \sum_{t\leq u}w_{tu}b_{tu}: 2b_{tt}+\sum_{u\neq t}b_{tu}\leq p_t\ \text{for every }t,\quad b\geq0 \right\}. \]
Here and below, \(b_{tu}\) denotes the same unordered-pair variable whether \(t<u\) or \(u<t\). Its dual is
\[ F=\min\left\{ \sum_t p_ta_t: a_t\geq0,\quad a_t+a_u\geq w_{tu}\ (t\neq u),\quad 2a_t\geq w_{tt} \right\}. \]
Both programs are feasible, and the primal is bounded, so strong linear-programming duality applies.
Claim 1. For every \(r\geq2\), the grand-coalition worth is \(f_r(V)=rF\).
To prove the upper bound, aggregate any fractional matching in \(G_r\) by type pair. Its aggregate variables satisfy the primal capacity inequalities with right-hand side \(rp\). Dividing those variables by \(r\) gives a feasible solution for the program defining \(F\).
For the reverse bound, take an optimal aggregate solution with capacities \(rp\). Put \(n_t=rp_t\), so \(n_t\geq2\). Distribute its type-pair quantities uniformly over the actual edges:
Every vertex of type \(t\) then has matching degree
\[ \frac{2b_{tt}+\sum_{u\neq t}b_{tu}}{n_t}\leq1. \]
The objective value is unchanged. Since scaling the capacities by \(r\) scales the aggregate optimum by \(r\), this proves the claim.
Define the polytope
\[ C=\left\{ a\geq0: \sum_t p_ta_t=F,\quad a_t+a_u\geq w_{tu}\ (t\neq u),\quad 2a_t\geq w_{tt} \right\}. \]
It is nonempty by duality. It is compact because every \(p_t\) is positive and \(0\leq a_t\leq F/p_t\).
Claim 2. For every \(r\geq2\), \(C\) is exactly the set of type-constant core allocations, expressed as per-vertex payoffs.
Necessity follows from efficiency, singleton coalitions, and two-vertex coalitions. The diagonal inequality uses two distinct vertices of type \(t\), which exist because \(rp_t\geq2\).
For sufficiency, let \(a\in C\), let \(S\) be a coalition, and let \(z\) be any fractional matching on \(S\). The pair inequalities give
\[ \sum_{\{i,j\}\subseteq S}w_{\operatorname{type}(i),\operatorname{type}(j)}z_{ij} \leq \sum_{i\in S}a_{\operatorname{type}(i)} \sum_{j:\{i,j\}\subseteq S}z_{ij} \leq \sum_{i\in S}a_{\operatorname{type}(i)}. \]
The second inequality uses nonnegativity of the payoffs and the vertex capacities. Maximizing over \(z\) proves every core inequality.
The nucleolus belongs to the core: a core allocation has all coalition surpluses nonnegative, whereas an allocation outside the core has a negative surplus and therefore cannot maximize the sorted surplus vector. By uniqueness and symmetry, the nucleolus is type-constant. Consequently, it can be computed by lexicographic optimization over the common polytope \(C\).
For a coalition \(S\), use the surplus convention
\[ e_r(S,a)=\sum_{i\in S}a_{\operatorname{type}(i)}-f_r(S). \]
For an actual edge with endpoint types \(t,u\), put
\[ c_{tu}(a)=a_t+a_u-w_{tu}, \]
also when \(t=u\). Every \(c_{tu}(a)\) is nonnegative on \(C\).
We will use the following elementary property.
Lemma 3. Every finite graph has an optimal fractional matching whose positive-support components are single edges with value \(1\), or odd cycles whose edges all have value \(1/2\).
Proof. Choose an optimal extreme point of the fractional-matching polytope; such a point exists because that polytope is nonempty and bounded.
Consider a connected positive-support component with \(v\) vertices and \(m\) edges. Let \(U\) be its vertices whose capacity constraints are slack. The columns of its incidence matrix, restricted to tight capacity rows, must be linearly independent. Otherwise, a nonzero dependence gives a sufficiently small perturbation in both directions preserving the tight constraints, positivity on the support, and feasibility of the slack constraints. This contradicts extremality.
Thus \(m\leq v-|U|\). Connectivity gives \(m\geq v-1\), leaving two possibilities.
This proves the lemma. \(\square\)
Fix such an optimal matching for \(S\). Let \(I\) be its unmatched vertices, \(M\) its single-edge components, and \(\mathcal O\) its odd-cycle components. Then
\[ e_r(S,a) = \sum_{i\in I}a_{\operatorname{type}(i)} + \sum_{\{i,j\}\in M}c_{\operatorname{type}(i),\operatorname{type}(j)}(a) + \frac12\sum_{H\in\mathcal O}\sum_{\{i,j\}\in E(H)} c_{\operatorname{type}(i),\operatorname{type}(j)}(a). \]
This is an identity, and all its summands are nonnegative on \(C\).
Let \(P\subseteq C\) be a nonempty polytope that is not a singleton. An affine function is called fixed on \(P\) if it is constant throughout \(P\).
A coalition is fixed precisely when its payoff sum is fixed: its worth does not depend on \(a\).
We construct a family \(\mathcal R(P)\) of nonfixed coalitions. The construction depends on \(P\) and the supplied type data, but not on \(r\).
Include:
Their surpluses are respectively \(a_t\) and \(c_{tu}(a)\).
Construct a graph \(K_P\) whose vertices are the types \(t\) for which \(a_t\) is nonfixed on \(P\). Join distinct types \(t,u\) exactly when \(a_t+a_u\) is fixed on \(P\).
Give this edge the weight \(c_{tu}\), which is a constant nonnegative rational number on \(P\).
Lemma 4. Every component of \(K_P\) is bipartite. Moreover, if \(t,u\) belong to the same component and \(a_t+a_u\) is nonfixed, then they lie in the same side of its bipartition.
Proof. For any \(a,a'\in P\), set \(d=a-a'\). Every edge of \(K_P\) imposes \(d_t+d_u=0\). Along a path, the coordinates of \(d\) therefore alternate signs.
An odd cycle would force every coordinate of \(d\) in its component to vanish, for every choice of \(a,a'\). All types in that component would then be fixed, contradicting the definition of its vertex set. Thus the component is bipartite.
If \(t,u\) were in opposite sides, an odd-length path would give \(d_t+d_u=0\) for every \(a,a'\in P\). Their pair sum would be fixed. \(\square\)
For each distinct pair \(t,u\) in the same component of \(K_P\) whose pair sum is nonfixed, choose a minimum-weight simple path between them. By Lemma 4, this path has even length. Add the edge between its endpoints to obtain an odd cycle, and include its vertex set in \(\mathcal R(P)\).
Also, for every type \(t\) with a neighbor in \(K_P\), choose a neighbor \(v\) minimizing \(c_{tv}\). Use two distinct vertices of type \(t\) and one vertex of type \(v\), forming a triangle. Include this coalition as well. This handles a closing edge whose endpoints have the same type.
Every selected coalition uses at most two vertices of each type and at most \(\tau+1\) vertices in total. For \(\tau\geq2\), it is therefore a proper coalition of every \(G_r\) with \(r\geq2\), since
\[ \tau+1<2\tau\leq rD. \]
The case \(\tau=1\) needs no refinement: \(C\) is already a singleton.
These cycle coalitions are nonfixed. Indeed, if \(Q\) is obtained from a fixed-edge path with endpoint types \(t,u\), then
\[ a(Q)=\frac12\left( \sum_{\{i,j\}\text{ on the path}} \bigl(a_{\operatorname{type}(i)}+a_{\operatorname{type}(j)}\bigr) +a_t+a_u \right). \]
All path-edge sums are fixed, while the closing pair sum is nonfixed. The same identity applies to the triangle with two vertices of type \(t\).
For each selected coalition, compute its worth on its actual small, loopless graph. In particular, a type represented by only one vertex has no diagonal edge.
The family \(\mathcal R(P)\) has \(O(\tau^2)\) members.
Lemma 5. Fix \(r\geq2\), \(a\in P\), and \(\varepsilon\geq0\). The following conditions are equivalent:
Proof. Every representative is a proper, nonfixed coalition, so the first condition implies the second.
For the converse, take a proper coalition \(S\) whose payoff sum is nonfixed on \(P\), and choose an optimal matching as in Lemma 3.
Its decomposition from Section 2 expresses its payoff sum as a sum of component payoff sums. At least one component payoff sum must therefore be nonfixed. Consider such a component.
An unmatched vertex. Its type is nonfixed, so its singleton is a representative. Its contribution is at least \(\varepsilon\).
A single edge. Its endpoint payoff sum is nonfixed, so its pair coalition is a representative. Its contribution is at least \(\varepsilon\).
An odd cycle with at least two nonfixed edge sums. Each such edge has slack at least \(\varepsilon\), by the pair representatives. All other edge slacks are nonnegative, so the cycle contributes at least
\[ \frac12(2\varepsilon)=\varepsilon. \]
An odd cycle with exactly one nonfixed edge sum. Let its exceptional edge have endpoint types \(t,u\). Removing that edge leaves an even-length path of fixed edge sums.
Every vertex type on this path is nonfixed. Otherwise, fixedness of one vertex payoff and of successive edge sums would propagate along the entire path, making the exceptional edge sum fixed as well.
The projected type walk therefore lies in \(K_P\). Write \(h\) for its total fixed slack weight.
If \(t\neq u\), the selected minimum-weight simple path has weight \(h'\leq h\). If \(t=u\), the first and last edges of the projected walk are both incident with \(t\); consequently, the selected two-edge walk through a minimum-weight neighbor also has weight \(h'\leq h\).
Let \(Q\) be the corresponding representative cycle coalition. The original cycle contribution is
\[ \frac12\bigl(c_{tu}(a)+h\bigr) \geq \frac12\bigl(c_{tu}(a)+h'\bigr). \]
Putting matching value \(1/2\) on every edge of the selected odd cycle is feasible on \(Q\). Hence
\[ \frac12\bigl(c_{tu}(a)+h'\bigr) = a(Q)-\frac12\sum_{e\text{ on the selected cycle}}w_e \geq a(Q)-f_r(Q) = e_r(Q,a) \geq\varepsilon. \]
Finally, a cycle with no nonfixed edge sums cannot be the chosen nonfixed component: its vertex payoff sum is half the sum of its fixed edge payoff sums.
Thus some component contributes at least \(\varepsilon\). All remaining contributions are nonnegative, proving \(e_r(S,a)\geq\varepsilon\). \(\square\)
In particular, for every \(a\in P\),
\[ \min_{\substack{S\text{ proper}\\a(S)\text{ nonfixed on }P}}e_r(S,a) = \min_{Q\in\mathcal R(P)}e_r(Q,a). \]
Both sides are nonnegative because \(P\subseteq C\).
For completeness, consider the standard lexicographic refinement procedure on a compact polytope.
At each stage, discard every surplus function fixed on the current polytope. Maximize the minimum of the remaining functions, and restrict to the maximizing set. Discarding fixed functions preserves lexicographic comparisons: inserting the same fixed multiset of numbers into two sorted vectors does not change which vector is lexicographically larger.
Each nonterminal stage decreases dimension. To see this, let the optimum minimum be \(\varepsilon\), and take a relative-interior point of the maximizing polytope. Some remaining function equals \(\varepsilon\) there. Since that function is at least \(\varepsilon\) throughout the maximizing polytope, equality at a relative-interior point makes it constant on that polytope. It was nonconstant on the preceding polytope, so dimension has decreased.
Apply this procedure starting from \(P_0=C\). By Lemma 5, each refinement can be performed by the explicit LP
\[ \max \varepsilon \quad\text{subject to}\quad a\in P_{j-1},\quad \varepsilon\geq0,\quad a(Q)-f(Q)\geq\varepsilon \quad(Q\in\mathcal R(P_{j-1})). \]
If its optimum is \(\varepsilon_j\), retain the corresponding inequalities and obtain \(P_j\).
A nonsingleton \(P_{j-1}\) always has a nonfixed coordinate, so the representative family contains a singleton and is nonempty. Since \(\dim C\leq\tau-1\), there are at most \(\tau-1\) refinements.
The terminal point is the nucleolus restricted to \(C\), and hence the ordinary nucleolus: the ordinary nucleolus lies in \(C\), as proved in Section 1.
Crucially, the whole procedure is independent of \(r\geq2\):
Choosing shortest-path ties by a fixed rule therefore gives exactly the same sequence of polytopes for every \(r\geq2\). Their common terminal point is \(a^*\). This proves
\[ a^{(r)}=a^*\quad(r\geq2). \]
An exceptional one-vertex game at \(r=1\), when it occurs, does not affect the limit.
The preceding construction uses only polynomially many explicit rational LPs:
It remains to check that the recursively obtained rational constants have polynomial binary length.
The value \(F\) has polynomial binary length by the usual determinant bound for rational LP solutions. Every possible representative worth also has a uniform polynomial bit bound: it is the optimum of a fractional-matching LP on at most \(\tau+1\) vertices, using only supplied edge weights.
For the refinement optima, introduce separate variables \(\lambda_1,\ldots,\lambda_j\) and form the polytope
\[ \widehat P_j= \left\{ (a,\lambda): a\in C,\quad \lambda_i\geq0,\quad a(Q)-\lambda_i\geq f(Q) \text{ for }Q\in\mathcal R(P_{i-1}),\ 1\leq i\leq j \right\}. \]
This description uses the selected coalition count vectors and their worths, rather than previously computed \(\varepsilon_i\).
It is nonempty: for every \(a\in C\), taking all \(\lambda_i=0\) is feasible. It is bounded: \(a\) lies in compact \(C\), and every representative family contains a singleton, which bounds its \(\lambda_i\) from above.
Lexicographically maximizing \(\lambda_1,\ldots,\lambda_j\) over \(\widehat P_j\) gives exactly
\[ (\lambda_1,\ldots,\lambda_j)=(\varepsilon_1,\ldots,\varepsilon_j). \]
Indeed, later variables can always be set to zero, so they impose no additional restriction on the earlier optimization stages.
The resulting optimal face has a vertex, which is also a vertex of \(\widehat P_j\). Consequently, all the recorded \(\varepsilon_i\) occur as coordinates of a vertex of a rational polytope with:
Cramer’s rule and the determinant bound therefore give a polynomial binary-length bound for all refinement optima and for the final payoff vector. This also bounds the constants and shortest-path weights used during the algorithm.
Thus all LPs and graph computations can be performed exactly in polynomial time in \(\tau\) and \(L\), completing the proof.
⟨structured verdict parsed — rendered above⟩
The argument establishes polynomial-time solvability and stabilization for every \(r\geq2\), subject to one minor omission in its invocation of nucleolus uniqueness. I found no false central step, missing substantive lemma, or failure in the bit-complexity argument.
The aggregate primal correctly counts a diagonal matching quantity twice against its type capacity. Its displayed dual consequently has the correct constraints \(2a_t\geq w_{tt}\).
Aggregating a fractional matching proves the upper bound \(f_r(V)\leq rF\). The reverse construction is feasible because \(n_t=rp_t\geq2\). Uniform distribution gives each vertex precisely the displayed degree, including the factor \(2b_{tt}/n_t\) for diagonal quantities. Thus \(f_r(V)=rF\).
The characterization of \(C\) is correct. Two-vertex coalitions enforce every pair inequality, including diagonal inequalities, and these inequalities together with nonnegative payoffs bound every fractional matching on every coalition. Efficiency uses the correctly established grand-coalition worth.
Compactness follows from positive \(p_t\), and nonemptiness follows from duality. The case \(F=0\) causes no problem: \(C\) is then a singleton.
The surplus convention is consistent throughout. A core allocation has no negative surplus, while any imputation outside the core has a negative surplus, so an outside allocation cannot be the nucleolus.
Permuting vertices within each type preserves the game and permutes coalition surpluses. Therefore uniqueness gives type-constant nucleolus payoffs. Once the ordinary nucleolus lies in the symmetric core, optimizing over \(C\) preserves it.
Minor issue: “By uniqueness and symmetry” invokes the nucleolus uniqueness theorem without stating its precise applicable form or explicitly checking its hypotheses. This is an expositional omission, not a substantive obstacle: the games are finite, singleton worths are zero, and the imputation set is nonempty and compact. The cited [Chen–Lu–Zhang paper](https://ojs.aaai.org/index.php/AAAI/article/download/8242/8101) also states uniqueness and the standard lexicographic refinement framework.
Minimum clarification requested: State the existence-and-uniqueness theorem being invoked for a finite transferable-utility game with nonempty imputation set, and identify why it applies here.
Lemma 3 correctly uses linear independence of positive-support columns restricted to tight capacity rows. A dependence would permit sufficiently small feasible perturbations in both directions, contradicting extremality.
The resulting inequality \(m\leq v-|U|\), together with connectivity, leaves only trees and unicyclic components. The leaf argument correctly excludes trees with more than one edge: every leaf would have to be slack, contradicting \(|U|\leq1\). A single positive edge must have value \(1\), since a smaller value permits a perturbation.
A unicyclic component has all capacity constraints tight. Attached trees are excluded by the same leaf argument; even cycles admit alternating perturbations; odd-cycle degree equations force value \(1/2\).
The surplus decomposition is then exact. Its contributions are nonnegative on \(C\), including unmatched-vertex contributions. This nonnegativity is essential later and is established.
Singleton and pair representatives have the stated surpluses. Diagonal pair representatives use distinct actual vertices, available for every \(r\geq2\).
Lemma 4 correctly derives sign alternation from fixed pair sums. An odd cycle would force every coordinate in its component to be fixed, contradicting the graph’s vertex definition. Opposite bipartition sides likewise imply a fixed pair sum.
For distinct endpoints with nonfixed pair sum, the selected path has even length, and closing it produces an actual odd cycle. Its payoff sum is nonfixed by the displayed identity. The repeated-type triangle likewise has a nonfixed closing sum \(2a_t\).
Selected cycles use at most two vertices of any type. Their size bound and
\[
\tau+1<2\tau\leq rD
\]
correctly establish properness for \(\tau\geq2\). Singleton and pair representatives are also proper in that range. For \(\tau=1\), \(C\) is already a singleton, so no refinement is needed.
Computing each representative’s worth on its actual induced graph correctly avoids introducing a loop when a type appears only once.
The forward implication of Lemma 5 follows from properness and nonfixedness.
For the converse, a nonfixed coalition payoff sum must have at least one nonfixed component payoff sum in the chosen matching decomposition. The unmatched-vertex and single-edge cases therefore reduce directly to representatives.
An odd cycle with at least two nonfixed edge sums contributes at least \(\varepsilon\): each corresponding pair slack is at least \(\varepsilon\), and the cycle multiplies their sum by \(1/2\).
In the exactly-one-nonfixed-edge case, fixedness propagates along the remaining path. Hence all its vertex types are nonfixed. Consecutive types cannot coincide: a fixed diagonal pair sum \(2a_t\) would make \(a_t\) fixed. Thus the projected walk indeed uses edges of \(K_P\).
For distinct endpoints, nonnegative edge weights permit a simple path of weight no greater than the projected walk. Bipartiteness gives the required even length. For equal endpoint types, the two endpoint edges of the walk each weigh at least the minimum incident weight, establishing the claimed two-edge comparison.
The crucial inequality direction is correct:
\[
a(Q)-\tfrac12\sum_e w_e\geq a(Q)-f_r(Q).
\]
A feasible selected-cycle matching provides a lower bound on worth and therefore an upper bound on surplus. Since the representative surplus is at least \(\varepsilon\), the original component contribution is also at least \(\varepsilon\).
Finally, an odd cycle whose edge sums are all fixed has fixed total payoff sum. This exhausts the possibilities. Lemma 5 and the subsequent equality of minimum surpluses follow.
Removing functions constant on the current polytope preserves lexicographic comparisons: the same fixed multiset is inserted into every candidate’s sorted surplus vector.
Each refinement maximizes exactly the minimum of all remaining coalition surpluses, by Lemma 5. Restricting to the maximizing set using representative inequalities therefore gives the correct refinement polytope.
The dimension-decrease argument is sound. At a relative-interior point of the maximizing set, some remaining function attains the optimum minimum. Since it is bounded below by that value throughout the set, it is constant there. It was nonconstant on the preceding polytope, so dimension decreases.
A nonsingleton polytope has a nonfixed coordinate, ensuring a nonempty representative family. Thus there are at most \(\tau-1\) refinements, ending at a singleton.
Every stage depends only on the common polytope and the same small representative graphs. Coalition multiplicities in different replications do not undermine this argument: the exact minimum-surplus reduction applies separately at every stage for every \(r\geq2\). Consequently the terminal payoff vector is independent of \(r\).
The counts of LPs, constraints, representative vertices, and refinement stages are polynomial in \(\tau\). No construction expands a graph proportional to \(D\).
Representative worths have a uniform polynomial bit bound because their fractional-matching LPs have polynomial dimension and use supplied rational weights.
The lifted polytope \(\widehat P_j\) successfully avoids recursive accumulation of previously computed optimum constants. Its coefficients contain coalition count vectors and worths, rather than the \(\varepsilon_i\).
It is nonempty because representative surpluses are nonnegative on \(C\), and bounded because each stage’s family contains a singleton bounding its \(\lambda_i\). Later variables can be set to zero, so successive maximization of the \(\lambda_i\) reproduces the refinement optima.
The resulting successive optimal face has a vertex of the original lifted polytope. Its polynomial dimension and coefficient lengths give polynomial bit bounds through determinants. At the terminal stage, the payoff coordinates are uniquely determined, so this also bounds the output vector.
This establishes polynomial-time exact computation in \(\tau\) and \(L\), including binary encoding of \(D\).
The only requested revision is a precise statement and hypothesis check for the standard nucleolus existence-and-uniqueness theorem. No additional mathematical argument is needed to support the claimed stabilization or 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.