← back to the atlas

d4-conf-ecai-2020-0218 (d4-conf-ecai-2020-0218)

Answer: —

The anchor (named result in the paper)

Theorem 3 — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximateFor customers with majority behaviour, computing an SPMS evolution that is also optimal is NP-hard even on classes of networks that are augmented quasi-paths or augmented cycles.

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

The continuous mirror question, as graded

Given a finite connected role graph \(H=(R,E)\) in the paper’s augmented quasi-path or augmented-cycle classes, rational role masses \(\mu_r>0\) summing to \(1\), and initial product masses \(x^0_{r,p}\), determine whether a finite schedule of rational mass updates can end at a stable state whose white mass equals the supremum over all feasible schedules; if so, return such an SPMS schedule. Each member of role \(r\) sees the product masses in the adjacent roles and follows the paper’s majority rule and tie-breaking, while white recommendations have priority whenever eligible mass exists.

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

A society is given by its support: the list of the \(\tau\) role types with positive mass, each mass a binary rational; \(\tau\) is the support size, not the number of possible types. There are \(m=3\) products \(P=\{\mathrm{black},\mathrm{gray},\mathrm{white}\}\).
The input is a finite simple connected undirected role graph \(H=(R,E)\), with \(\tau=|R|\), rational masses \(\mu_r>0\) satisfying \(\sum_r\mu_r=1\), and rational initial allocations \(x^0_{r,p}\geq0\) satisfying \(\sum_p x^0_{r,p}=\mu_r\). The graph is an augmented quasi-path if acyclic, or an augmented cycle if it contains a cycle: in either class, every vertex of degree \(3\) or at least \(5\) has at most one neighbor whose degree exceeds \(1\).
At state \(x\), members of role \(r\) see scores \(s_{r,p}(x)=\sum_{u:\{r,u\}\in E}x_{u,p}\). A member currently holding \(p\) keeps it if \(p\) maximizes these scores; otherwise she chooses white if white is a maximizer, and otherwise chooses either maximizing nonwhite product. Both choices are allowed when black and gray tie.
A legal update selects one role \(r\), one current product \(p\), a different product \(q\) prescribed by this rule, and a rational amount \(0<\delta\leq x_{r,p}\); it transfers \(\delta\) from \(x_{r,p}\) to \(x_{r,q}\), leaving everything else fixed. Initial white holders may subsequently leave white; no further seeding occurs.
A state is stable if no positive mass can legally change product. A feasible schedule is a finite sequence of legal updates from \(x^0\) ending in a stable state, including the empty sequence when already stable. An SPMS schedule must update to white whenever any positive mass anywhere is eligible to change to white; otherwise any legal update is allowed.
Let \(W(x)=\sum_r x_{r,\mathrm{white}}\) and let \(M\) be the supremum of terminal white mass over all feasible schedules, without the SPMS restriction. The problem asks whether an SPMS schedule ends with \(W(x)=M\), and requests such a schedule when one exists; if no feasible schedule exists, the answer is no. Schedules are explicit lists of updates with binary rational amounts. Let \(L\) be the total input bit length; state running times in \(m,\tau,L\).

Is deciding whether an SPMS schedule attains \(M\) in \(\mathrm{P}\), or is it \(\mathrm{NP}\)-hard? Can an attaining schedule also be returned in polynomial time on yes-instances?

