The Strong Core of Housing Markets with Partial Order Preferences (aamas25-00210)

Given a finite type set \(T\), rational masses \(\mu_t\ge 0\) with \(\sum_{t\in T}\mu_t=1\), partial orders \(\succ_t\) over house types, and forbidden type-arcs \(F\), where type \(t\) owns mass \(\mu_t\) of house type \(t\), decide whether there exists \(x_{t,u}\ge 0\) with \(\sum_u x_{t,u}=\mu_t\), \(\sum_t x_{t,u}=\mu_u\), and \(x_{t,u}=0\) on unacceptable or forbidden arcs, such that no nonzero \(z_{t,u,v}\) with \(0\le z_{t,u,v}\le x_{t,u}\) satisfies \(v\succeq_t t\), \(v\succeq_t u\), strict preference for at least one positive-mass class, and \(\sum_{u,v}z_{q,u,v}=\sum_{t,u}z_{t,u,q}\) for every \(q\in T\); if so, output \(x\).

A society is given by its support: a nonempty list \(T\) of \(\tau\) types with positive binary rational masses \(\mu_t\), summing to \(1\). The support size \(\tau\) counts listed types, not possible types. House types are also indexed by \(T\), so \(m=\tau\); type \(t\) initially owns mass \(\mu_t\) of house type \(t\).
Each type has an explicitly given strict partial order \(\succ_t\) on \(T\). Define \(v\succeq_t u\) to mean \(\neg(u\succ_t v)\), thus including incomparability. Let \(E=\{(t,u):u\succeq_t t\}\), and let \(F\subseteq E\) be forbidden allocation arcs, possibly including self-arcs.
An allocation is a nonnegative real matrix \(x\) with \(\sum_u x_{t,u}=\mu_t\), \(\sum_t x_{t,u}=\mu_u\), and \(x_{t,u}=0\) whenever \((t,u)\notin E\setminus F\).
A blocking deviation is a nonnegative real array \(z_{t,u,v}\), representing mass of type \(t\) currently receiving \(u\) and switching to \(v\), with \(\sum_v z_{t,u,v}\le x_{t,u}\) for every \(t,u\).
Require \(z_{t,u,v}=0\) unless \(v\succeq_t t\) and \(v\succeq_t u\), \(\sum_{u,v}z_{q,u,v}=\sum_{t,u}z_{t,u,q}\) for every \(q\in T\), and \(\sum_{t,u,v:\,v\succ_t u}z_{t,u,v}>0\). Forbidden arcs do not restrict deviations.
Call an allocation unblocked if no such deviation exists. The computational problem is to decide whether an unblocked allocation exists and, if so, find an exact rational allocation. Let \(L\) be the total input bit length; state running times in \(m,\tau,L\).

Is deciding the existence of an unblocked allocation in \(\mathsf{P}\), with a polynomial-time algorithm also finding one, or is the decision problem \(\mathsf{NP}\)-hard?

