Answer: \(\mathrm{NP}\)-complete, already for \(C=1\) and equal dyadic type masses.
Theorem 6.1 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateLet 𝐼 be an sf instance with regret 𝑟. Finding a stable half-matching (or a GSP) of 𝐼 with a maximum value of rank 1 assignments, minimum value of rank 𝑟 assignments, or minimum egalitarian cost, is NP-hard. Motivated by this intractability result, we will give integer linear programming formulations (ILP) for these problems.
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>0\) summing to \(1\), integer capacities \(c_t\), strict rankings of partner types, and a rational bound \(B\), decide whether a stable half-matching exists with average rank-weighted cost at most \(B\). A realization assigns mass to finite individual portfolios of full partners and half-match incidences; portfolio masses sum to \(\mu_t\), capacities hold for each individual, and compatible incidences are paired into mass-preserving edges and half-match cycles. Stability uses the paper’s blocking condition interpreted over partner types.
A society is given by its support: a list of \(\tau\) types \(T\) with positive binary-rational masses \(\mu_t\), summing to \(1\); \(\tau\) is the support size, not the number of possible types. Each type has a binary-encoded integer capacity \(c_t\geq1\) and a strict complete ranking of partner types \(T\). Write \(r_t(s)\) for the rank of \(s\), starting at \(1\), and let \(B\in\mathbb Q\).
Individuals form disjoint atomless spaces \(X_t\) of mass \(\mu_t\). Distinct individuals of the same type may partner; self-partnership is forbidden. Partners of the same type are indifferent, with no additional tie-breaking.
A realization assigns individuals finite portfolios of distinct full partners and either zero or two distinct half-partners. Each type's portfolio masses are nonnegative reals summing to \(\mu_t\). Partner types may repeat within a portfolio.
Incidences must be realized by measurable, mass-preserving pairings between individuals: full edges have weight \(1\), half edges have weight \(\tfrac12\), and the half-edge graph consists of vertex-disjoint finite simple cycles of length at least \(3\). No individual pair has multiple edges.
Writing \(\theta(x)\) for the type of \(x\) and \(w_{xy}\in\{0,\tfrac12,1\}\) for pair weight, every individual satisfies \(\sum_y w_{xy}\leq c_{\theta(x)}\); an individual on a half-cycle is saturated. Unused capacity contributes zero cost.
Stability means that, after deleting a null set of individuals, every distinct pair \(x,y\) satisfies either \(w_{xy}=1\), or \(\sum_{z:\,\theta(z)\succeq_{\theta(x)}\theta(y)}w_{xz}=c_{\theta(x)}\), or the symmetric equality at \(y\). Thus half-matched pairs are also tested.
The average rank-weighted cost is \(\int_X\sum_y r_{\theta(x)}(\theta(y))w_{xy}\,d\nu(x)\), where \(\nu\) is population mass; both endpoints contribute. Decide whether a stable realization has cost at most \(B\).
Is this decision problem in \(\mathrm P\), or is it \(\mathrm{NP}\)-hard? State running times in \(m=|T|\), \(\tau\), the total input bit length \(L\), and \(C=\max_t c_t\); polynomial time refers to the binary input length.
For finite Stable Fixtures instances, minimizing egalitarian cost over stable half-matchings is NP-hard, already when every capacity is \(1\); an arbitrary stable half-matching is computable in polynomial time. [Source](https://arxiv.org/html/2505.11456v3)
Existence results are known for distributional many-to-many matching with finite portfolios, but concern a different stability model and do not classify this half-cycle cost problem. [Source](https://www2.uibk.ac.at/downloads/c9821000/wpaper/2026-02.pdf)
The problem is \(\mathrm{NP}\)-complete, already when \(C=1\) and all type masses are equal dyadic rationals.
A general decision algorithm runs in \(m^\tau\operatorname{poly}(L)\) bit time. Its dependence on capacities is through their binary encodings, rather than through \(C\) itself. In the stated input, \(m=|T|=\tau\).
The proof below interprets the atomless populations in the usual distributional sense: interval populations are permissible representatives of the given support.
For an individual \(x\), define
\(A_x(s)=\sum_{z:\,r_{\theta(x)}(\theta(z))\leq r_{\theta(x)}(s)}w_{xz}\).
Thus an individual of type \(t\) rejects an additional partner of type \(s\) precisely when \(A_x(s)=c_t\).
All assertions about individuals below are made outside the null set allowed in the stability definition.
Lemma 1. In every stable realization, almost every individual is saturated.
Proof. Suppose a positive-mass set of individuals is unsaturated. Some type \(t\) then has a positive-mass set \(U\) of unsaturated individuals.
Choose \(x\in U\). Its portfolio is finite, so the set consisting of \(x\) and its full partners has mass zero. Consequently, there exists \(y\in U\) distinct from \(x\) with \(w_{xy}\neq1\).
Both individuals have total incident weight strictly below \(c_t\). Hence neither stability equality can hold for this pair, a contradiction. \(\square\)
For each type \(t\), let \(q_t\) be the largest rank of a partner type occurring with positive aggregate incidence mass among individuals of type \(t\). Saturation and \(\mu_t>0\) ensure that this is defined. There are finitely many partner types, so almost every type-\(t\) individual has all partner ranks at most \(q_t\).
Lemma 2. Every stable realization satisfies, for all \(t,s\in T\),
\[q_t\leq r_t(s)\quad\text{or}\quad q_s\leq r_s(t).\tag{1}\]
This includes \(t=s\), and therefore \(q_t\leq r_t(t)\).
Proof. If \(q_t>r_t(s)\), a positive aggregate incidence mass goes from type \(t\) to types strictly worse than \(s\). Since portfolios are finite and capacities are bounded by \(C\), a positive-mass set of type-\(t\) individuals therefore satisfies \(A_x(s)<c_t\).
If both inequalities in (1) fail, there are positive-mass sets of individuals of types \(t\) and \(s\) that fail their respective stability equalities. Choose one individual from the first set, and then choose an individual from the second set outside its finite set of full partners and outside itself. This gives a blocking pair.
The same argument applies when \(t=s\). \(\square\)
Conversely, if everyone is saturated, all type-\(t\) portfolios use ranks at most \(q_t\), and (1) holds, then the realization is stable. Indeed, for every pair of types, (1) supplies an endpoint whose entire capacity is assigned to partner types at least as good as the other endpoint's type.
Let
\(d_t=\mu_t c_t,\qquad y_{ts}=\int_{X_t}\sum_{z\in X_s}w_{xz}\,d\nu(x).\)
Here \(y_{tt}\) counts incidences at both endpoints of same-type edges. Mass-preserving pairings give \(y_{ts}=y_{st}\).
For a fixed cutoff vector \(q\in\{1,\ldots,m\}^{T}\) satisfying (1), consider the following rational linear feasibility problem:
\(y_{ts}\geq0,\qquad y_{ts}=y_{st},\)
\[\sum_{s\in T}y_{ts}=d_t\quad(t\in T),\tag{2}\]
\[y_{ts}=0\quad\text{if }r_t(s)>q_t\text{ or }r_s(t)>q_s,\tag{3}\]
\[\sum_{t,s\in T}r_t(s)y_{ts}\leq B.\tag{4}\]
Every stable realization of cost at most \(B\) yields a feasible solution for its cutoff vector, by Lemmas 1 and 2.
We next prove the converse, including the requirement that individual partners be distinct.
Lemma 3. Every feasible instance of (2)–(4) has a valid stable realization of cost at most \(B\), using only full edges.
Proof. A nonempty rational polyhedron contains a rational point. Choose a rational feasible matrix \(y\).
Choose a positive integer \(Q\) such that every \(Q\mu_t\) and \(Qy_{ts}\) is integral and every \(Qy_{tt}\) is even. For type \(t\), create \(Q\mu_t\) temporary vertices, each with \(c_t\) stubs.
By (2), the number of these stubs is
\(Q\mu_t c_t=\sum_s Qy_{ts}.\)
Label exactly \(Qy_{ts}\) type-\(t\) stubs with partner type \(s\). Pair the stubs between distinct types using symmetry, and pair the same-type stubs among themselves using their even counts. This produces a finite multigraph with the required degrees and type incidence counts. It may contain loops and parallel edges.
We remove those defects while preserving degrees and incidence proportions. Put \(k=2C+1\), and replace each temporary vertex \(v\) by copies \(v_a\), indexed by \(a\in\mathbb Z/k\mathbb Z\).
For distinct temporary vertices \(u,v\) joined by \(p\) parallel edges, fix an orientation of their unordered pair and replace their edges by
\(\{u_a,v_{a+j}\}\quad(a\in\mathbb Z/k\mathbb Z,\ 0\leq j<p).\)
Since \(p\leq C<k\), these edges are distinct.
If a temporary vertex \(v\) has \(\ell\) loops, replace them by
\(\{v_a,v_{a+j}\}\quad(a\in\mathbb Z/k\mathbb Z,\ 1\leq j\leq\ell).\)
Each former loop contributes degree two to every copy. Because \(2\ell\leq C\) and \(k=2C+1\), these edges contain neither loops nor repetitions: the shifts \(j\) are nonzero and distinct even up to sign.
The resulting graph is simple, and each copy of a type-\(t\) vertex has degree \(c_t\).
Replace every graph vertex by an interval of mass \(1/(Qk)\). For every graph edge, pair equal coordinates in its two intervals. These pairings are measurable and mass-preserving. Every individual has exactly \(c_t\) distinct full partners, and self-partnership is impossible.
The type masses are \(\mu_t\), and the aggregate incidence matrix is exactly \(y\). Condition (3) places every partner within the prescribed cutoff. Condition (1) consequently proves stability. The cost is the left-hand side of (4).
There are no half edges, so the half-cycle requirement is satisfied vacuously. \(\square\)
Thus the cutoff linear programs characterize the decision problem exactly.
Each program has \(O(\tau^2)\) variables and constraints, with rational encoding length polynomial in \(L\). Products \(\mu_t c_t\) have polynomial bit length even when \(C\) is large. Enumerating the cutoffs and solving the programs therefore takes
\(m^\tau\operatorname{poly}(L)\)
bit time.
Guessing a cutoff vector and checking its linear program is a nondeterministic polynomial-time algorithm. Equivalently, a feasible rational matrix of polynomial encoding length supplies a certificate. Hence the problem belongs to \(\mathrm{NP}\). The potentially large graph in Lemma 3 is an existence construction; it need not be written into the certificate.
The reverse direction of the hardness reduction requires more than lifting a finite instance: arbitrary population mixtures must also be controlled.
Consider \(n\) types corresponding to finite agents. Their rankings of other original types are the finite rankings, and each ranks its own type after all other original types.
Suppose \(p\) is a symmetric nonnegative matrix on these types satisfying
\[\sum_j p_{ij}=1.\tag{5}\]
For each \(i\), define its worst supported rank by
\(W_i=\max\{r_i(j):p_{ij}>0\}.\)
Assume that
\[W_i\leq r_i(j)\quad\text{or}\quad W_j\leq r_j(i)\qquad\text{for all }i,j.\tag{6}\]
Define its rank cost as \(H(p)=\sum_{i,j}r_i(j)p_{ij}\).
Lemma 4. Such a matrix can be replaced, without increasing \(H\), by a matrix whose components are isolated diagonal entries of value \(1\), full pairs, and simple half-cycles.
Proof. Form the undirected support graph, including a loop at \(i\) when \(p_{ii}>0\).
For a positive off-diagonal edge \(\{i,j\}\), the definition of \(W\) gives
\(r_i(j)\leq W_i,\qquad r_j(i)\leq W_j.\)
Together with (6), this implies equality at at least one endpoint. Assign the edge to an endpoint at which it is the worst supported partner. A positive loop is likewise the worst supported partner at its vertex, because own type is ranked last among original types.
Strict rankings imply that each vertex can receive at most one assigned edge. Thus every connected component has at most as many edges as vertices.
A vertex of graph degree one has exactly one off-diagonal entry. Equation (5) forces that entry to be \(1\), and symmetry and (5) force its neighbor to have no other positive entry. Such a component is an isolated full pair.
Every other component has minimum graph degree at least two, counting loops twice. Since its edge count is at most its vertex count, the degree-sum identity forces every vertex to have degree exactly two. Consequently, it is an isolated loop or a simple cycle.
An isolated loop has value \(1\). On a simple cycle, (5) forces successive edge weights to alternate between \(\alpha\) and \(1-\alpha\). On an odd cycle, this forces \(\alpha=\tfrac12\).
On an even cycle, the matrix is a convex combination of the two alternating perfect matchings. Choose the matching with smaller rank cost. Its cost is no greater than the convex combination's cost.
These replacements only remove supported partners. Thus every new worst rank is at most its old value, which preserves (6). This proves the lemma. \(\square\)
Interpret every isolated diagonal entry as an unmatched finite agent, and retain the full pairs and half-cycles.
The result is a finite stable half-matching. To check this carefully, give an unmatched agent worst rank \(n\), corresponding to its diagonal entry before deletion. For a distinct pair \(i,j\), (6) guarantees an endpoint that is matched entirely to agents at least as good as the other endpoint. That endpoint cannot be unmatched, since every distinct original type has rank strictly below \(n\).
If the decoded matching has \(h\) unmatched agents, then
\[H(p')=\operatorname{cost}(M)+nh.\tag{7}\]
Use the finite capacity-one egalitarian half-matching threshold problem from the question. Its decision version is \(\mathrm{NP}\)-hard; the corresponding stable-partition threshold hardness is stated explicitly in [Glitzner–Manlove, Theorem 4.16](https://arxiv.org/html/2406.00437v1#S4).
We also use two finite results: a stable half-matching can be computed in \(O(n^3)\) combinatorial time, and every agent receives the same total allocation in all stable half-matchings of the same instance. These are [Theorem 4.4 and Theorem 5.1](https://arxiv.org/html/2505.11456v3). Their hypotheses apply here: the finite instance has strict complete preferences and integral capacities equal to one.
Let the source instance have \(n\) agents and cost threshold \(K\). Compute any stable half-matching and let \(h\) be its number of unmatched agents. Allocation invariance shows that this same \(h\) occurs in every stable half-matching of the instance.
Put \(N=2^{\lceil\log_2 n\rceil}\). Construct a society with \(N\) types, each of mass \(1/N\) and capacity \(1\).
For each original agent \(i\), its type ranks:
Each of the \(N-n\) added types ranks its own type first, followed by the remaining types in any strict order.
Set
\[B=\dfrac{K+nh+(N-n)}{N}.\tag{8}\]
All masses are dyadic rationals.
Given a finite stable half-matching \(M\):
A same-type matching can be realized on its interval by the fixed-point-free involution that exchanges its two halves.
All portfolios are finite and have distinct partners. The half-edge components are disjoint finite simple cycles.
For distinct original types, finite stability supplies the required endpoint equality. A finite full pair also supplies that equality at both endpoints, since capacities are one. Replacing an unmatched agent by same-type partners changes none of its cumulative allocations through the rank of a distinct original type. Same-type pairs satisfy the equality because everyone is saturated and own type is no better than their assigned original partners. Added types reject every distinct type because their portfolios consist entirely of their first choice.
The realization is therefore stable. Its cost is
\(\dfrac{\operatorname{cost}(M)+nh+(N-n)}{N}.\)
Thus \(\operatorname{cost}(M)\leq K\) implies population cost at most \(B\).
Suppose the constructed society has a stable realization of cost at most \(B\).
By Lemmas 1 and 2, an added type has cutoff at most its own rank, namely \(1\). It therefore partners only with its own type and contributes exactly \(1/N\) to the cost.
An original type has cutoff at most its own rank \(n\), so it has no partners among added types.
Let \(y\) be the aggregate incidence matrix restricted to original types, and put \(p_{ij}=Ny_{ij}\). This is symmetric and has row sums one. Its worst supported ranks satisfy (6), by Lemma 2. Moreover,
\(\operatorname{cost}(\text{realization})=\dfrac{H(p)+(N-n)}{N}.\)
Apply Lemma 4 and decode the rounded matrix into a finite stable half-matching \(M\). Allocation invariance guarantees that \(M\) has exactly \(h\) unmatched agents. Hence (7) gives
\(\operatorname{cost}(M)+nh=H(p')\leq H(p).\)
Using the assumed cost bound and (8),
\(H(p)\leq NB-(N-n)=K+nh.\)
Therefore \(\operatorname{cost}(M)\leq K\). This proves the reverse implication.
The reduction uses \(N<2n\) types, has \(C=1\), and produces encoding length \(O(n^2\log n+\operatorname{bits}(K))\). Its finite preprocessing uses \(O(n^3)\) combinatorial operations; the entire reduction takes polynomial bit time.
For general inputs, the cutoff algorithm takes \(m^\tau\operatorname{poly}(L)\) bit time and requires no expansion proportional to \(C\). In particular, fixed support size gives polynomial time in the binary input length.
When support size varies, the reduction proves \(\mathrm{NP}\)-hardness already for \(C=1\). Combined with Section 2, this establishes \(\mathrm{NP}\)-completeness.
⟨structured verdict parsed — rendered above⟩
The argument is sound in substance and establishes the claimed NP-completeness under the stated interpretation of interval populations as representatives of the support. I found one minor citation issue, but no false central step or substantive mathematical gap.
1. Saturation and cutoff conditions
Lemma 1 correctly uses the strong, pairwise stability requirement after deletion of a null set. A positive-mass set of unsaturated individuals contains an individual outside any chosen individual’s finite set of full partners and outside that individual itself. For both endpoints, every cumulative allocation is strictly below capacity. Thus the selected pair violates stability.
This argument correctly includes pairs of distinct individuals of the same type. Atomlessness and finite portfolios are essential, and both are available.
The definition of \(q_t\) is valid: saturation and positive type mass imply positive aggregate incidence somewhere, and there are only finitely many partner types. Zero aggregate incidence to a partner type implies that almost every individual has no incidence to that type. Taking the finite union of the exceptional sets establishes the asserted almost-everywhere cutoff bound.
Lemma 2 is also correct. Positive aggregate incidence to partners worse than \(s\) produces a positive-mass set of individuals for whom \(A_x(s)<c_t\). If both cutoff inequalities fail, the two resulting sets contain a distinct pair outside the selected individual’s finite set of full partners. Neither endpoint satisfies its stability equality.
The same selection works when \(t=s\), so \(q_t\leq r_t(t)\) follows legitimately. There is no mistaken exemption for same-type partnerships.
The converse cutoff criterion is sufficient: saturation and the partner-rank upper bounds make the cumulative allocation equal to capacity at whichever endpoint the cutoff disjunction supplies. It applies to absent edges and half edges alike.
2. Aggregate linear programming formulation
The incidence convention is consistent. An off-diagonal entry records incidence mass from one type to another; symmetry follows from mass-preserving pairings. A diagonal entry records both endpoints of same-type edges. Accordingly, the row sums are \(\mu_t c_t\), and summing \(r_t(s)y_{ts}\) over ordered type pairs counts the cost at both endpoints exactly as required.
Conditions (2)–(4) are necessary. Condition (3) correctly requires an edge’s partner type to satisfy the cutoff at both endpoints.
Lemma 3 establishes sufficiency, subject to the cutoff condition (1) already imposed before its statement:
The removal of loops and parallel edges is correct. For parallel edges, \(p\leq C<k\) makes the shifts distinct modulo \(k\). For loops, \(2\ell\leq C\) ensures that the selected shifts are nonzero and distinct up to sign. Each former loop gives degree two at each copied vertex. Edges arising from different pairs of temporary vertices cannot coincide.
The interval construction then gives measurable, mass-preserving pairings, distinct individual partners, and no self-partnership. Copying preserves the incidence proportions: each original graph edge produces \(k\) edges, while each interval has mass \(1/(Qk)\). Consequently, the aggregate matrix remains \(y\).
The construction uses only full edges, so the half-cycle restriction is satisfied. The potentially enormous construction is used solely to prove existence, which is sufficient for the proposed certificate.
The explicit interval interpretation is consistent with the task’s support-only input model.
3. Running time and NP membership
There are \(m^\tau\) cutoff vectors. Each linear program has \(O(\tau^2)\) variables and constraints and polynomial coefficient bit length. Multiplying a binary-rational mass by a binary-encoded capacity increases bit length polynomially; it does not require expansion proportional to \(C\).
Thus the stated \(m^\tau\operatorname{poly}(L)\) bit-time bound follows from polynomial-time rational linear programming. In this input model, \(m=\tau\), as the prover correctly states.
Guessing a cutoff vector and then deterministically checking its linear program establishes NP membership. The alternative assertion about a polynomial-length rational certificate is also consistent with standard rational linear programming bounds. The graph need not be included in the certificate.
4. Rounding lemma
The support-graph argument is valid, including its treatment of loops.
For a positive off-diagonal edge, both incident ranks are bounded by their respective worst supported ranks. Condition (6) therefore forces equality at at least one endpoint. Strict rankings ensure that a vertex has only one worst supported partner type, so it can receive at most one assigned edge.
A positive loop is indeed worst at its vertex because own type is ranked last among the original types. Hence each connected component has at most as many edges as vertices.
A degree-one vertex has one positive off-diagonal entry and no loop. Its row sum forces that entry to equal one; the neighbor’s row sum then excludes every other positive entry. This component is an isolated full pair.
For every remaining component, minimum degree is at least two, counting a loop twice. The edge-count bound and degree-sum identity force degree exactly two throughout. The stated possibilities—an isolated loop or a simple cycle—follow.
The cycle equations give alternating weights. Odd cycles consequently have weight one half on every edge. On an even cycle, the weighted matrix is a convex combination of the two alternating perfect matchings, so selecting the cheaper matching cannot increase cost.
Removing supported entries cannot worsen any cutoff, so condition (6) is preserved. Decoding a diagonal entry as an unmatched finite agent also preserves the finite stability test: an unmatched agent’s artificial worst rank is \(n\), whereas every distinct original agent has rank below \(n\). Such an endpoint therefore cannot supply the cutoff inequality.
The identity \(H(p')=\operatorname{cost}(M)+nh\) correctly separates genuine assignment cost from the artificial diagonal contribution.
5. External results and their applicability
The allocation-invariance statement used in the reduction is accurately stated: Theorem 5.1 gives equality of each agent’s total allocation across stable half-matchings of the same Stable Fixtures instance. Its hypotheses apply to strict complete preferences and capacity one. The cited paper’s stability definition also matches the cumulative-allocation equality used here. [Glitzner–Manlove, definitions and Theorem 5.1](https://arxiv.org/html/2505.11456v3)
The source hardness claim is supported. Theorem 4.16 explicitly establishes NP-completeness of the stable-partition egalitarian threshold problem. Its cost definition averages predecessor and successor ranks and excludes self-assignment cost, consistently with the weighted finite cost used in this reduction. [Glitzner–Manlove, Definition 2.13 and Theorem 4.16](https://arxiv.org/html/2406.00437v1)
Minor issue — Section 4, algorithm citation. Theorem 4.4 is stated as an algorithm for computing a generalized stable partition, rather than directly as the asserted half-matching algorithm. The same paper supplies the correspondence in Theorem 4.1, and its algorithmic discussion supports the claimed running time. This is a citation precision issue, not a substantive obstruction. [Glitzner–Manlove, Theorems 4.1 and 4.4](https://arxiv.org/html/2505.11456v3)
Minimum clarification: explicitly cite the generalized-stable-partition-to-half-matching conversion alongside Theorem 4.4 and state that the conversion preserves the polynomial preprocessing bound.
6. Reduction and threshold accounting
The construction preserves strict complete rankings. Original types place their own type at rank \(n\), and added types place their own type first. Equal masses \(1/N\) are positive dyadic rationals and sum to one.
The forward realization satisfies all partnership restrictions. Full pairs and half-cycles lift by equal coordinates; same-type full matchings use a fixed-point-free involution. The prover explicitly handles the important distinction between a finite full pair and pairs of population individuals with the same two types: capacity one makes the necessary cumulative equality hold even when those individuals are not directly paired.
Original same-type pairs satisfy stability because all assigned partners have rank at most \(n\). Added types reject every other type through their first-choice allocation. The cost expression correctly includes \(nh\) for the unmatched original agents and \(N-n\) for the added types before division by \(N\).
In the reverse direction, Lemma 2 forces added types to partner only within their own type and excludes added partners for original types. Thus the original block has the asserted symmetric matrix with row sums one.
Lemma 4 produces a finite stable half-matching without increasing cost. Allocation invariance then justifies using precisely the precomputed number \(h\) of unmatched agents. Subtracting the same \(nh\) from the two sides of the cost inequality gives the source threshold condition correctly.
Finally, \(N<2n\) and the explicit ranking construction give the stated polynomial output length and polynomial bit-time reduction. The hardness restriction \(C=1\) and equal dyadic masses is established.
⟨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.