For discrete agents on these graph classes, an optimal SPMS evolution always exists, but computing one is \(\mathrm{NP}\)-hard. [Source](https://ebooks.iospress.nl/pdf/doi/10.3233/FAIA200071)
No result settling the exact rational-mass problem above was located in the literature search.

Modeling choices made when packaging the task

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

1. Status

The general complexity question remains unresolved. I prove two additional results:

Thus the discrete existence theorem does not extend to the exact rational-mass model.

2. Two preliminary facts

Write $w=\mathrm{white}$, $b=\mathrm{black}$, and $g=\mathrm{gray}$. At any role, a legal transfer must move from a product whose score is strictly below the maximum to a maximizing product, with white taking priority among possible destinations.

2.1. A finite feasible SPMS schedule always exists

Define
$$ \Phi(x)=\sum_{\{r,u\}\in E}\sum_{p\in P}x_{r,p}x_{u,p}. $$

A transfer of amount $\delta$ at role $r$, from $p$ to $q$, changes the potential by
$$ \Phi(x')-\Phi(x) =\delta\bigl(s_{r,q}(x)-s_{r,p}(x)\bigr)>0. $$

Indeed, the graph has no loops, so the scores at $r$ remain unchanged during its update. The strict inequality follows from legality.

Let $D$ be the product of the denominators appearing in the input masses and allocations. Then $\log_2 D=O(L)$. Use the following rule: whenever a white update is available, select one; otherwise select any legal update. Transfer the entire allocation of the selected source product.

All coordinates remain integer multiples of $1/D$. Consequently, every update increases $\Phi$ by at least $1/D^2$. Moreover,
$$ 0\leq\Phi(x) \leq\sum_{\{r,u\}\in E}\mu_r\mu_u \leq\frac{1-\sum_r\mu_r^2}{2} <\frac12. $$

The procedure therefore terminates after fewer than $D^2/2$ updates. It stops only at a stable state and respects SPMS throughout.

This gives a construction in
$$ 2^{O(L)}\operatorname{poly}(m,\tau,L) $$
time. It proves feasibility, not optimality.

If $\tau=1$, all scores are zero and the initial state is stable. The empty schedule attains $M=W(x^0)$.

2.2. The one-third obstruction

Suppose $\tau\geq2$ and
$$ x_{r,w}\leq\frac{\mu_r}{3} \qquad\text{for every }r. $$

These inequalities prevent any transfer to white. To prove this, put
$$ C_r=\sum_{u:\{r,u\}\in E}\mu_u. $$
Then
$$ s_{r,w}\leq C_r/3, \qquad s_{r,b}+s_{r,g}+s_{r,w}=C_r. $$

If a transfer to white were legal, white would maximize the scores, while the source score would be strictly smaller. Hence
$$ C_r<3s_{r,w}\leq C_r, $$
a contradiction. Every other update preserves or decreases the white coordinate of the updated role, so the inequalities are invariant.

There is also a useful restriction on stable states satisfying these inequalities. If such a state has $x_{r,w}>0$, stability requires white to maximize the scores at $r$. Therefore
$$ s_{r,b}=s_{r,g}=s_{r,w}=C_r/3. $$
Equality in
$$ \sum_{u:\{r,u\}\in E}x_{u,w} \leq\sum_{u:\{r,u\}\in E}\mu_u/3 $$
forces every neighbor $u$ of $r$ to satisfy $x_{u,w}=\mu_u/3>0$. Repeating this argument along paths shows that every role has positive white allocation and all three scores are equal at every role. Since every vertex has a neighbor, it also gives $x_{u,w}=\mu_u/3$ for every $u$.

No nonempty legal schedule can end at a state with all three scores equal everywhere. The scores at the last updated role are unchanged by that last update; they would already have been equal immediately before it, making the update illegal.

It follows that, under the one-third inequalities:

3. A no-instance on a four-vertex path

Consider the path
$$ A\!-\!B\!-\!C\!-\!D. $$

Every role has mass $1/4$. In the order $(b,g,w)$, let the initial allocations be:

| Role | Initial allocation |
|---|---|
| $A$ | $(0,0,4)/16$ |
| $B$ | $(2,2,0)/16$ |
| $C$ | $(0,4,0)/16$ |
| $D$ | $(3,1,0)/16$ |

All allocations are dyadic rationals. The graph is an augmented quasi-path because all its degrees are at most two.

3.1. The unrestricted optimum is attained and equals one

Here is a legal schedule. Amounts in the last column are in units of $1/16$.

| Update | Role | Transfer | Amount |
|---|---|---|---|
| 1 | $C$ | $g\to b$ | $1$ |
| 2 | $B$ | $b\to w$ | $2$ |
| 3 | $B$ | $g\to w$ | $2$ |
| 4 | $C$ | $b\to w$ | $1$ |
| 5 | $C$ | $g\to w$ | $3$ |
| 6 | $D$ | $b\to w$ | $3$ |
| 7 | $D$ | $g\to w$ | $1$ |

We verify legality explicitly.

Initially, the scores at $C$, in units of $1/16$, are
$$ (2,2,0)+(3,1,0)=(5,3,0). $$
Thus its first transfer from gray to black is legal.

After that transfer, $C$ has allocation $(1,3,0)/16$. The scores at $B$ are consequently
$$ (0,0,4)+(1,3,0)=(1,3,4). $$
White is the unique maximizer, so updates 2 and 3 are legal and make $B$ entirely white.

The scores at $C$ are now
$$ (0,0,4)+(3,1,0)=(3,1,4). $$
White again uniquely maximizes, so updates 4 and 5 make $C$ entirely white. White then uniquely maximizes the scores at $D$, making updates 6 and 7 legal.

Role $A$ was already entirely white. The resulting state is white consensus and is stable. Since total mass is one,
$$ M=1. $$

3.2. Every feasible SPMS schedule has terminal white mass three eighths

Initially, the only possible transfers to white are from black at $B$: its scores are $(0,4,4)/16$, so gray holders keep gray and black holders must choose white.

Let $t/16$ be the cumulative amount transferred from black to white at $B$. As long as $0\leq t<2$, SPMS forces another white update, and the state must be
$$ x_A=(0,0,4)/16,\qquad x_B=(2-t,2,t)/16, $$
$$ x_C=(0,4,0)/16,\qquad x_D=(3,1,0)/16. $$

To justify that assertion inductively, the scores at $C$ are
$$ (5-t,3,t)/16. $$
For $t<2$,
$$ 5-t>3>t, $$
so white is not a maximizer there. White is also not a maximizer at $D$, whose only neighbor is entirely gray. Role $A$ holds only white and therefore cannot receive a white transfer. At $B$, its remaining black allocation is still eligible to change to white.

Thus, before any nonwhite update is permitted, the entire black allocation of $B$ must be transferred to white. A finite schedule ending in a stable state cannot stop earlier.

At that point,
$$ x_B=(0,2,2)/16. $$
Roles $A$ and $B$ are stable. The scores at $C$ are
$$ (3,3,2)/16, $$
so its gray holders also keep their product. The only legal updates are transfers from black to gray at $D$.

If their cumulative amount is $u/16$, where $0\leq u\leq3$, then
$$ x_D=(3-u,1+u,0)/16, $$
and the scores at $C$ become
$$ (3-u,3+u,2)/16. $$
Gray remains a maximizer throughout, so $C$ never changes. The other two roles remain stable. Terminal stability requires all remaining black at $D$ to move to gray.

Consequently, every feasible SPMS schedule terminates at
$$ x_A=(0,0,4)/16,\qquad x_B=(0,2,2)/16, $$
$$ x_C=(0,4,0)/16,\qquad x_D=(0,4,0)/16. $$
Its white mass is
$$ W=\frac{4+2}{16}=\frac38<1=M. $$

For example, transferring $2/16$ from black to white at $B$, followed by $3/16$ from black to gray at $D$, is a feasible SPMS schedule.

Therefore this is a no-instance. Its failure is not caused by nonattainment of the unrestricted supremum: $M$ is attained by the explicit seven-update schedule above.

4. Complete solution for two roles

Theorem. For $m=3$ and $\tau=2$, every instance has an SPMS schedule attaining $M$. Such a schedule uses at most five updates and can be constructed in $O(L^3)$ bit operations. In particular, the decision and construction problems are polynomial-time solvable on $\tau\leq2$.

Let the two roles be $A,B$, joined by one edge. Their allocation vectors are denoted by $a,b$, with respective total masses $\mu_A,\mu_B$. Define
$$ \operatorname{Max}(a)=\{p:a_p=\max_{q\in P}a_q\}, \qquad \operatorname{Supp}(a)=\{p:a_p>0\}. $$

The scores at $A$ are exactly $b$, and the scores at $B$ are exactly $a$.

4.1. Classification of stable states

Stability is equivalent to
$$ \operatorname{Supp}(a)\subseteq\operatorname{Max}(b), \qquad \operatorname{Supp}(b)\subseteq\operatorname{Max}(a). $$
Because both masses are positive, maximizing coordinates are positive. Hence
$$ \operatorname{Supp}(a) \subseteq\operatorname{Max}(b) \subseteq\operatorname{Supp}(b) \subseteq\operatorname{Max}(a) \subseteq\operatorname{Supp}(a). $$
All these sets are therefore equal to a nonempty set $S\subseteq P$.

Both roles distribute their masses uniformly over $S$:
$$ a_p= \begin{cases} \mu_A/|S|,&p\in S,\\ 0,&p\notin S, \end{cases} \qquad b_p= \begin{cases} \mu_B/|S|,&p\in S,\\ 0,&p\notin S. \end{cases} $$
Conversely, every state of this form is stable.

Thus there are exactly seven stable states. Their white masses belong to
$$ \left\{0,\frac13,\frac12,1\right\}. $$

If the input is already stable, no first update is legal, and the empty schedule is optimal. Assume henceforth that it is unstable.

4.2. A common nonwhite maximum blocks positive terminal white

We first prove a lemma needed in the case analysis.

Lemma. Suppose a nonwhite product $c$ maximizes both allocation vectors, and
$$ a_c>a_w,\qquad b_c>b_w. $$
Then every reachable stable state has zero white mass.

Proof. Consider any legal schedule. Until $c$ first ceases to maximize one of the allocation vectors, its allocations cannot decrease: a holder of $c$ sees $c$ maximizing at the other role. White cannot receive transfers either, because the other role's $c$ allocation is strictly larger than its white allocation. Consequently, throughout this interval, both strict inequalities persist.

If $c$ remains a maximizer of both allocation vectors for the whole schedule, white is strictly below a maximizing score at each role. Terminal stability then forces both white allocations to be zero.

Otherwise, consider the first update after which $c$ no longer maximizes an allocation vector, say that of role $A$. The destination must be the other nonwhite product $d$. A destination of white is impossible, and a destination of $c$ cannot destroy its maximality. The $c$ allocation at $A$ cannot decrease, so after the update,
$$ a'_d>a'_c>a'_w. $$
Therefore
$$ a'_w<\mu_A/3. $$

For the transfer to $d$ to be legal, $d$ must maximize the allocation vector of $B$. Before this first loss of maximality, $c$ also maximizes that vector. Hence
$$ b_d=b_c>b_w, $$
which gives
$$ b_w<\mu_B/3. $$

Both roles now have strictly less than one-third white. Section 2.2 shows that these strict bounds persist and exclude any stable state with positive white. This proves the lemma. $\square$

4.3. Case analysis and constructions

The following cases exhaust all initial allocation vectors.

Case 1: White uniquely maximizes an allocation vector

Suppose white uniquely maximizes $a$. Transfer each positive nonwhite allocation at $B$ entirely to white. These transfers are legal because the scores at $B$ remain $a$.

Role $B$ is then entirely white. Transfer each positive nonwhite allocation at $A$ entirely to white.

This is an SPMS schedule with at most four updates, ending at white consensus. Thus $M=1$.

Case 2: White ties with exactly one nonwhite maximum

Suppose
$$ \operatorname{Max}(a)=\{w,c\}, $$
and let $d$ be the remaining nonwhite product. Thus
$$ a_w=a_c>a_d. $$

A positive allocation of $d$ at $B$ can legally be transferred entirely to white. After that transfer,
$$ b_d=0,\qquad b_w=\mu_B-b_c. $$

There are three subcases.

If $b_c<\mu_B/2$, this makes white the unique maximum at $B$. Case 1 then yields white consensus. Counting only the remaining positive source allocations, the complete schedule uses at most four updates.

If $b_c=\mu_B/2$, role $B$ becomes balanced between $c$ and white.

If $a_d>0$, transfer it to white. This is legal because its score is zero at $B$, whereas white has score $\mu_B/2$. White now uniquely maximizes $a$, so white consensus follows. The complete schedule again uses at most four updates.

If $a_d=0$, role $A$ was already balanced between $c$ and white. The constructed terminal state has white mass $1/2$ and is optimal. Indeed, initially,
$$ a_c=\mu_A/2,\qquad b_c=\mu_B/2. $$
The property that both $c$ allocations are at least half their role masses is invariant. Under that property, $c$ maximizes both allocation vectors and its holders cannot leave. Therefore every reachable state satisfies
$$ W\leq(\mu_A-a_c)+(\mu_B-b_c)\leq\frac12. $$

If $b_c>\mu_B/2$, every reachable terminal state has zero white. To prove this, observe that the following properties are invariant:
$$ b_c>\mu_B/2, \qquad c\in\operatorname{Max}(a). $$
At $A$, the unique maximizing score is $c$, so every update there increases $a_c$ and decreases another coordinate. At $B$, a holder of $c$ cannot leave because $c$ maximizes $a$. These observations prove the invariance by induction.

Terminal stability therefore forces $A$ entirely to $c$, since $c$ uniquely maximizes $b$. It then forces $B$ entirely to $c$.

An SPMS schedule with at most four updates is explicit: first transfer $b_d$ to white if positive; then transfer $a_w$ to $c$, followed by the remaining positive non-$c$ allocations to $c$. After the first transfer, no white update remains available; after the second, $c$ uniquely maximizes both allocation vectors. Thus the schedule respects SPMS and attains $M=0$.

Case 3: A role is uniform over all three products

This case remains only if Cases 1 and 2 do not apply. Suppose
$$ a_b=a_g=a_w=\mu_A/3. $$
The other role cannot have white as a maximizer: it would fall under Cases 1 or 2, or both roles would be uniform and already stable.

Initially, no update at $B$ is legal because all its scores are equal. Every legal first update is therefore at $A$ and has a maximizing nonwhite destination $c$ of $b$. Any positive such transfer makes $c$ the unique maximum of the allocation vector at $A$. At $B$, $c$ was already a maximum and strictly exceeded white.

The lemma in Section 4.2 now applies. Every reachable terminal state has zero white.

A short attaining SPMS schedule transfers $a_w$ to any such $c$, then all non-$c$ allocations at $B$ to $c$, and finally the remaining non-$c$ allocation at $A$ to $c$. It uses at most four updates. Throughout this construction, white is strictly below a maximizing score at both roles, so no white update is available.

Case 4: White maximizes neither vector, and there is a common nonwhite maximum

Choose
$$ c\in\operatorname{Max}(a)\cap\operatorname{Max}(b). $$
Both strict inequalities required by Section 4.2 hold, so $M=0$.

If some role has positive white, transfer its entire white allocation to $c$. This makes $c$ uniquely maximize that role's allocation vector. Transfer all non-$c$ allocations at the other role to $c$, and then the first role's remaining non-$c$ allocation to $c$. This uses at most four updates.

If both white allocations are zero, instability implies that $c$ uniquely maximizes at least one vector; otherwise both roles would be balanced between black and gray and stable. Transfer the other role's non-$c$ allocation to $c$, and then do the same at the first role. At most two updates suffice.

All these transfers preserve a common maximum $c$ strictly above white, so SPMS permits them.

Case 5: White maximizes neither vector, and the maximum sets are disjoint

The maximum sets must be opposite singletons. Relabeling the nonwhite products if necessary, suppose
$$ \operatorname{Max}(a)=\{b\}, \qquad \operatorname{Max}(b)=\{g\}. $$

If both white allocations are at most one-third of their role masses, Section 2.2 gives $M=0$.

A short attaining schedule drains each positive white allocation to a currently maximizing nonwhite product. These drains are legal: initially white is not maximizing at either role, and draining white at one role can only worsen white relative to nonwhite scores at the other. No white update is available by Section 2.2.

After at most two drains, only two products remain. If the resulting state is unstable, choose a legal update and transfer its entire source allocation. The updated role becomes monochromatic; the other role can then transfer its allocation of the other color to that color. Thus at most two additional updates produce a stable state.

Finally, suppose one role has more than one-third white. Choose that role as $A$, and relabel the opposite maxima as above. Then
$$ a_w>\mu_A/3. $$
Transfer
$$ \delta=\frac{a_b-a_g}{2} $$
from black to gray at $A$. This amount is positive and no larger than $a_b$. The transfer is legal because gray uniquely maximizes the scores at $A$.

After it,
$$ a'_b=a'_g=\frac{\mu_A-a_w}{2}<a_w. $$
White now uniquely maximizes the allocation vector at $A$, so Case 1 produces white consensus.

The initial transfer respects SPMS because white initially maximizes neither allocation vector; every subsequent transfer is to white. The schedule uses at most five updates and attains $M=1$.

4.4. Exhaustiveness and complexity

If white maximizes an allocation vector, its maximizing set is either a singleton, a two-element set, or all three products. Cases 1–3 cover these possibilities. Otherwise, the two nonempty maximum sets are subsets of $\{b,g\}$; they either intersect or are opposite singletons, giving Cases 4–5.

Every construction uses at most five updates. The case tests and update amounts require only a constant number of rational comparisons, additions, subtractions, and divisions by two. All resulting numbers have $O(L)$ bits. Exact arithmetic therefore gives the conservative bound $O(L^3)$ for $m=3,\tau=2$, or $O(m\tau^2L^3)$ on the stated subclass $\tau\leq2$.

This proves the theorem.

5. Consequences and remaining questions

The four-role counterexample establishes that the rational-mass decision problem has actual no-instances even on paths. It also shows why the discrete existence theorem cannot be imported directly: discrete agents and divisible role allocations have different attainable evolutions. The cited paper proves existence of an optimal SPMS evolution in its discrete model, and hardness of computing one. [Auletta, Ferraioli, and Greco, Theorems 2–3](https://ebooks.iospress.nl/pdf/doi/10.3233/FAIA200071)

The two-role theorem gives a complete polynomial-time solution for the smallest nontrivial connected graph, including arbitrary rational partial transfers. Neither result supplies a general polynomial-time algorithm or a hardness reduction for the requested decision problem.

⟨structured verdict parsed — rendered above⟩

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

Verification report

Overall assessment: correct partial progress; the requested general complexity classification remains unresolved.

The preliminary results, the four-role counterexample, and the polynomial-time construction for at most two roles are sound as written. I found no false mathematical step or substantive gap in those results. The output explicitly acknowledges that it does not resolve the main task.

The two major issues below are missing task deliverables, rather than defects in the partial proofs.

1. Preliminary facts

1.1. Finite feasible SPMS schedules

The potential calculation is correct:
$$ \Phi(x')-\Phi(x) =\delta\bigl(s_{r,q}(x)-s_{r,p}(x)\bigr). $$

Only terms incident to the updated role change. Because the graph is loopless, the scores at that role do not change during its own update. A legal source has score strictly below the maximizing destination’s score, so the potential increases strictly.

The denominator argument also checks out. With the specified full-source transfers, all allocations remain multiples of $1/D$. Both the positive transfer amount and the positive score difference are therefore at least $1/D$, giving a potential increase of at least $1/D^2$.

The potential bound is valid:
$$ \sum_{\{r,u\}\in E}\sum_p x_{r,p}x_{u,p} \leq \sum_{\{r,u\}\in E}\mu_r\mu_u \leq \frac{1-\sum_r\mu_r^2}{2} <\frac12. $$

Consequently, the procedure terminates after fewer than $D^2/2$ updates. Its stopping condition is stability, and its selection rule satisfies SPMS. Since $\log_2 D=O(L)$ and each update can be represented and selected using polynomial work, the stated exponential-time bound follows.

This establishes existence of a finite feasible SPMS schedule for every input. It does not establish existence of an optimal SPMS schedule or attainment of $M$.

For $\tau=1$, all scores vanish, every held product maximizes, and no legal update exists. The empty schedule is correctly identified as optimal.

1.2. The one-third obstruction

The argument excluding transfers to white is correct. If white maximizes and a source score is strictly smaller, all three scores are at most the white score and at least one is strictly smaller. Thus
$$ C_r<3s_{r,w}, $$
contradicting $s_{r,w}\leq C_r/3$.

Every permitted update consequently preserves or decreases white allocation, so the inequalities are invariant.

The characterization of stable states with positive white also follows:

The last-update argument is valid: a terminal state with equal scores everywhere cannot result from a nonempty legal schedule, because the scores at the last updated role were already equal immediately before that update.

Therefore, for an unstable initial state satisfying the bounds, every feasible terminal state has zero white. Existence from Section 2.1 justifies the conclusion $M=0$.

2. Four-role path counterexample

2.1. Input validity

The graph is simple, connected, and acyclic, with maximum degree two, so it satisfies the required graph restriction. Each allocation row sums to $4/16=1/4$, and all entries are nonnegative dyadic rationals.

2.2. Unrestricted schedule

All seven updates are legal.

Successive updates at the same role leave that role’s scores unchanged. Every transfer amount is positive and no larger than the available source allocation.

The terminal state is stable white consensus. Since total mass is one, this proves that $M=1$ and that the supremum is attained in this example.

2.3. All feasible SPMS schedules

The asserted forced evolution is correct.

Initially, only black mass at $B$ can legally move to white. For cumulative transferred amount $t/16$ with $t<2$, the scores at $C$ satisfy
$$ 5-t>3>t. $$
Thus no white transfer becomes available at $C$. None is available at $D$, while $A$ has no nonwhite source mass. The remaining black mass at $B$ continues to be eligible for white.

Although partial transfers are allowed, a finite feasible schedule cannot terminate before exhausting that black mass: otherwise a legal white update remains available.

At $t=2$, roles $A$, $B$, and $C$ are stable. The only legal updates are black-to-gray transfers at $D$. Throughout these transfers, the scores at $C$ are
$$ (3-u,3+u,2)/16, \qquad 0\leq u\leq3, $$
so its held gray product continues to maximize.

Terminal stability forces $u=3$. The resulting white mass is exactly $3/8$. The supplied two-update schedule confirms feasibility.

The example is therefore a valid no-instance, even though the unrestricted optimum is attained.

3. Two-role theorem

3.1. Stable-state classification

The support conditions correctly express stability. Positive role masses ensure that every maximizing coordinate is positive, validating the chain
$$ \operatorname{Supp}(a) \subseteq\operatorname{Max}(b) \subseteq\operatorname{Supp}(b) \subseteq\operatorname{Max}(a) \subseteq\operatorname{Supp}(a). $$

All four sets must coincide. Each vector is therefore uniform on the same nonempty product set. Conversely, such states are stable.

There are exactly seven possible nonempty product sets, and the listed possible terminal white masses are correct. An initially stable state permits no first update, so the empty schedule is optimal.

3.2. Common nonwhite maximum lemma

The lemma is sound.

While $c$ maximizes both vectors, neither role can lose $c$ mass. White cannot receive transfers because the other role’s $c$ coordinate strictly exceeds its white coordinate. Hence both strict inequalities persist.

At the first loss of maximality, the updated vector must acquire a strictly larger coordinate for the other nonwhite product $d$. Consequently,
$$ a'_d>a'_c>a'_w, $$
which implies $a'_w<\mu_A/3$.

Legality requires $d$ to maximize the unchanged vector at $B$. Since $c$ also maximizes that vector,
$$ b_d=b_c>b_w, $$
and hence $b_w<\mu_B/3$.

The one-third obstruction applies from that point onward. Its stable-state characterization excludes positive terminal white. If no loss of maximality occurs, terminal stability directly excludes white. Both branches are covered.

3.3. Case analysis

| Case | Verification |
|---|---|
| White uniquely maximizes one vector | All transfers are legal transfers to white. Once the other role is entirely white, the remaining transfers are legal. White consensus establishes optimality. |
| White ties with one nonwhite maximum | The third-product transfer to white is legal whenever its source is positive. Each comparison with $\mu_B/2$ gives the asserted subsequent behavior. |
| One role is uniform | The other role has white strictly below a maximum. Any legal first transfer makes its destination the unique maximum of the initially uniform vector, so the lemma applies. |
| Neither vector has white as a maximum, with a common nonwhite maximum | The lemma applies. The proposed full-source transfers legally produce nonwhite consensus without introducing a white-update obligation. |
| Neither vector has white as a maximum, with disjoint maximum sets | The maximum sets are opposite nonwhite singletons. Both the one-third branch and the larger-white branch are valid. |

The following critical points also check out:

$$ \delta=\frac{a_b-a_g}{2}>0, \qquad \delta\leq a_b, $$
and gray is the unique permitted destination. Afterwards,
$$ a'_b=a'_g=\frac{\mu_A-a_w}{2}<a_w. $$
The initial transfer satisfies SPMS because initially neither vector has white as a maximum. All subsequent transfers are to white.

The cases are exhaustive, including ties and zero source allocations. The stated update bounds hold, with at most five updates in the final branch.

3.4. Complexity

For fixed $m=3$ and $\tau=2$, the constructions require only constantly many rational operations and comparisons. Their operands and outputs have $O(L)$ bits. The conservative $O(L^3)$ bound is justified.

Together with the singleton argument, this proves polynomial-time decision and construction on $\tau\leq2$. It does not provide a polynomial-time bound for unbounded support size.

4. External comparison

The cited discrete statements are accurately summarized: Theorem 2 asserts existence of an optimal SPMS evolution on the specified graph classes, and Theorem 3 asserts hardness of computing one. The paper’s majority behavior includes retaining a maximizing held product and prioritizing white among other tied destinations. [Auletta, Ferraioli, and Greco](https://ebooks.iospress.nl/pdf/doi/10.3233/FAIA200071)

The prover correctly does not apply these theorems to divisible rational allocations. The verified path example supports its conclusion that the discrete existence guarantee does not extend to the present model.

5. Issues and actionable feedback

Issue 1 — Major: general decision complexity remains unsettled

Where: Sections 1 and 5; final open points.

The output gives neither a polynomial-time decision algorithm for the full graph classes nor an $\mathrm{NP}$-hardness reduction. A no-instance and a polynomial-time solution for bounded support do not classify the general problem.

Minimum additional deliverable: Supply and justify a general polynomial-time algorithm with its bound in $m,\tau,L$, or a hardness reduction for the exact decision predicate in USER_TASK. The existing partial results require no repair.

Issue 2 — Major: general polynomial-time schedule construction remains unsettled

Where: Sections 2.1, 4.4, and 5.

The universal construction produces a feasible schedule in exponential time, with no optimality guarantee. The polynomial-time optimal construction applies only to $\tau\leq2$. Neither establishes the requested construction guarantee on general yes-instances.

Minimum additional deliverable: Resolve whether an attaining SPMS schedule can be returned in polynomial time on general yes-instances, accounting for the encoded length of the explicit update list and its rational amounts.

No additional mathematical clarification is needed to verify the partial results already presented.

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