← back to the atlas

Stable Marriage with Covering Constraints-A Complete Computational Trichotomy (d4-conf-sagt-2017-0020)

Answer: —

The anchor (named result in the paper)

Theorem 9 — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximateSMC-1 is NP-hard even if ∆W = 2 and ∆M = 3.

statement extracted from the paper’s text layer; consult the paper for the exact wording

The continuous mirror question, as graded

Given rational masses μ_i and ν_j on male and female types, with each type specifying acceptable counterpart types, a strict order over them, and whether it is distinguished, find a mass matching x covering all distinguished female mass and minimizing \(\operatorname{BP}(x)=\sum_{(i,j)\in E}u^M_{ij}(x)u^W_{ji}(x)\), where every female type has at most two acceptable male types and every male type has at most three acceptable female types; equivalently, decide whether \(\operatorname{BP}(x)\le B\).

Packaged proof task (what the prover saw — nothing else)

A society is given by its support: male types \(M\) and female types \(W\), each with positive binary-rational mass \(\mu_i\) or \(\nu_j\). Let \(\tau=|M|+|W|\) be the support size, not the number of possible types; let \(m=|E|\) count mutually acceptable type pairs and \(L\) be the total input bit length. Masses need not sum to one or have equal totals on the two sides.
Each type strictly ranks its acceptable counterpart types, all above being unmatched. Acceptability is mutual; each female list has length at most two and each male list at most three. A subset \(W^\star\subseteq W\) is distinguished; there are no distinguished male types.
A mass matching has real entries \(x_{ij}\geq0\) on \(E\), with \(\sum_{j:(i,j)\in E}x_{ij}\leq\mu_i\) and \(\sum_{i:(i,j)\in E}x_{ij}\leq\nu_j\); feasibility requires equality in the latter constraint for every \(j\in W^\star\). Remaining mass is unmatched.
For \((i,j)\in E\), define \(u^M_{ij}(x)=\mu_i-\sum_{k:(i,k)\in E,\ k\succeq_i j}x_{ik}\) and \(u^W_{ji}(x)=\nu_j-\sum_{h:(h,j)\in E,\ h\succeq_j i}x_{hj}\), where \(\succeq\) includes equality. These are the masses unmatched or assigned to strictly worse types. Set \(\operatorname{BP}(x)=\sum_{(i,j)\in E}u^M_{ij}(x)u^W_{ji}(x)\).

Given a binary-rational threshold \(B\geq0\), is deciding whether a feasible mass matching \(x\) satisfies \(\operatorname{BP}(x)\leq B\) solvable in polynomial time in \(m,\tau,L\), or is it NP-hard?