For finite agents with one indivisible house each, strict partial orders, and forbidden allocation arcs, strong-core existence and construction are polynomial-time solvable. [Schlotter and Mendoza-Cadena](https://www.ifaamas.org/Proceedings/aamas2025/pdfs/p1867.pdf).
No result settling the exact mass problem defined above was identified in the literature search.

Result

The decision problem is in \(\mathsf{P}\), and an exact rational unblocked allocation can be constructed in polynomial time.

The algorithm below adapts the SCFA pruning strategy of [Schlotter and Mendoza-Cadena](https://www.ifaamas.org/Proceedings/aamas2025/pdfs/p1867.pdf), replacing matching tests with transportation-flow tests. We prove its correctness directly for the mass model, including real-valued deviations and forbidden self-arcs.

1. Blocking deviations have a graph characterization

We work also with restricted instances on a nonempty set \(R\subseteq T\). Such an instance retains the original masses, preferences restricted to \(R\), and forbidden arcs restricted to \(R\times R\). The masses need not sum to one in a restricted instance.

Write \(E_R=E\cap(R\times R)\).

For a feasible allocation \(x\) on \(R\), define a directed graph \(G_x\) on \(R\). Include an arc \(t\to v\) precisely when there is some \(u\in R\) such that

\[ x_{t,u}>0,\qquad (t,v)\in E_R,\qquad \neg(u\succ_t v). \]

Mark this arc strict if a witness \(u\) also satisfies \(v\succ_t u\). An arc can have several witnesses; it is marked strict whenever at least one witness gives a strict improvement.

Forbidden arcs do not enter this definition, because they do not restrict deviations.

Lemma 1. An allocation \(x\) is blocked if and only if \(G_x\) contains a directed cycle with a strict arc.

Proof. Suppose such a cycle exists. We may choose a simple directed cycle containing a strict arc, allowing a loop as a cycle. For each cycle arc \(t\to v\), choose a witnessing current house \(u_t\), choosing a strict witness for one strict arc.

Choose a positive \(\varepsilon\) no larger than every \(x_{t,u_t}\) on the cycle. Set \(z_{t,u_t,v}=\varepsilon\) on its arcs and set all other entries to zero. Each cycle vertex contributes and receives exactly \(\varepsilon\). The capacity and preference conditions hold by construction, and some positive mass strictly improves. Thus this is a blocking deviation.

Conversely, let \(z\) be a blocking deviation and put

\[ f_{t,v}=\sum_{u\in R}z_{t,u,v}. \]

The deviation’s balance constraints say that \(f\) is a nonnegative circulation. Every positive arc of a nonnegative circulation lies on a directed cycle. To verify this fact, consider a positive arc \(a\to b\), and let \(W\) consist of vertices reachable from \(b\) through positive arcs. If \(a\notin W\), no positive arc leaves \(W\), whereas \(a\to b\) enters it. Summing flow conservation over \(W\) gives a contradiction.

The strict-improvement condition supplies a positive entry \(z_{t,u,v}\) with \(v\succ_t u\). Consequently, \(t\to v\) is a positive arc of \(f\) and a strict arc of \(G_x\). A cycle through this arc proves the claim. \(\square\)

Equivalently, \(x\) is unblocked precisely when no strict arc has both endpoints in the same strongly connected component of \(G_x\).

2. Structure forced by an unblocked allocation

Define the undominated acceptable arcs in the current instance by

\[ U_R=\{(t,u)\in E_R:\text{ there is no }v\in R \text{ with }(t,v)\in E_R\text{ and }v\succ_t u\}. \]

These arcs are computed using all acceptable destinations, including forbidden ones.

Lemma 2. Let \(x\) be unblocked on \(R\), and let \(P\) be a sink strongly connected component of \(G_x\). Then:

• No positive allocation entry crosses between \(P\) and \(R\setminus P\).
• Every positive entry with receiving type in \(P\) belongs to \(U_R\).
• Whenever \(t\in P\), \(x_{t,u}>0\), and \((t,v)\in E_R\) with \(v\notin P\), we have \(u\succ_t v\).
• The set \(P\) is a union of strongly connected components of \((R,U_R)\). For every such component \(C\subseteq P\), the restriction of \(x\) to \(C\times C\) has row and column sums \(\mu_t\).

Proof.

Every positive allocation entry \(x_{t,u}\) induces an arc \(t\to u\) in \(G_x\): its witness is the currently received house \(u\) itself. Since \(P\) has no outgoing graph arc, allocation mass cannot leave \(P\).

Let \(\mu(P)=\sum_{t\in P}\mu_t\). The rows indexed by \(P\) therefore place exactly \(\mu(P)\) mass inside \(P\times P\). The columns indexed by \(P\) also total \(\mu(P)\), so no mass can enter \(P\) from outside. This proves the first assertion.

Suppose \(x_{t,u}>0\), \(t\in P\), and \((t,u)\notin U_R\). There is an acceptable \(v\in R\) with \(v\succ_t u\). This creates a strict arc \(t\to v\) in \(G_x\). The sink property forces \(v\in P\). Both endpoints are then in one strongly connected component, contradicting Lemma 1. This proves the second assertion.

For the third assertion, if \(\neg(u\succ_t v)\), the positive entry \(x_{t,u}\) would witness an arc \(t\to v\) leaving \(P\). Hence \(u\succ_t v\).

Next, \(U_R\subseteq E(G_x)\). Indeed, for each \((t,v)\in U_R\), positivity of \(\mu_t\) supplies some \(u\) with \(x_{t,u}>0\). Such a house \(u\) is acceptable. Undominatedness of \(v\) implies \(\neg(u\succ_t v)\), so \(t\to v\) belongs to \(G_x\). Consequently, any strongly connected component of \((R,U_R)\) meeting \(P\) lies entirely inside \(P\).

Finally, \(x\) restricted to \(P\) is a circulation supported on \(U_R\). By the circulation fact proved in Lemma 1, each positive entry lies on a directed cycle of \(U_R\), and hence its endpoints belong to the same strongly connected component of \((R,U_R)\). Thus this restriction separates into allocations on those components, with the original row and column sums. \(\square\)

3. A group that can safely be removed

The following lemma supplies the recursive step.

Lemma 3. Suppose a nonempty set \(A\subseteq R\) admits an allocation \(y\) on \(A\times A\) with the original row and column sums, satisfying:

• Every positive entry of \(y\) belongs to \(U_R\setminus F\).
• For every \(y_{t,u}>0\) and every acceptable \(v\in R\setminus A\), we have \(u\succ_t v\).

Then:

• Combining \(y\) with any unblocked allocation on \(R\setminus A\) gives an unblocked allocation on \(R\).
• Every unblocked allocation on \(R\) restricts to an unblocked allocation on \(R\setminus A\).

Proof of the first assertion. In the combined allocation, no graph arc leaves \(A\): every currently received house of a type in \(A\) strictly dominates every acceptable destination outside \(A\).

Furthermore, no strict graph arc leaves any vertex in \(A\), even to another vertex in \(A\), because every currently received house there is undominated among acceptable houses in \(R\).

A directed cycle therefore cannot cross between \(A\) and its complement, and a cycle inside \(A\) has no strict arc. A cycle inside the complement is governed by its unblocked allocation. Lemma 1 proves the assertion.

Proof of the second assertion. Let \(x\) be any unblocked allocation on \(R\). Define a potential deviation by

\[ z_{t,u,v}=\frac{x_{t,u}y_{t,v}}{\mu_t} \quad\text{for }t,v\in A,\ u\in R, \]

and set all other entries to zero.

The division is valid because every listed mass is positive. For \(t\in A\),

\[ \sum_{v\in A}z_{t,u,v} =\frac{x_{t,u}}{\mu_t}\sum_{v\in A}y_{t,v} =x_{t,u}. \]

Thus the capacity constraints hold. Every positive destination \(v\) is acceptable and undominated. Since any current house \(u\) with \(x_{t,u}>0\) is acceptable, undominatedness implies \(\neg(u\succ_t v)\). All preference conditions therefore hold.

Each type \(t\in A\) contributes exactly \(\mu_t\), while each house type \(v\in A\) receives

\[ \sum_{t\in A,\ u\in R}z_{t,u,v} =\sum_{t\in A}y_{t,v} =\mu_v. \]

Vertices outside \(A\) contribute and receive zero. Hence the deviation balances.

If any positive entry of \(x\) leaves \(A\), say \(x_{t,u}>0\) with \(t\in A\) and \(u\notin A\), every destination positively used by \(y\) for type \(t\) strictly dominates \(u\). The displayed deviation then has positive strict-improvement mass, contradicting unblockedness.

Thus no allocation mass leaves \(A\). Equality of total row and column mass on \(A\) also prevents incoming mass. Consequently, \(x\) restricts to a feasible allocation on \(R\setminus A\). Any blocking deviation for that restriction, extended by zero, would block \(x\). The restriction is therefore unblocked. \(\square\)

4. The algorithm

A transportation test on a set \(C\) and arc set \(B\subseteq C\times C\) asks whether a nonnegative matrix supported on \(B\) has row and column sums \(\mu_t\), and returns such a matrix when one exists.

Define the recursive procedure \(\mathrm{Solve}(R)\).

• If \(R=\varnothing\), return the empty allocation.
• Compute \(U_R\) and the family \(\mathcal C\) of strongly connected components of \((R,U_R)\).
• While \(\mathcal C\neq\varnothing\), let \(A=\bigcup_{C\in\mathcal C}C\). For each \(C\in\mathcal C\), define

\[ B_C(A)=\{(t,u)\in U_R\setminus F: t,u\in C,\ u\succ_t v\text{ for every }v\in R\setminus A \text{ with }(t,v)\in E_R\}. \]

Perform a transportation test on \(C\) using \(B_C(A)\).

• If some tests fail, remove all failed components from \(\mathcal C\) and repeat.
• If all tests succeed, combine their returned allocations into \(y\) on \(A\). Recursively call \(\mathrm{Solve}(R\setminus A)\). Return its allocation combined with \(y\), or report infeasibility if the recursive call reports infeasibility.

• If \(\mathcal C\) becomes empty, report infeasibility.

Each failed iteration removes a component. Each recursive call removes a nonempty set of types. Thus the procedure terminates.

5. Correctness

Theorem. The procedure reports infeasibility exactly when no unblocked allocation exists. Otherwise it returns an unblocked allocation.

Proof. We use induction on \(|R|\), with the empty instance as the base case.

First suppose an unblocked allocation \(x\) exists on a nonempty \(R\). Choose a sink strongly connected component \(P\) of \(G_x\). By Lemma 2, \(P\) is a nonempty union of components of \((R,U_R)\).

We claim that every component contained in \(P\) remains in \(\mathcal C\) throughout pruning. Initially this holds because \(\mathcal C\) contains all components.

Suppose it holds before an iteration, so \(P\subseteq A\). For any component \(C\subseteq P\), Lemma 2 supplies a transportation allocation \(x|_{C\times C}\) supported on \(U_R\setminus F\). Every acceptable destination outside \(A\) is also outside \(P\). Lemma 2 therefore says that every positive entry of this restriction dominates every such destination. The restriction is supported on \(B_C(A)\), so its transportation test succeeds. Hence \(C\) is retained, proving the invariant.

It follows that pruning cannot empty \(\mathcal C\) when an unblocked allocation exists.

If all tests succeed, their union \(y\) satisfies the hypotheses of Lemma 3. By its second assertion, existence of an unblocked allocation on \(R\) implies existence on \(R\setminus A\). The induction hypothesis then prevents a false rejection by the recursive call.

Conversely, suppose the procedure returns an allocation. Its recursive allocation is unblocked by induction. The matrices produced by the successful transportation tests together satisfy Lemma 3, whose first assertion proves that the combined allocation is unblocked.

This proves both directions. The argument applies to arbitrary real feasible allocations; it makes no prior rationality assumption. \(\square\)

6. Exact construction and running time

Write each input mass as \(\mu_t=p_t/d_t\), with positive integer numerator and denominator. Set

\[ D=\prod_{t\in T}d_t,\qquad Q_t=D\mu_t. \]

Every \(Q_t\) is a positive integer. The binary length of \(D\) is \(O(L)\), and \(\sum_{t\in T}Q_t=D\).

For a transportation test on \(C\), construct a network with a source, one row vertex for each type in \(C\), one column vertex for each house type in \(C\), and a sink:

• The source-to-row capacity for \(t\) is \(Q_t\).
• For each \((t,u)\in B\), add a row-to-column arc of capacity \(D\).
• The column-to-sink capacity for \(u\) is \(Q_u\).

The test succeeds precisely when the maximum-flow value is \(\sum_{t\in C}Q_t\). Such a flow saturates every source-to-row and column-to-sink arc, giving the required margins. Conversely, any feasible transportation matrix, scaled by \(D\), gives a flow of that value.

All capacities are nonnegative integers of \(O(L)\) bits. The standard Edmonds–Karp algorithm finds an integral maximum flow in \(O(VE^2)\) arithmetic operations, independent of capacity magnitudes. Its integrality follows also directly from augmenting integral flows by integral residual capacities. Dividing the resulting row-to-column flows by \(D\) therefore gives exact rational entries.

There are at most \(\tau\) recursion levels and at most \(\tau+1\) testing batches per level. Within one batch, the tested components are disjoint. Their networks collectively have \(O(\tau+m)\) vertices and \(O(\tau m+\tau+m)\) arcs. Summing the Edmonds–Karp bounds over these networks is at most

\[ O\bigl((\tau+m)(\tau m+\tau+m)^2\bigr) \]

arithmetic operations. All integer operands have \(O(L)\) bits. Using a conservative \(O(L^2)\) allowance per arithmetic operation, including preprocessing, gives the overall bit-complexity bound

\[ O\bigl(\tau^2(\tau+m)(\tau m+\tau+m)^2L^2\bigr). \]

Preference-table preparation, undominated-arc computation, strongly connected components, and eligibility checks also fit within this bound. Since the problem requires \(m=\tau\), it simplifies to

\[ O(\tau^7L^2)=O(m^7L^2). \]

Every returned entry has denominator \(D\) and an \(O(L)\)-bit numerator, so the allocation’s total encoding length is \(O(\tau mL)\). No expansion into individual agents is needed.

⟨structured verdict parsed — rendered above⟩

The output resolves the assigned mass problem. The proof is correct for arbitrary real deviations, and the algorithm constructs an exact rational unblocked allocation in polynomial time. I found no major or minor mathematical issues.

• Definitions and restricted instances.

Restricting to \(R\subseteq T\) preserves the relevant acceptability condition: for \(t,v\in R\), membership in \(E_R\) still means \(\neg(t\succ_t v)\). Keeping the original masses is consistent with both allocation margins and deviation balance; normalization to total mass one is unnecessary in restricted instances.

The graph definition correctly includes incomparability through \(\neg(u\succ_t v)\). Strictness is existential over witnesses, as required: a destination may be weakly acceptable from several currently allocated houses and strictly better than only one.

Forbidden arcs are excluded from allocations but retained as possible deviation destinations throughout the argument. This matches USER_TASK, including when self-arcs are forbidden.

• Lemma 1: characterization of blocking deviations.

The cycle-to-deviation construction is valid. On a simple directed cycle, each participating type appears once, so choosing a positive amount bounded by every selected allocation entry satisfies all capacity constraints. Every cycle vertex contributes and receives the same amount. Selecting a strict witness for one marked arc ensures positive strict-improvement mass.

The reverse direction also holds. Aggregating a deviation into \(f_{t,v}=\sum_u z_{t,u,v}\) produces precisely a nonnegative circulation under the stated balance constraints. Every positive aggregated arc belongs to \(G_x\), because a positive deviation entry implies a positive current allocation entry and satisfies both preference conditions.

The reachability argument establishing that every positive circulation arc lies on a cycle is correct: if the tail were outside the set reachable from the head, that set would have positive incoming flow and no positive outgoing flow, contradicting conservation. A strictly improving deviation entry therefore supplies a strict graph arc on a directed cycle.

The equivalent strongly connected component criterion follows correctly. These arguments apply to real flows; no integrality or rationality assumption enters.

• Lemma 2: structure of a sink component.

All four assertions are justified.

• Every positive allocation entry induces a graph arc using its own destination as witness. The sink property therefore prevents allocation mass from leaving \(P\). Equality of total row and column mass on \(P\) then prevents incoming mass.
• If a positive allocation destination for a type in \(P\) were dominated by an acceptable destination, that destination would induce a strict graph arc. The sink property places its endpoint in \(P\), contradicting Lemma 1.
• For any acceptable destination outside \(P\), failure of strict dominance by the currently received house would create an outgoing graph arc. Thus the claimed strict dominance is necessary.
• The inclusion \(U_R\subseteq E(G_x)\) is valid: positive row mass supplies an acceptable current house, and undominatedness excludes that house strictly dominating the undominated destination. Consequently, an entire strongly connected component of \((R,U_R)\) lies in \(P\) whenever it meets \(P\).

Finally, the restriction to \(P\) is a circulation supported on \(U_R\). The circulation fact from Lemma 1 places every positive allocation entry within one strongly connected component of \((R,U_R)\). Together with the absence of mass crossing \(P\), this establishes the original margins separately on each component \(C\subseteq P\).

• Lemma 3: safe removal and restriction.

The first assertion correctly establishes unblockedness of the combined allocation. The strict-dominance condition prevents graph arcs from leaving \(A\), while undominatedness prevents any strict graph arc with its tail in \(A\). Thus no blocking cycle can cross the boundary or occur inside \(A\). Graph arcs within the complement are exactly those governed by its restricted allocation and preferences.

The second assertion is the crucial necessity argument, and its displayed construction is valid.

• Division by \(\mu_t\) is permitted because every listed mass is positive.
• Summing over destinations gives exactly \(x_{t,u}\) for participating types, so capacities hold.
• Every positive destination is acceptable and undominated among acceptable houses in \(R\). Since every positive current allocation destination is acceptable, the required weak preference condition follows.
• Row and column sums of \(y\) give contributions and receipts equal to \(\mu_t\) at each vertex in \(A\), with zero contributions and receipts outside \(A\).

The construction is initially a balanced, capacity-feasible array satisfying the preference conditions; it need not strictly improve anyone unless allocation mass leaves \(A\). The proof handles this distinction correctly. If such outgoing mass exists, every positive destination in the corresponding row of \(y\) strictly dominates that outside current house, so the constructed array becomes a blocking deviation.

Hence no mass leaves \(A\), and equal total margins prevent incoming mass. Restriction to the complement is feasible. Extending any blocking deviation there by zero preserves every constraint and would block the original allocation. Both assertions follow without assuming rationality of \(x\).

• Pruning and recursive correctness.

The algorithm’s transportation tests enforce exactly the hypotheses of Lemma 3 when they all succeed: their supports are undominated and non-forbidden, and every positive assigned destination dominates every acceptable destination outside their union \(A\).

The pruning invariant is valid. Given an unblocked allocation, Lemma 2 supplies a nonempty sink component \(P\) that is a union of undominated-graph components. As long as its components remain in the candidate family, \(P\subseteq A\). Each restriction \(x|_{C\times C}\), for \(C\subseteq P\), satisfies its transportation test because every destination outside \(A\) is outside \(P\). Therefore none of these components can be removed, even when all failed components are removed simultaneously.

This proves that pruning cannot exhaust the candidates when an unblocked allocation exists. When the algorithm selects a successful union, Lemma 3’s second assertion ensures that its complement still admits an unblocked allocation. The induction hypothesis therefore rules out a false recursive rejection.

Conversely, every returned allocation is feasible by combination of allocations on disjoint sets, and Lemma 3’s first assertion proves unblockedness. The empty-instance base case is valid. Every recursive call removes a nonempty set, and every failed pruning iteration removes at least one component, so termination is established.

The attribution to SCFA is consistent with the cited paper’s component-pruning procedure. The mass-model correctness proof is supplied independently rather than inferred from the finite-agent result. [Schlotter and Mendoza-Cadena](https://www.ifaamas.org/Proceedings/aamas2025/pdfs/p1867.pdf).

• Transportation tests and exact rational construction.

The denominator construction is correct. Each denominator divides \(D\), so \(Q_t=D\mu_t\) is a positive integer. The product has \(O(L)\) bits, and normalization of the original masses gives \(\sum_t Q_t=D\).

The flow network has equal total source and sink capacities, namely \(\sum_{t\in C}Q_t\). A flow attaining this value saturates every margin arc and produces the required transportation matrix. Conversely, any real feasible matrix, scaled by \(D\), yields a feasible flow of that value. Capacity \(D\) on each internal arc is sufficient because no entry can exceed its row margin, which is at most \(D\).

The invocation of Edmonds–Karp states the relevant bound correctly, and the constructed networks satisfy its hypotheses. Its running time is independent of capacity magnitudes. [Cornell’s algorithm notes](https://www.cs.cornell.edu/courses/cs4820/2019sp/handouts/edmondskarp.pdf).

The written integral-augmentation argument establishes integral returned flows. Thus real transportation feasibility is detected exactly, while successful tests return rational entries with denominator \(D\). There is no assumption that an initially existing unblocked allocation already has this denominator.

• Running time, encoding size, and edge cases.

There are at most \(\tau\) nonempty recursive levels and at most \(\tau+1\) testing batches per level, giving \(O(\tau^2)\) batches.

Within a batch, disjointness of the components justifies the aggregate vertex and arc bounds. Summing the individual Edmonds–Karp bounds is bounded by the stated product of total vertices and squared total arcs. Capacities, flows, residual capacities, and flow values have \(O(L)\)-bit representations. The conservative arithmetic allowance therefore yields the claimed bit bound
\[ O\bigl(\tau^2(\tau+m)(\tau m+\tau+m)^2L^2\bigr). \]
With \(m=\tau\), its simplification to \(O(\tau^7L^2)\) is correct. Preference processing and eligibility checks fit within this bound, as does denominator preprocessing.

Each output numerator is at most \(D\), so the stated \(O(\tau mL)\) allocation encoding bound is valid.

Singleton instances, forbidden self-arcs, components without feasible transportation, unequal masses, and empty recursive complements are covered by the general procedure. No expansion into individual agents is used.

No repair or additional clarification is needed. The central progress is the proved necessity of safe removal in Lemma 3, combined with the pruning invariant; together they justify the polynomial algorithm for the exact mass model.

⟨structured verdict parsed — rendered above⟩