Answer: \(\mathrm{NP}\text{-complete}\) for every fixed rational \(0<\alpha<\tfrac12\)
Theorem 2 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateFor every 0<α< 1 2, CONSENSUS[α] is NP-hard.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite connected role graph \(H=(T,F)\), rational masses \(\mu_t>0\) with \(\sum_{t\in T}\mu_t=1\), and fixed rational \(0<\alpha<\frac12\), let \(x_t\in[0,\mu_t]\) denote opinion-\(1\) mass and define \(a_t(x)=\sum_{\{t,u\}\in F}x_u\) and \(b_t(x)=\sum_{\{t,u\}\in F}(\mu_u-x_u)\). A \(0\to1\) transfer at \(t\) is legal when \(\mu_t-x_t>0\) and \(a_t(x)>b_t(x)\), while a \(1\to0\) transfer is legal when \(x_t>0\) and \(b_t(x)>a_t(x)\). Decide whether there exists \(x^0\) with \(\sum_t x_t^0\le\alpha\) whose two-phase \(\max_1\) closure, exhausting legal \(0\to1\) transfers before legal \(1\to0\) transfers, reaches \(x_t=\mu_t\) for every \(t\).
Fix a rational \(0<\alpha<\tfrac12\). A society is given by its support: a list of \(\tau\) types with positive binary rational masses \(\mu_t\), summing to \(1\). Here \(\tau\) is the support size, not the number of possible types.
The input also specifies a finite connected simple undirected role graph \(H=(T,F)\) on these types. Write \(m=|F|\) and let \(L\) be the total input bit length; state running times in \(m,\tau,L\), with \(\alpha\) fixed.
A configuration has real opinion-\(1\) masses \(x_t\in[0,\mu_t]\). Define \(a_t(x)=\sum_{u:\{t,u\}\in F}x_u\) and \(b_t(x)=\sum_{u:\{t,u\}\in F}(\mu_u-x_u)\).
A transfer changes only one coordinate: it increases \(x_t\) by any \(0<\delta\le\mu_t-x_t\) when \(a_t(x)>b_t(x)\), or decreases it by any \(0<\delta\le x_t\) when \(b_t(x)>a_t(x)\). Ties permit neither move.
Define \(\max_1(x)\) by first repeatedly setting \(x_t=\mu_t\) whenever \(x_t<\mu_t\) and \(a_t(x)>b_t(x)\), until none is possible; then repeatedly set \(x_t=0\) whenever \(x_t>0\) and \(b_t(x)>a_t(x)\), until none is possible. In each phase choose the first eligible type in the support list.
The decision problem asks whether some \(x^0\) satisfies \(\sum_{t\in T}x_t^0\le\alpha\) and \(\max_1(x^0)_t=\mu_t\) for every \(t\in T\).
For each fixed rational \(0<\alpha<\tfrac12\), is this continuous consensus decision problem in \(\mathrm{P}\), or is it \(\mathrm{NP}\)-hard?
The discrete counterpart, with binary opinions and at most \(\lceil\alpha n\rceil\) initial supporters among \(n\) agents, is \(\mathrm{NP}\)-hard for every fixed rational \(0<\alpha<\tfrac12\). [Source](https://www.ijcai.org/proceedings/2018/0007.pdf)
No result settling this exact mass-based decision problem was located in the literature search.
For every fixed rational \(0<\alpha<\tfrac12\), the stated continuous consensus decision problem is \(\mathrm{NP}\)-complete.
The reduction below handles arbitrary real initial masses. Its central lemma converts every successful fractional configuration into a vertex cover, with each selected vertex charged to disjoint initial masses.
Write \(N(t)\) for the neighbors of type \(t\). An upward move at \(t\) is eligible exactly when
\(2\sum_{u\in N(t)}x_u>\sum_{u\in N(t)}\mu_u.\)
Each coordinate is completed at most once during the upward phase, so that phase terminates after at most \(\tau\) updates.
Order independence. Fix an initial configuration \(x^0\), and let \(z\) be the terminal configuration of any exhaustive upward schedule. Consider another legal upward sequence. We prove inductively that \(z\) dominates every configuration in that sequence coordinatewise.
Initially, \(z\ge x^0\). Suppose the other sequence next completes coordinate \(t\). If \(z_t=\mu_t\), domination persists. Otherwise, the strict eligibility inequality at the current configuration also holds at \(z\), because neighbor masses only increase. This contradicts termination of the schedule producing \(z\). Thus domination persists in either case.
Applying this argument in both directions to two exhaustive schedules shows that their terminal configurations coincide. The same argument shows monotonicity with respect to the initial configuration: increasing initial coordinates cannot prevent upward consensus.
The downward phase only decreases coordinates. Consequently, if the upward phase leaves any coordinate below its cap, the downward phase cannot produce all-\(1\) consensus. Conversely, the all-\(1\) configuration permits no downward move.
Therefore:
The specified process reaches all-\(1\) consensus if and only if some legal upward sequence completes every coordinate.
This permits us to use convenient activation orders in the proof, despite the prescribed support-list order.
Guess the set \(S\) of coordinates initially at their caps and an order \(v_1,\ldots,v_r\) for completing the remaining coordinates.
Introduce initial-mass variables \(y_t\) and a common slack \(\varepsilon\). Require
\(y_t=\mu_t\quad(t\in S),\qquad 0\le y_t\le\mu_t-\varepsilon\quad(t\notin S),\)
\(\sum_t y_t\le\alpha,\qquad 0\le\varepsilon\le1.\)
Immediately before completing \(v_i\), its neighbors have masses
\(z_u^{(i)}=\mu_u\) if \(u\in S\cup\{v_1,\ldots,v_{i-1}\}\), and \(z_u^{(i)}=y_u\) otherwise.
For each \(i\), require
\(2\sum_{u\in N(v_i)}z_u^{(i)}-\sum_{u\in N(v_i)}\mu_u\ge\varepsilon.\)
A successful real configuration gives a feasible solution with \(\varepsilon>0\): take the minimum of its finitely many positive activation margins and positive initial cap gaps, decreasing it to at most \(1\).
Conversely, a feasible solution with \(\varepsilon>0\) certifies a legal successful sequence. By Section 1, it also certifies success under the prescribed order.
This is a bounded rational linear program with \(\tau+1\) variables, \(O(\tau)\) constraints, and \(O(m+\tau)\) nonzero coefficients. If its optimum slack is positive, an optimal vertex has polynomial binary encoding length. Indeed, clearing rational denominators produces integer data of polynomial bit length, and Cramer’s rule together with the determinant bound gives polynomial bit length for every vertex coordinate.
Thus every YES instance has a rational certificate of polynomial size. Checking it takes \(O(m+\tau)\) exact rational arithmetic operations by maintaining neighbor sums along the guessed sequence, and hence \(\operatorname{poly}(m,\tau,L)\) bit operations.
We reduce from Vertex Cover. Let \(G=(V,E)\) be a simple graph without isolated vertices, with
\(n=|V|,\qquad q=|E|,\qquad 0\le k\le n.\)
The question is whether \(G\) has a vertex cover of size at most \(k\). These restrictions preserve its standard \(\mathrm{NP}\)-completeness: isolated vertices can be deleted, and instances outside the indicated budget range are immediately decidable.
We first use unnormalized positive weights. Normalization will occur after padding.
Set
\(p=\dfrac1{100(n+1)}.\)
For each vertex \(v\), of degree \(d_v\), create types \(A_v,B_v\), with weights
\(w(A_v)=2,\qquad w(B_v)=d_v+2p.\)
For each edge \(e=\{u,v\}\), create a type \(E_e\) of weight \(1\). Create one additional type \(P\), of weight \(p\).
The core edges are:
For these weights, the upward eligibility inequalities are:
\(B_v:\quad x_{A_v}>1,\)
\(A_v:\quad x_{B_v}+\sum_{e\ni v}x_{E_e}>d_v+p,\)
\(E_{\{u,v\}}:\quad x_{A_u}+x_{A_v}+x_P>2+\dfrac p2.\)
Suppose \(C\subseteq V\) is a vertex cover, with \(|C|\le k\). Initialize
\(x_{A_v}=1+p\) for \(v\in C\), and \(x_{A_v}=0\) otherwise;
\(x_{B_v}=2p\) for every \(v\);
\(x_{E_e}=0\) for every \(e\), and \(x_P=p\).
All coordinates respect their caps.
For every \(v\in C\), first complete \(B_v\), since \(x_{A_v}=1+p>1\). Then complete \(A_v\), since its neighbor \(B_v\) contributes \(d_v+2p>d_v+p\).
Every edge has an endpoint in \(C\). Consequently every \(E_e\) becomes eligible: a completed endpoint contributes \(2\), and \(P\) contributes \(p\), giving
\(2+p>2+\dfrac p2.\)
After all edge types are completed, every remaining \(A_v\) is eligible because
\(x_{B_v}+\sum_{e\ni v}x_{E_e}=2p+d_v>d_v+p.\)
Completing those types then makes their \(B_v\) neighbors eligible.
The initial core cost, including \(P\), is at most
\(k(1+p)+2np+p.\)
The following lemma supplies soundness.
Lemma. Consider any initial masses on the core types. If the core reaches upward consensus when \(P\) is initially full, then \(G\) has a vertex cover \(C\) satisfying
\(\left(1-\dfrac p4\right)|C|\le \sum_{v\in V}(x_{A_v}+x_{B_v})+\sum_{e\in E}x_{E_e}.\)
Proof. Put
\(c=1-\dfrac p4.\)
Begin a set \(C\) by including:
Charge the vertices added in the first step to their \(A_v\) coordinates. Each such coordinate costs at least \(c\).
Charge new vertices from the second step to their \(B_v\) coordinates. Since \(d_v\ge1\), each costs at least \(1\).
Finally, charge new vertices from the third step to initially full edge coordinates. Each costs \(1\), and each edge can add at most one new vertex. These initial charges use distinct coordinates. Therefore their total is at least \(c\) times the number of initially selected vertices.
Now run a successful upward schedule that always completes every eligible edge type before completing another \(A\)- or \(B\)-type. Such a schedule succeeds by order independence.
Suppose \(A_v\) is about to be completed and \(v\notin C\). Then
\(x_{A_v}<c<1,\)
and \(B_v\) was not initially full. Moreover, \(B_v\) cannot have been completed earlier: before the first completion of \(A_v\), its eligibility condition \(x_{A_v}>1\) is false. Thus \(B_v\) still has its initial mass.
Let \(R_v\) be the set of incident edge types not yet full, and put \(r_v=|R_v|\). Every edge type in \(R_v\) still has its initial mass; all other incident edge types contribute \(1\). The eligibility inequality for \(A_v\) consequently gives
\(x_{B_v}+(d_v-r_v)+\sum_{e\in R_v}x_{E_e}>d_v+p,\)
and hence
\(x_{B_v}+\sum_{e\in R_v}x_{E_e}>r_v+p.\)
If \(r_v\ge1\), add \(v\) to \(C\) and charge it to the initial coordinates \(B_v\) and \(E_e\) for \(e\in R_v\). Their combined cost exceeds \(1\), so it exceeds \(c\).
These charges are disjoint:
In particular, an edge coordinate can occur in at most one charged set \(R_v\). The initial and subsequent charges together prove
\(c|C|\le\sum_v(x_{A_v}+x_{B_v})+\sum_e x_{E_e}.\)
It remains to prove that \(C\) covers every edge.
Suppose, for contradiction, that \(e=\{u,v\}\) has neither endpoint in the final \(C\). It was not initially full, since otherwise an endpoint would have been selected. Also,
\(x_{A_u}<c,\qquad x_{A_v}<c.\)
Before either endpoint type is completed, the neighbor sum at \(E_e\) is strictly less than
\(2c+p=2+\dfrac p2.\)
Thus \(E_e\) cannot be completed before the first completion of \(A_u\) or \(A_v\).
At that first endpoint completion, \(E_e\) therefore belongs to the corresponding set \(R_u\) or \(R_v\). That set is nonempty, so the endpoint is added to \(C\), a contradiction. Hence \(C\) is a vertex cover. \(\square\)
For a successful configuration in a larger graph whose core has no additional neighbors except at \(P\), the lemma still applies. In the soundness analysis, we may increase \(P\) to its cap for free. This only helps activation, and we use neither its initial cost nor any padding cost in the lemma.
The core weight, including \(P\), is
\(W_0=2n+3q+2np+p,\)
because \(\sum_v d_v=2q\).
Choose an integer \(h\ge2\), depending only on the fixed \(\alpha\), such that
\(\dfrac{h-1}{2h}>\alpha.\)
Define the positive constant
\(\gamma=\dfrac{h-1}{2}-\alpha h>0,\)
and set
\(R=1+\dfrac{\alpha W_0+n+1}{\gamma},\qquad M=\dfrac{k+\tfrac14+n+1+\gamma}{\alpha}.\)
Both weights are positive, and \(R>1\).
Add a clique on types \(Q_1,\ldots,Q_h\), each of weight \(R\). Join only \(Q_1\) to \(P\). Also add one type \(D\), of weight \(M\), whose only neighbor is \(P\).
Let
\(B=\dfrac{(h-1)R}{2}\)
and let \(W=W_0+hR+M\) be the total unnormalized weight. The definitions give the exact identity
\(\alpha W=B+k+\dfrac14.\)
Indeed,
\(\alpha M=k+\dfrac14+n+1+\gamma\)
and
\(\gamma R=\gamma+\alpha W_0+n+1,\)
so
\(\alpha W =\alpha W_0+\alpha hR+\alpha M =k+\dfrac14+(\alpha h+\gamma)R =k+\dfrac14+B.\)
Let \(s\) be the total initial mass on the clique.
If no clique coordinate is completed during the upward phase, successful consensus requires all clique coordinates to have been initially full, so \(s=hR>B-\tfrac p2\).
Otherwise, examine the first upward completion in the clique. At that moment all other clique coordinates still have their initial masses.
If the completed type is \(Q_i\) with \(i\ne1\), eligibility requires
\(s-x_{Q_i}>B,\)
and hence \(s>B\).
If it is \(Q_1\), eligibility requires
\(s-x_{Q_1}+x_P>B+\dfrac p2.\)
Since \(x_P\le p\) and \(x_{Q_1}\ge0\), this implies
\(s>B-\dfrac p2.\)
This lower bound is valid regardless of what happens elsewhere in the graph.
Initialize \(Q_1\) with mass \(0\), and every other clique type with mass
\(\dfrac R2+\dfrac p{h-1}.\)
These values are below \(R\), because \(R>1\) and \(p<\tfrac1{100}\). Their total is \(B+p\).
With \(P\) full, \(Q_1\) has neighbor sum \(B+2p\), exceeding its threshold \(B+\tfrac p2\). Complete \(Q_1\).
Every other clique type now has neighbor sum at least
\(R+(h-2)\left(\dfrac R2+\dfrac p{h-1}\right)>B,\)
so all can be completed.
Finally, initialize \(D\) with mass \(0\). It completes whenever \(P\) is full, because its sole neighbor has positive opinion-\(1\) mass.
Set \(\mu_t=w(t)/W\) for every constructed type. Multiplying every configuration coordinate by \(W\) preserves all strict eligibility comparisons. The normalized budget \(\alpha\) is therefore equivalent to the unnormalized budget
\(B+k+\dfrac14.\)
If \(G\) has a vertex cover of size at most \(k\), use the core initialization from Section 3, the clique initialization from Section 5, and \(x_D=0\).
The total initial mass is at most
\(B+k+p(k+2n+2).\)
Since \(k\le n\),
\(p(k+2n+2)\le\dfrac{3n+2}{100(n+1)}<\dfrac3{100}<\dfrac14.\)
Thus the initialization satisfies the budget. The explicitly described upward sequences complete every type, so Section 1 guarantees consensus under the prescribed support-list order.
Suppose the constructed instance has a successful real initial configuration satisfying the budget. Let
\(C_{\mathrm{core}}=\sum_v(x_{A_v}+x_{B_v})+\sum_e x_{E_e}\)
be its initial mass on the core coordinates other than \(P\).
The clique lower bound, and nonnegativity of all remaining initial masses, imply
\(C_{\mathrm{core}}<k+\dfrac14+\dfrac p2.\)
Increase \(P\) to its cap in the soundness analysis. The successful original core sequence remains legal, because \(P\) is the core’s only connection to the padding. The charging lemma consequently yields a vertex cover \(C\) with
\(|C|< \dfrac{k+\tfrac14+\tfrac p2}{1-\tfrac p4}.\)
The right-hand side is less than \(k+1\). To verify this, it suffices to check
\(\dfrac14+\dfrac{p(k+3)}4<1.\)
Using \(k\le n\) and the definition of \(p\),
\(\dfrac{p(k+3)}4\le\dfrac{n+3}{400(n+1)}\le\dfrac3{400}.\)
Hence \(|C|<k+1\). Since its size is integral, \(|C|\le k\).
This proves soundness for arbitrary real initial masses.
The constructed role graph is finite, simple, undirected, and connected. Each original vertex has an incident edge, so its \(A_v\)- and \(B_v\)-types connect through an edge type to \(P\). The clique and \(D\) also connect to \(P\).
All masses are positive rational numbers and, after normalization, sum exactly to \(1\).
For fixed \(\alpha\), the chosen \(h\) is constant. The construction has
\(\tau=2n+q+h+2\)
types and
\(m=n+3q+\binom h2+2\)
role edges. Each normalized mass has \(O(\log(n+q))\) bits, with constants depending on \(\alpha\). Thus the output has total bit length
\(L=O((n+q)\log(n+q)).\)
The reduction takes polynomial time in the source input length. For the target problem, certificate verification takes \(\operatorname{poly}(m,\tau,L)\) bit operations, as established in Section 2. An explicit exact deterministic upper bound is
\(2^\tau\tau!\,\operatorname{poly}(m,\tau,L),\)
obtained by enumerating initial-full sets and activation orders and solving the corresponding slack linear programs.
The reduction and membership proof together establish \(\mathrm{NP}\)-completeness for every fixed rational \(0<\alpha<\tfrac12\).
⟨structured verdict parsed — rendered above⟩
Assessment: proved. The output establishes \(\mathrm{NP}\)-completeness for every fixed rational \(0<\alpha<\tfrac12\). The fractional charging argument is valid, the padding preserves soundness for arbitrary real initial masses, and the membership argument supplies polynomial-size rational certificates. I found no major or minor mathematical issues.
The eligibility condition
\[
2\sum_{u\in N(t)}x_u>\sum_{u\in N(t)}\mu_u
\]
correctly rewrites \(a_t(x)>b_t(x)\).
Each upward update puts one previously incomplete coordinate at its cap. Since upward updates never decrease coordinates, each coordinate is updated at most once. Thus every exhaustive upward schedule terminates after at most \(\tau\) updates.
The order-independence proof is sound. Its induction compares another legal sequence against a terminal configuration \(z\). If a coordinate eligible in the other sequence remains incomplete in \(z\), coordinatewise domination makes the same strict inequality hold at \(z\), contradicting termination. Applying this in both directions proves equality of terminal configurations.
The stated monotonicity also follows from this comparison: a terminal configuration obtained from a larger initialization dominates the smaller initialization, so the same induction applies to its legal upward sequence.
The equivalence with the specified two-phase process is correct:
These conclusions also handle a connected graph with a single vertex: its isolated coordinate cannot move, and the budget prevents it from starting full.
The guessed set \(S\) and order of its complement correctly describe initially full coordinates and subsequent completions.
The common slack variable enforces both necessary strict conditions:
For any successful real initialization, finitely many positive cap gaps and activation margins admit a common positive lower bound. Consequently, the proposed linear program has a feasible point with \(\varepsilon>0\). Conversely, such a feasible point makes every completion legal.
The polyhedron is bounded: all initial masses lie in their prescribed finite intervals, and \(0\le\varepsilon\le1\). Its coefficients are rational. A positive optimum therefore has an optimal vertex, and the denominator-clearing and determinant argument gives polynomial encoding length for its coordinates. This justifies a polynomial-size rational certificate despite allowing arbitrary real initial configurations.
The constraint and sparsity counts are correct. Each activation constraint uses only the relevant initial neighbor variables; completed neighbors contribute constants. Across all activation constraints there are at most \(2m\) such neighbor occurrences. The remaining constraints contribute \(O(\tau)\) nonzero coefficients.
Maintaining neighbor sums requires \(O(m+\tau)\) rational arithmetic operations. The certificate lengths and intermediate rational lengths remain polynomially bounded, so the claimed \(\operatorname{poly}(m,\tau,L)\) bit complexity follows.
The three displayed thresholds correctly account for all neighbors:
The initialization associated with a vertex cover respects all caps. In particular, \(1+p<2\), and \(2p\le d_v+2p\).
Each claimed activation is valid:
The initial core cost is correctly bounded by
\[
k(1+p)+2np+p.
\]
This is the central soundness argument, and it is valid.
The initial charges use distinct coordinates:
Overlaps between selection rules do not cause double charging because subsequent rules charge only newly selected vertices.
If \(A_v\) is about to complete and \(v\notin C\), its initial mass is below \(c<1\). It has not previously changed, and \(B_v\) cannot previously have completed: its only enabling condition is \(x_{A_v}>1\). Also, \(B_v\) was not initially full.
The activation inequality therefore correctly implies
\[
x_{B_v}+\sum_{e\in R_v}x_{E_e}>r_v+p.
\]
When \(r_v\ge1\), the charged mass exceeds \(1\), and hence exceeds \(c\).
The disjointness argument checks out. A charged \(B_v\) is unique to its vertex and was not initially charged. Every charged edge is initially incomplete. Once \(A_v\) completes, full \(P\) makes each edge in \(R_v\) strictly eligible. Edge priority completes these edges before another \(A\)-type completion can charge them again.
Thus the claimed bound
\[
c|C|\le\sum_v(x_{A_v}+x_{B_v})+\sum_e x_{E_e}
\]
is justified.
An edge with neither endpoint in the final \(C\) is initially incomplete, and both endpoint initial masses are strictly below \(c\). Before either endpoint completes, its neighbor sum is strictly below
\[
2c+p=2+\frac p2.
\]
Therefore the edge cannot complete first. At the first endpoint completion, it remains in that endpoint’s nonempty \(R_v\), which forces selection of the endpoint. This contradicts the assumed uncovered edge.
The extension to the padded graph is also valid. Only \(P\) has additional neighbors. Setting \(P\) full and retaining the original relative order of core completions preserves every core activation inequality.
The core weight
\[
W_0=2n+3q+2np+p
\]
is correct.
The required constant \(h\) exists because \(\tfrac{h-1}{2h}\) approaches \(\tfrac12\) from below. Its choice makes \(\gamma>0\), and the specified \(R\) and \(M\) are positive rational numbers.
Rechecking the algebra gives the exact identity
\[
\alpha W=B+k+\frac14.
\]
The clique lower bound is valid even if some clique coordinates start full. At its first actual completion, every other clique coordinate retains its initial mass. The two cases yield respectively \(s>B\) and \(s>B-\tfrac p2\). If there is no completion, successful consensus requires every clique coordinate to start full, which also satisfies the bound.
The proposed clique initialization respects its caps and costs \(B+p\). With full \(P\), the activation margin at \(Q_1\) is positive. After \(Q_1\) completes, each remaining clique type exceeds threshold: the displayed neighbor sum exceeds \(B\) by at least \(R/2\). This includes \(h=2\).
The activation of \(D\) is valid because its sole neighbor \(P\) is full.
Scaling weights and coordinates by the same positive factor preserves caps and strict eligibility comparisons. The normalized budget therefore corresponds exactly to \(B+k+\tfrac14\).
The YES-direction total cost is correctly computed as
\[
B+k+p(k+2n+2).
\]
Using \(k\le n\), the stated bound makes its excess over \(B+k\) strictly less than \(\tfrac14\).
In the NO direction, subtracting the strict clique lower bound from the total budget gives
\[
C_{\mathrm{core}}<k+\frac14+\frac p2.
\]
Discarding nonnegative costs on \(P\) and \(D\) is legitimate.
Applying the charging lemma yields the claimed strict bound on \(|C|\). The calculation comparing it with \(k+1\) is correct: the required condition is precisely
\[
\frac14+\frac{p(k+3)}4<1.
\]
The supplied estimate establishes this with ample slack. Integrality then gives \(|C|\le k\).
Thus arbitrary fractional initializations cannot defeat the reduction.
The construction satisfies connectedness, simplicity, undirectedness, positivity, and normalization. Deleting isolated vertices from Vertex Cover is legitimate, with budgets beyond the remaining vertex count handled as immediate YES cases.
The counts
\[
\tau=2n+q+h+2,\qquad
m=n+3q+\binom h2+2
\]
are correct.
For fixed \(\alpha\), all rational weights and normalized masses have logarithmic encoding length in the source graph size. The stated asymptotic output-size bound is valid, with constant-size source cases absorbed conventionally.
Enumerating initial-full sets and orders gives at most \(2^\tau\tau!\) candidate linear programs. Polynomial-time rational linear programming applies to the explicitly bounded rational programs described above, so the deterministic upper bound is justified.
No additional clarification or repair is needed.
⟨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.