The discrete problem of covering distinguished women while minimizing blocking pairs is NP-hard with female lists of length at most two and male lists of length at most three ([Mnich–Schlotter](https://arxiv.org/abs/1602.08230v3)).
For fractional bipartite matchings with strict preferences, maximizing welfare or the number of fully matched agents subject to ordinal stability is polynomial-time solvable ([Chen–Roy–Sorge](https://www.ijcai.org/proceedings/2021/0013.pdf)); those objectives differ from the product objective above. No result settling this exact mass problem was located.

Modeling choices made when packaging the task

Prover output (gpt-6.1-sol / high, Bolzano prover prompt)

Status: partial progress

The general problem with female lists of length at most $2$ and male lists of length at most $3$ remains unresolved here.

The new result is a polynomial-time algorithm for all thresholds and arbitrary rational masses when both sides’ lists have length at most $2$. More generally, I give an exact decomposition that isolates the terms preventing the same convexity argument from handling male lists of length $3$.

1. An exact decomposition of the objective

Let $V=M\cup W$. Write $x_e=x_{ij}$ for an acceptable pair $e=(i,j)$, and define
$$ s_v(x)=\sum_{e\ni v}x_e. $$
For $e=(i,j)$, let
$$ A_e(x)=\sum_{h\succ_i j}x_{ih}, \qquad C_e(x)=\sum_{g\succ_j i}x_{gj}. $$
Thus $A_e$ and $C_e$ count assignments strictly preferred to $e$ at its male and female endpoints, respectively. The dissatisfaction quantities are
$$ u^M_e=\mu_i-x_e-A_e, \qquad u^W_e=\nu_j-x_e-C_e. $$

Expanding the objective gives
$$ \operatorname{BP}(x)=c+\ell(x)+Q(x), $$
where
$$ c=\sum_{(i,j)\in E}\mu_i\nu_j, $$
$$ \ell(x)=- \sum_{e=(i,j)\in E} \left[ \nu_j(x_e+A_e(x))+ \mu_i(x_e+C_e(x)) \right], $$
and the homogeneous quadratic part is
$$ Q(x)=\sum_{e\in E}(x_e+A_e(x))(x_e+C_e(x)). $$

Lemma 1. For arbitrary strict preference lists,
$$ Q(x)= \frac12\sum_{v\in V}s_v(x)^2+ \sum_{e\in E}A_e(x)C_e(x). $$

Proof. Expanding $Q$ yields
$$ Q(x)= \sum_e x_e^2+ \sum_e x_e(A_e+C_e)+ \sum_e A_eC_e. $$
At a fixed vertex, each unordered pair of distinct incident edges contributes exactly once to the middle sum: it contributes through the less-preferred edge, whose strict-better sum contains the more-preferred edge. Consequently,
$$ \sum_e x_e(A_e+C_e) = \sum_{v\in V} \sum_{\substack{\{e,f\}\subseteq E\\e,f\ni v,\ e\ne f}} x_ex_f. $$
Every edge has two endpoints. Therefore
$$ \frac12\sum_{v\in V}s_v^2 = \sum_e x_e^2+ \sum_{v\in V} \sum_{\substack{\{e,f\}\subseteq E\\e,f\ni v,\ e\ne f}} x_ex_f. $$
Substitution proves the identity. $\square$

These are polynomial identities, valid even for signed vectors $x$; feasibility is not needed.

2. A sum-of-squares formula under the stated list bounds

From now on, assume female lists have length at most $2$ and male lists have length at most $3$.

Define two sets of acceptable pairs:

For $e\in R$, let $a(e)$ be the first-choice edge at its male endpoint, and let $b(e)$ be the first-choice edge at its female endpoint.

Because every nonisolated vertex has a unique last-choice edge, distinct edges of $D$ have disjoint endpoints. Let $V(D)$ denote their endpoints.

Define
$$ Q_0(x)= \frac12\sum_{v\notin V(D)}s_v(x)^2 + \frac12\sum_{e=(i,j)\in D} \left[ (s_i(x)+s_j(x)-x_e)^2+x_e^2 \right]. $$

Theorem 2. Under the stated list bounds,
$$ \boxed{ \operatorname{BP}(x) = c+\ell(x)+Q_0(x)+ \sum_{e\in R}x_{a(e)}x_{b(e)}. } $$
In particular, $Q_0$ is positive semidefinite.

Proof. We first classify the products $A_eC_e$ in Lemma 1.

If an edge is ranked first at either endpoint, the corresponding strict-better sum is zero, so $A_eC_e=0$.

Suppose instead that both strict-better sums are nonzero. The female endpoint must have two acceptable men and rank $e$ second.

At the male endpoint there are exactly two possibilities:

$$ A_e=s_i-x_e, \qquad C_e=s_j-x_e. $$

$$ A_e=x_{a(e)}, \qquad C_e=x_{b(e)}. $$

This exhausts the possibilities. Edges in $D$ that are also first choices at an endpoint have a zero strict-better sum there, and the same formula remains valid. Hence
$$ \sum_e A_eC_e = \sum_{e=(i,j)\in D}(s_i-x_e)(s_j-x_e) + \sum_{e\in R}x_{a(e)}x_{b(e)}. $$

For every $e=(i,j)\in D$, direct expansion gives
$$ \frac12s_i^2+\frac12s_j^2+(s_i-x_e)(s_j-x_e) = \frac12(s_i+s_j-x_e)^2+\frac12x_e^2. $$
The edges in $D$ have disjoint endpoints, so these replacements use disjoint terms of $\frac12\sum_v s_v^2$. Applying them to Lemma 1 gives the claimed decomposition.

Finally, $Q_0$ is a sum of squares of linear functions, with nonnegative coefficients. Thus $Q_0(x)\geq0$ for every real vector $x$, which proves positive semidefiniteness. $\square$

3. A polynomial-time solvable case for every threshold

Corollary 3. If $R=\varnothing$, the decision problem is polynomial-time solvable in $m,\tau,L$, for arbitrary positive rational masses, arbitrary $W^\star$, and every rational threshold $B\geq0$.

In particular, this holds when both male and female preference lists have length at most $2$.

Proof. Let $P$ be the feasible set specified in the question. It is a rational polytope: its constraints are linear, with rational right-hand sides. It has $m$ variables and a polynomial number of constraints.

Every coordinate satisfies
$$ 0\leq x_{ij}\leq\min\{\mu_i,\nu_j\}, $$
so $P$ is bounded. An empty $P$ gives a no-instance.

When $R=\varnothing$, Theorem 2 gives
$$ \operatorname{BP}(x)=c+\ell(x)+Q_0(x). $$
The objective is convex because its quadratic part is positive semidefinite.

We use the exact convex quadratic programming theorem of Kozlov–Tarasov–Khachiyan: a quadratic objective with rational positive-semidefinite Hessian, minimized under rational linear constraints, admits a polynomial-time algorithm that detects infeasibility and, when a finite optimum exists, computes the exact optimal value. Their theorem is formulated for integer data; clearing denominators extends it to rational data with polynomial increase in encoding length. [Kozlov–Tarasov–Khachiyan, *The polynomial solvability of convex quadratic programming*](https://www.mathnet.ru/eng/zvmmf5189)

All hypotheses hold here:

Compute the exact minimum and compare it with $B$. This handles equality at the threshold as well as strict inequality.

If male lists have length at most $2$, no edge meets the definition of $R$, proving the stated special case. No balance or normalization of the masses was used. $\square$

This also gives a tractable subclass allowing male lists of length $3$: it suffices that no man’s middle-ranked pair is simultaneously the less-preferred pair of its female endpoint.

4. Quantifying the remaining nonconvexity

The decomposition also gives a bound on the number of negative eigenvalues.

Proposition 4. Let $k=|R|$, and let $H$ be the Hessian of $\operatorname{BP}$. Then $H$ has at most $k$ negative eigenvalues, counted with multiplicity.

Moreover, fixing the coordinates $x_{a(e)}$ for all $e\in R$ makes the objective convex in the remaining coordinates. For prescribed rational values of those coordinates, the resulting constrained decision problem is polynomial-time solvable.

Proof. Consider the linear subspace
$$ T=\{z\in\mathbb R^m:z_{a(e)}=0\text{ for every }e\in R\}. $$
Its codimension is at most $k$. On this subspace, every residual product vanishes, so Theorem 2 gives
$$ \frac12z^{\mathsf T}Hz=Q(z)=Q_0(z)\geq0. $$

If the negative eigenspace of $H$ had dimension greater than $k$, it would intersect $T$ in a nonzero vector. The quadratic form would be strictly negative on that vector, contradicting the displayed inequality.

After fixing $x_{a(e)}=\alpha_e$, every residual product becomes the linear term
$$ \alpha_e x_{b(e)}. $$
The remaining quadratic part is the restriction of the positive-semidefinite form $Q_0$. The feasible constraints remain rational and linear when the prescribed values are rational. Corollary 3’s quadratic programming argument therefore applies, with input length including the prescribed values. $\square$

This proposition does not provide a global algorithm: the optimal values of the fixed coordinates are still unknown.

One residual term already permits nonconvexity

The bound in Proposition 4 cannot be replaced by a claim that the objective remains convex whenever $k$ is small.

Consider men $a,b,c,d$ with masses
$$ \mu_a=2, \qquad \mu_b=\mu_c=\mu_d=1, $$
and five distinguished women, each of mass $1$. Preferences are:

| Type | Preference list |
|---|---|
| $a$ | $w_{da}\succ w_{ab}\succ w_{ac}$ |
| $b$ | $w_{ab}\succ w_{bd}$ |
| $c$ | $w_{ac}\succ w_{cd}$ |
| $d$ | $w_{bd}\succ w_{cd}\succ w_{da}$ |
| $w_{ab}$ | $a\succ b$ |
| $w_{ac}$ | $a\succ c$ |
| $w_{bd}$ | $b\succ d$ |
| $w_{cd}$ | $c\succ d$ |
| $w_{da}$ | $d\succ a$ |

Here
$$ R=\{(d,w_{cd})\}, $$
so $k=1$.

For $p,q\geq0$ with $p+q\leq1$, allocate:

| Woman | Mass to first choice | Mass to second choice |
|---|---:|---:|
| $w_{ab}$ | $1-p$ | $p$ |
| $w_{ac}$ | $1-q$ | $q$ |
| $w_{bd}$ | $1-p$ | $p$ |
| $w_{cd}$ | $1-q$ | $q$ |
| $w_{da}$ | $1-p-q$ | $p+q$ |

Every woman is saturated. The male totals are
$$ (p+q)+(1-p)+(1-q)=2, $$
$$ p+(1-p)=1, \qquad q+(1-q)=1, $$
and
$$ p+q+(1-p-q)=1. $$
Thus the allocations are feasible.

Every woman’s dissatisfaction toward her second-choice man is zero. For the first-choice pairs involving $w_{ac},w_{bd},w_{cd},w_{da}$, the man ranks that woman last and is saturated, so his dissatisfaction is zero.

Only $(a,w_{ab})$ can contribute. Its two factors are
$$ u^M_{a,w_{ab}}=2-(p+q)-(1-p)=1-q, $$
$$ u^W_{w_{ab},a}=p. $$
Consequently,
$$ \operatorname{BP}(p,q)=p(1-q). $$

Along the feasible affine segment $p=q=t$, with $0\leq t\leq\frac12$,
$$ \operatorname{BP}(t,t)=t-t^2. $$
At its midpoint,
$$ \operatorname{BP}\left(\frac14,\frac14\right) =\frac{3}{16} > \frac18 = \frac12\left( \operatorname{BP}(0,0)+ \operatorname{BP}\left(\frac12,\frac12\right) \right). $$
Hence the objective is not convex on the feasible set.

This segment also supplies a direction of strictly negative curvature. Proposition 4 bounds the number of negative eigenvalues by $1$, so the Hessian in this example has exactly one negative eigenvalue. Disjoint copies show that the bound of $k$ negative eigenvalues is attained for every positive integer $k$.

5. Polynomial-size certificates for the general problem

For completeness, the general problem belongs to $\mathrm{NP}$. This statement is useful if a future reduction establishes hardness.

Proposition 5. Every yes-instance has a rational feasible witness of polynomial encoding length.

Proof. Write
$$ q(x)=\operatorname{BP}(x) =\frac12x^{\mathsf T}Hx+h^{\mathsf T}x+c. $$
The coefficients have polynomial encoding length.

For a yes-instance, the compact feasible polytope $P$ is nonempty, so $q$ has a global minimizer $x^\ast$. Let $F$ be the smallest face of $P$ containing $x^\ast$. Then $x^\ast$ lies in the relative interior of $F$.

Choose independent active input constraints describing
$$ \operatorname{aff}(F)=\{x:Cx=d\}. $$
Let the columns of $U$ form a rational basis of $\ker C$. Gaussian elimination produces such a basis with polynomial encoding length.

Every direction in $\ker C$ permits sufficiently small perturbations of both signs from $x^\ast$ within $F$. First-order optimality therefore gives
$$ U^{\mathsf T}(Hx^\ast+h)=0. $$
Define the rational polytope
$$ S=\{x\in P:Cx=d,\ U^{\mathsf T}(Hx+h)=0\}. $$
It is nonempty and bounded.

The objective is constant on $S$. Indeed, for $a,b\in S$, put $z=b-a$. Since $Cz=0$, stationarity at both points gives
$$ z^{\mathsf T}(Ha+h)=z^{\mathsf T}(Hb+h)=0. $$
Subtracting yields $z^{\mathsf T}Hz=0$. Thus
$$ q(b)-q(a) = z^{\mathsf T}(Ha+h)+\frac12z^{\mathsf T}Hz =0. $$
Every point of $S$ therefore has the global minimum value.

A nonempty bounded polytope has a vertex. At a vertex of $S$, a nonsingular subsystem of its active constraints determines all coordinates. Those constraints have rational coefficients of polynomial encoding length. Clearing denominators and applying Cramer’s rule gives polynomial bit bounds for the coordinates: determinants of matrices of polynomial dimension and polynomial-bit entries themselves have polynomial bit length.

Hence $S$ contains a polynomial-size rational global minimizer. In a yes-instance, this point has objective at most $B$. Exact rational arithmetic verifies its feasibility and objective comparison in polynomial time. $\square$

6. What remains open

The decomposition settles every threshold when both sides’ lists have length at most $2$, and identifies the additional bilinear terms present under the requested length-three male bound.

It does not settle how to optimize those residual terms globally. Nonconvexity, including the example with just one residual term, is not a hardness proof. A complete classification still requires either a polynomial-time algorithm for the full objective or a reduction that controls all fractional feasible allocations.

⟨structured verdict parsed — rendered above⟩

Adversarial review (gpt-6.1-sol / medium, Bolzano verifier prompt)

Verification report

Result: partial. The output establishes correct, rigorous partial results: an exact decomposition, polynomial-time solvability for the stated subclass, a sharp bound on negative eigenvalues, a feasible nonconvexity example, and membership of the general decision problem in $\mathrm{NP}$.

It does not classify the full problem in USER_TASK. The prover explicitly acknowledges this limitation. I found no false mathematical step or substantive gap in the partial results.

1. Objective expansion and Lemma 1

The definitions of $A_e$ and $C_e$ correctly exclude the edge $e$ itself. Consequently,
$$ u^M_e=\mu_i-x_e-A_e, \qquad u^W_e=\nu_j-x_e-C_e $$
agree with the task’s dissatisfaction quantities.

Expanding their product gives exactly the stated constant, linear, and quadratic parts. All signs and coefficients are correct.

In Lemma 1, each unordered pair of incident edges contributes once to
$$ \sum_e x_e(A_e+C_e), $$
because strict preferences select exactly one less-preferred edge in that pair. Also, each edge’s square occurs twice in $\sum_v s_v^2$, once at each endpoint. Thus
$$ Q(x)=\frac12\sum_v s_v(x)^2+\sum_e A_e(x)C_e(x) $$
is correct.

No feasibility assumption enters this calculation, so the claimed extension to signed vectors is justified.

Finding: verified.

2. Theorem 2: sum-of-squares decomposition

The sets $D$ and $R$ correctly classify every potentially nonzero product $A_eC_e$ under the list bounds.

If both strict-better sums are nonzero, the female endpoint necessarily ranks $e$ second on a list of length two. The male endpoint then either ranks $e$ last, placing it in $D$, or ranks it second on a list of length three, placing it in $R$. These possibilities exhaust the permitted ranks.

For an edge in $D$,
$$ A_e=s_i-x_e, \qquad C_e=s_j-x_e. $$
These identities remain valid when an endpoint has degree one: its corresponding difference is zero.

Distinct edges in $D$ have disjoint endpoints because each vertex has only one last-ranked edge. Therefore the proposed replacements do not reuse any vertex-square term.

The critical algebraic identity is correct:
$$ \frac12s_i^2+\frac12s_j^2+(s_i-x_e)(s_j-x_e) = \frac12(s_i+s_j-x_e)^2+\frac12x_e^2. $$

It follows that the displayed decomposition is exact. The formula for $Q_0$ is a sum of squares with nonnegative coefficients, so its positive semidefiniteness follows for all real vectors.

Finding: verified.

3. Corollary 3: exact polynomial-time solvability when $R=\varnothing$

The feasible set has $m$ variables and polynomially many rational linear constraints. Each edge coordinate is bounded by the masses at its endpoints. Thus the feasible set is bounded and closed; if nonempty, it is compact. Distinguished isolated women correctly produce infeasibility through their required saturation constraints.

When $R=\varnothing$, the objective’s quadratic part is $Q_0$, so the objective is convex.

The cited theorem supplies the exact computation claimed, rather than merely approximate optimization. The original paper defines exact solution to include detecting feasibility, determining boundedness below, and computing the exact rational optimum and an attaining point; it establishes polynomial running time for integer positive-semidefinite quadratic data and integer linear constraints. [Kozlov–Tarasov–Khachiyan, original paper](https://www.mathnet.ru/php/getFT.phtml?jrnid=zvmmf&option_lang=eng&paperid=5189&what=fullt)

The application satisfies the hypotheses:

Exact comparison with $B$ therefore handles equality at the threshold. The specialization to lists of length at most two on both sides is correct because $R$ is then empty.

Finding: verified, including the exact threshold decision claim.

4. Proposition 4: negative eigenvalues and fixed coordinates

The subspace $T$ has codimension at most $k$, even if some designated coordinates coincide. On $T$, every residual product vanishes, leaving the nonnegative quadratic form $Q_0$.

If the negative eigenspace had dimension greater than $k$, the dimension bound would force a nonzero intersection with $T$. The Hessian’s quadratic form is strictly negative on every nonzero vector in its negative eigenspace, contradicting nonnegativity on $T$.

Fixing the designated coordinates converts each residual product into an affine term in the remaining variables. Restricting $Q_0$ preserves positive semidefiniteness. Prescribed rational values preserve rational linear constraints, so the cited quadratic-programming theorem applies with those values included in the input length. Inconsistent prescriptions simply produce infeasibility.

The proposition correctly does not claim that this yields a global algorithm.

Finding: verified.

5. Nonconvexity example and sharpness

The preference table respects mutual acceptability and the required list bounds. Inspection confirms
$$ R=\{(d,w_{cd})\}. $$

For the stated parameter domain, all allocated masses are nonnegative. Each woman receives total mass one, and the male totals are exactly
$$ 2,\quad 1,\quad 1,\quad 1. $$
Hence the entire parameterized family is feasible.

Every second-choice pair has zero female dissatisfaction because its woman is saturated. For the four identified first-choice pairs, the man is saturated and ranks that woman last, giving zero male dissatisfaction.

The remaining pair has factors
$$ u^M_{a,w_{ab}}=1-q, \qquad u^W_{w_{ab},a}=p. $$
Thus the objective calculation
$$ \operatorname{BP}(p,q)=p(1-q) $$
is correct.

On the affine feasible segment $p=q=t$, the midpoint and endpoint calculations are
$$ \operatorname{BP}\left(\frac14,\frac14\right)=\frac{3}{16}, \qquad \frac12\left(\operatorname{BP}(0,0)+ \operatorname{BP}\left(\frac12,\frac12\right)\right)=\frac18. $$
The strict inequality violates convexity.

The restriction has second derivative $-2$, so it supplies a direction of negative Hessian curvature. Together with Proposition 4, this establishes exactly one negative eigenvalue. Disjoint copies produce independent Hessian blocks and additive counts of residual edges, justifying sharpness for every positive integer $k$.

Finding: verified. This demonstrates nonconvexity, not computational hardness, as the prover correctly states.

6. Proposition 5: polynomial-size rational certificates

The argument does not assume convexity and is valid for the general objective.

A global minimizer exists on a nonempty compact feasible polytope. Its membership in the relative interior of its smallest containing face permits sufficiently small feasible perturbations of both signs along every direction in that face’s affine hull. The stated first-order stationarity condition therefore follows.

Selecting independent active input constraints to describe the affine hull is valid for a face of a polytope. A rational nullspace basis of polynomial encoding length can be obtained by Gaussian elimination.

The set $S$ is a nonempty bounded rational polytope: it contains $x^\ast$ and is contained in $P$.

For $a,b\in S$, their difference belongs to $\ker C$. Stationarity at both points gives the two displayed scalar equalities. Subtraction yields
$$ z^{\mathsf T}Hz=0, $$
and the exact quadratic difference formula then proves that $q$ is constant on $S$. Since $x^\ast\in S$, that constant is the global minimum.

A vertex of $S$ is determined by a full-rank subsystem of active constraints. The polynomial coefficient bounds and determinant bounds justify polynomial encoding length for its rational coordinates. This includes lower-dimensional polytopes; the active equations still determine a vertex uniquely in the ambient space.

Exact rational evaluation verifies both feasibility and the objective comparison in polynomial time. Thus the claimed membership in $\mathrm{NP}$ is established.

Finding: verified.

7. Remaining task-level issue and actionable feedback

Major completeness issue: the full classification requested by USER_TASK remains unresolved. The established polynomial-time algorithm applies when $R=\varnothing$; the general allowed instances may have residual bilinear terms.

Membership in $\mathrm{NP}$ and nonconvexity do not determine whether the decision problem is polynomial-time solvable or $\mathrm{NP}$-hard.

No clarification or expositional repair is needed for the verified partial results. Completing the assignment requires a substantive additional result: either a polynomial-time algorithm covering all permitted instances or a valid hardness reduction for the continuous feasible allocations. The write-up accurately identifies this outstanding requirement.

⟨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.