← back to the atlas

Iterative voting and acyclic games (d4-journals-ai-2017-0031)

Answer: —

The anchor (named result in the paper)

Theorem 7 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximate$f^{PL}_{\hatv s}$ is FDRP. Moreover, any path of direct replies will converge after at most $m^2 n^2$ steps. In particular, Plurality is order-free acyclic.

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

The continuous mirror question, as graded

Given candidates \(C\), a rational ranking-type distribution \(\mu\in\mathbb{Q}^{\pi(C)}\), per-capita fixed scores \(\hat{\rho}\in\mathbb{Q}_{\ge 0}^{C}\), and an initial report state \(x=(x_{t,a})\) with \(x_{t,a}\ge 0\) and \(\sum_{a\in C}x_{t,a}=\mu_t\), decide whether every legal sequence of positive-mass cohort direct replies terminates at a state with no legal move. Moving all mass \(x_{t,a}>0\) from report \(a\) to \(b\) is legal exactly when \(b\) is the post-move lexicographic winner and \(b\succ_t f(x)\); if termination is guaranteed, compute a terminal state and a worst-case move bound.

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

Let \(C\) be a nonempty candidate set, \(m=|C|\), with a fixed input priority order for breaking score ties. A society is given by its support \(T\): the list of its \(\tau\) strict ranking types with positive binary-rational masses \(\mu_t\), normalized by \(\sum_{t\in T}\mu_t=1\). Here \(\tau=|T|\) is the support size, not the number of possible rankings.
The input also contains fixed scores \(\hat\rho\in\mathbb Q_{\ge0}^{C}\) and an arbitrary binary-rational initial state \(x^0\), where \(x^0_{t,a}\ge0\) and \(\sum_{a\in C}x^0_{t,a}=\mu_t\). Let \(L\) be the total input bit length.
At state \(x\), plurality scores are \(s_x(c)=\hat\rho(c)+\sum_{t\in T}x_{t,c}\); \(f(x)\) is the highest-scoring candidate, with exact ties resolved by the priority order.
A move selects \(t\in T\) and distinct \(a,b\in C\) with \(\delta=x_{t,a}>0\), sets \(x'_{t,a}=0\) and \(x'_{t,b}=x_{t,b}+\delta\), and leaves every other entry unchanged. It is legal exactly when \(f(x')=b\) and \(b\succ_t f(x)\). Cohorts merge on arrival; subsequent moves transfer the entire current entry.
Sequences are maximal: a scheduler chooses any legal move whenever one exists, without a fairness requirement. A terminal state has no legal move.

Is deciding whether every maximal legal sequence from \(x^0\) terminates in \(\mathrm P\), or is it \(\mathrm{NP}\)-hard?
On instances with guaranteed termination, can a reachable terminal state and a worst-case move bound be computed in polynomial time? State running times and move bounds in \(m,\tau,L\).

For finite societies of \(n\) unit-weight voters, all direct-reply sequences terminate within \(m^2n^2\) moves; unequal voter weights can permit direct-reply cycles. [Meir et al.](https://arxiv.org/pdf/1606.05837)
A nonatomic plurality model has convergence under local-dominance moves with uncertainty and negligible individual influence, which differs from the cohort legality above. [Meir](https://arxiv.org/pdf/1411.4949) No result settling this exact cohort problem was located.

Modeling choices made when packaging the task

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

Partial results for cohort direct-reply dynamics

The general complexity classification remains unresolved. The results proved below advance the finite-state analysis in two ways:

I also give a self-contained polynomial-space upper bound, an exponential algorithm with explicit graph lookup costs, and a convergence proof for two initially unsplit cohorts.

1. Definitions and finite-state representation

A legal sequence is universally terminating from $x^0$ if every maximal legal sequence starting there is finite.

For each type $t$, define
$$ k_t=\bigl|\{a\in C:x^0_{t,a}>0\}\bigr|, \qquad K=\sum_{t\in T}k_t. $$
Positive type masses imply
$$ \tau\le K\le m\tau. $$

Label each positive initial entry as an atom, retaining its initial mass and type. Every reachable entry is the sum of the atoms of its type currently located at that candidate. A move transfers all those atoms together. Thus atoms can merge but cannot split.

An assignment of these $K$ labeled atoms to candidates determines a numerical state. Consequently, the number of reachable numerical states is at most
$$ N=m^K. $$

Let $D$ be the product of the denominators appearing in the input masses, initial entries, and fixed scores. Its binary length is $O(L)$. After scaling by $D$, every reachable entry and score is an integer with $O(L)$ bits: entries are sums of initial entries and are at most one before scaling, while
$$ \hat\rho(c)\le s_x(c)\le\hat\rho(c)+1. $$
Thus all winner and legality tests admit exact arithmetic with polynomial bit complexity.

For running-time statements, write
$$ H=L+K\log_2(m+1). $$
In particular,
$$ H\le L+m\tau\log_2(m+1). $$

2. A three-candidate cycle from a truthful state

Weighted direct replies can cycle, as discussed in [Meir et al., Example 7](https://arxiv.org/pdf/1606.05837). The following construction establishes this with just three candidates and independently verifies every move.

Take $C=\{a,b,c\}$ and the following five distinct supported rankings:

| Type | Mass | Ranking |
|---|---:|---|
| $1$ | $23/64$ | $a\succ_1 c\succ_1 b$ |
| $2$ | $2/64$ | $b\succ_2 a\succ_2 c$ |
| $3$ | $12/64$ | $b\succ_3 c\succ_3 a$ |
| $4$ | $7/64$ | $c\succ_4 a\succ_4 b$ |
| $5$ | $20/64$ | $c\succ_5 b\succ_5 a$ |

The masses are positive dyadic rationals and sum to one. Set
$$ \hat\rho=\frac{1}{64}(1,14,0). $$
Initially, each type places its entire mass at its first-ranked candidate. Thus the initial position tuple is
$$ (a,b,b,c,c). $$

In the table, positions record the candidates supported by types $1,\ldots,5$, and scores are multiplied by $64$.

| Positions | Scaled scores $(a,b,c)$ | Winner | Next move |
|---|---:|---|---|
| $(a,b,b,c,c)$ | $(24,28,27)$ | $b$ | Type $4$: $c\to a$ |
| $(a,b,b,a,c)$ | $(31,28,20)$ | $a$ | Type $3$: $b\to c$ |
| $(a,b,c,a,c)$ | $(31,16,32)$ | $c$ | Type $2$: $b\to a$ |
| $(a,a,c,a,c)$ | $(33,14,32)$ | $a$ | Type $5$: $c\to b$ |
| $(a,a,c,a,b)$ | $(33,34,12)$ | $b$ | Type $1$: $a\to c$ |
| $(c,a,c,a,b)$ | $(10,34,35)$ | $c$ | Type $3$: $c\to b$ |
| $(c,a,b,a,b)$ | $(10,46,23)$ | $b$ | Type $5$: $b\to c$ |
| $(c,a,b,a,c)$ | $(10,26,43)$ | $c$ | Type $1$: $c\to a$ |
| $(a,a,b,a,c)$ | $(33,26,20)$ | $a$ | Type $4$: $a\to c$ |
| $(a,a,b,c,c)$ | $(26,26,27)$ | $c$ | Type $2$: $a\to b$ |
| $(a,b,b,c,c)$ | $(24,28,27)$ | $b$ | Repeat |

Every destination is the unique resulting winner. The ten required preference improvements, in order, are
$$ a\succ_4 b,\quad c\succ_3 a,\quad a\succ_2 c,\quad b\succ_5 a,\quad c\succ_1 b, $$
$$ b\succ_3 c,\quad c\succ_5 b,\quad a\succ_1 c,\quad c\succ_4 a,\quad b\succ_2 c. $$
Each transfer moves an entire positive entry. Each type always has exactly one cohort, so no merging occurs.

The last state equals the first state. Repeating the ten moves therefore gives an infinite legal sequence. It is an admissible maximal sequence because no fairness condition restricts the scheduler.

A terminal state is also reachable

From the same truthful initial state, instead move type $1$ from $a$ to $c$. This gives positions
$$ (c,b,b,c,c) $$
and scaled scores
$$ (1,28,50). $$
The move is legal because $c$ becomes the unique winner and $c\succ_1 b$.

This state is terminal:

Thus even with three candidates and a truthful initial state, existence of a reachable terminal state does not imply universal termination.

Three is the minimum candidate count permitting a cycle

For $m=1$, no move exists.

For $m=2$, every legal destination must be the moving type’s preferred candidate, and the source must be its less-preferred candidate. After the transfer, the less-preferred entry is zero. It can never receive another legal transfer, because the less-preferred candidate cannot be an improving destination.

Hence each type moves at most once, and every sequence has at most $\tau$ moves. Together with the construction above, this proves that the minimum candidate count permitting a cycle is exactly three.

3. A sharper move bound under universal termination

Define the falling factorial
$$ (m)_r=m(m-1)\cdots(m-r+1). $$

Let $p(x)$ be the number of positive entries. A move into an empty entry preserves $p(x)$; a move into a positive entry decreases it by exactly one. Every type retains positive total mass, so any sequence has at most
$$ h=K-\tau $$
merging moves.

Between consecutive merging moves, the partition of initial atoms into current cohorts remains fixed. If type $t$ has $r_t$ cohorts during such a phase, those cohorts occupy distinct candidates. There are therefore at most
$$ P(r)=\prod_{t\in T}(m)_{r_t} $$
possible labeled cohort placements during that phase.

On a universally terminating instance, a numerical state cannot repeat along a legal sequence: the intervening closed walk could otherwise be repeated forever. A phase consequently has at most $P(r)-1$ nonmerging moves.

If a sequence has $q$ merges and phase cohort-count vectors
$$ r^{(0)},r^{(1)},\ldots,r^{(q)}, $$
its total number of moves is at most
$$ \sum_{i=0}^{q}\bigl(P(r^{(i)})-1\bigr)+q = \sum_{i=0}^{q}P(r^{(i)})-1. $$

An explicit polynomial-time computable bound

Set
$$ P_0=\prod_{t\in T}(m)_{k_t}. $$
Form the multiset
$$ \mathcal D= \biguplus_{t\in T} \{m-k_t+1,m-k_t+2,\ldots,m-1\}. $$
It has $h=K-\tau$ elements. List them in nondecreasing order:
$$ d_1\le d_2\le\cdots\le d_h. $$
Define
$$ P_i=\frac{P_0}{d_1d_2\cdots d_i} \quad (1\le i\le h), \qquad B=\sum_{i=0}^{h}P_i-1. $$

These quantities are integers. Indeed, reducing a type’s cohort count from $r$ to $r-1$ divides its placement count by
$$ \frac{(m)_r}{(m)_{r-1}}=m-r+1. $$
For each type, these divisors occur in increasing order. Sorting all divisors therefore permits an order respecting each type’s required merge order.

After any $i$ actual merges, the placement count equals $P_0$ divided by a product of $i$ elements of $\mathcal D$. That product is at least $d_1\cdots d_i$. Thus its placement count is at most $P_i$. The preceding phase bound proves that every legal sequence on a universally terminating instance has at most
$$ U=\min\{m^K-1,B\} $$
moves. In particular,
$$ U\le \min\left\{ m^K-1,\; (K-\tau+1)\prod_{t\in T}(m)_{k_t}-1 \right\}. $$

All intermediate integers have $O(K\log(m+1))$ bits. Using elementary integer arithmetic, sorting and computing $U$ takes
$$ O\!\left(L+K^3\log^2(m+1)\right) $$
bit operations.

This is a polynomial-time computation of a valid upper bound. Neither its magnitude nor a terminal-state construction is thereby shown to be polynomially bounded.

4. General decision and construction algorithms

Universal termination is equivalent to absence of a reachable cycle

If a directed cycle of numerical states is reachable, a scheduler can reach it and repeat it indefinitely.

Conversely, an infinite legal sequence visits infinitely many states in a graph with at most $N=m^K$ vertices. Some state repeats, producing a nonempty directed closed walk and hence a directed cycle.

A finite maximal sequence ends at a terminal state by definition. Therefore universal termination is exactly the absence of a reachable directed cycle.

Polynomial-space upper bound

Nondeterministically attempt to execute exactly $N$ legal moves, rejecting a branch when it cannot continue.

A successful branch visits $N+1$ states and thus repeats a state. Conversely, a reachable cycle supplies a legal sequence of $N$ moves.

The algorithm stores the current numerical state, exact arithmetic workspace, and a counter with
$$ O(K\log(m+1)) $$
bits. This is polynomial space, and every branch halts.

Savitch’s theorem gives
$$ \mathrm{NPSPACE}=\mathrm{PSPACE}. $$
Deterministic polynomial space is closed under complement. Hence
$$ \boxed{\text{Universal termination belongs to }\mathrm{PSPACE}.} $$
This does not establish membership in $\mathrm P$ or hardness.

Exact exponential algorithm, including graph lookup

Use labeled atom assignments as vertices. An edge transfers all atoms of one type at a selected source to a selected destination, provided the corresponding numerical move is legal.

Every numerical legal trajectory lifts from the initial assignment by tracking its atoms. Conversely, every labeled path projects to a numerical legal trajectory. Consequently, an infinite numerical trajectory exists exactly when the reachable labeled graph contains a cycle: either trajectory is infinite in a finite corresponding graph.

There are at most $N$ vertices and at most $\tau m(m-1)$ outgoing edges per vertex.

Encode an assignment by its $K$ candidate indices. Store visited assignments in a binary trie. Each encoding has $O(K\log(m+1))$ bits, so insertion and lookup take that many bit operations; no linear scan through visited vertices is needed.

Exact arithmetic, successor construction, trie lookup, and graph analysis give the conservative bound
$$ O\!\left(H^3+m^K\tau m^2H^2\right). $$
Within this time one can:

Direct simulation under the termination promise

For a proposed transfer, only the source and destination scores change. The three highest current score-priority keys suffice to identify the highest unaffected competitor after excluding those two candidates. When fewer than three candidates exist, retain all candidates.

Scanning all possible moves therefore costs $O(\tau m^2H)$ bit operations per state. Under universal termination, simulation reaches a terminal state within
$$ O\!\left(H^3+(U+1)\tau m^2H\right) $$
bit operations.

This remains an exponential-time construction in general.

Because supported rankings are distinct, $\tau\le m!$. The exhaustive algorithm therefore has running time $g(m)L^{O(1)}$ for a computable function $g$. In particular, for every fixed $m$, all three exhaustive tasks above are polynomial-time solvable in $L$.

5. Two initially unsplit cohorts always terminate

Suppose $\tau=2$ and each type initially has exactly one positive entry. Each type thereafter retains exactly one cohort.

Assume, for contradiction, that a reachable nonempty closed walk exists. Choose one with the fewest moves.

Two cyclically consecutive moves cannot belong to the same type. Indeed, suppose that type moves its cohort from $a$ to $b$ and then from $b$ to $c$. If $c=a$, the numerical state returns to its state before these two moves, contradicting the two strict winner improvements. Otherwise, transferring directly from $a$ to $c$ produces the same final state. Its resulting winner is $c$, and transitivity makes it preferable to the original winner. This legal shortcut contradicts minimality.

Thus the two types alternate around the closed walk.

After any move, the moving type supports the current winner. If both cohorts coincide at some state, the next move separates them. Once separated, alternating moves cannot reunite them: the next mover would have to move to the other cohort’s candidate, which is the current winner and cannot be an improving destination. A closed walk therefore cannot contain a coincident state.

At every state of the closed walk, the next mover consequently supports a candidate different from the current winner. Its move leaves the current winner’s score unchanged. Since a different candidate becomes winner, the winning score-priority key strictly increases.

Strict increase around a closed walk is impossible. This contradiction proves universal termination.

There are at most $m^2$ states, so every sequence has at most
$$ m^2-1 $$
moves. Direct simulation constructs a terminal state in
$$ O(H^3+m^4H) $$
bit operations.

For completeness, if $\tau=1$ with arbitrary initial splitting, every move strictly improves the winner in the sole supported ranking. Thus every sequence has at most $m-1$ moves, and simulation takes $O(H^3+m^3H)$ bit operations.

6. What remains open

The three-candidate construction rules out extending unconditional convergence from two to three candidates, even for truthful initial states and unique winners.

The general results establish a polynomial-space upper bound, an explicit exponential algorithm, and a polynomial-time computable exponential move bound. They do not settle the requested general decision classification or polynomial-time terminal-state construction.

⟨structured verdict parsed — rendered above⟩

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

Verification report

Assessment: correct partial results; the general task remains unresolved.

The cycle construction, finite-state analysis, conditional move bound, general algorithms, and restricted convergence proofs are sound. I found no false central step. The output explicitly acknowledges that it does not settle the general decision classification or polynomial-time terminal-state construction.

One distinction matters: the task requests polynomial-time computation of a worst-case move bound, not necessarily a bound whose numerical value is polynomial. Section 3 does establish that requested bound computation.

1. Definitions and finite-state representation

The atom representation is valid. Every initially positive entry has a fixed mass and type. A legal move transfers all atoms comprising the source entry, and arrival can merge cohorts but cannot split them. Consequently, assigning the $K$ labeled atoms to candidates determines every reachable numerical state, giving
$$ N=m^K $$
as a valid upper bound.

Positive type masses ensure $k_t\ge 1$, and there are at most $m$ positive entries per type. Thus
$$ \tau\le K\le m\tau $$
is correct.

The exact-arithmetic argument also holds. The product $D$ has binary length $O(L)$ because the sum of the encoded denominator lengths is bounded by the total input length. Every reachable entry remains a sum of initial entries, so scaling by $D$ gives integers. The bounds
$$ 0\le x_{t,a}\le 1, \qquad \hat\rho(c)\le s_x(c)\le \hat\rho(c)+1 $$
justify $O(L)$-bit representations of scaled entries and scores. Exact winner and legality tests therefore require only polynomial bit complexity.

Minor terminology issue. Universal termination is a property of the instance and initial state, whereas the opening definition grammatically assigns it to “a legal sequence.” The intended quantification is explicit, so this does not affect any subsequent argument.

Minimum clarification: replace the subject of that definition with “The instance is universally terminating from $x^0$.”

2. Three-candidate cycle and reachable terminal state

Cycle verification

The five masses are positive, sum to one, and accompany distinct strict rankings. The initial state is truthful.

I independently recomputed all eleven score rows. They agree with the table. The winners along the ten moves are
$$ b,\ a,\ c,\ a,\ b,\ c,\ b,\ c,\ a,\ c,\ b. $$
Every winner is unique.

For each transition:

The final position tuple equals the initial tuple. Repetition therefore supplies an infinite legal sequence. With no fairness restriction, this establishes failure of universal termination.

The contextual citation is accurate: weighted direct-reply cycling is illustrated in [Meir et al., Example 7](https://arxiv.org/pdf/1606.05837). The submitted construction is independently verified and does not depend on importing that example’s proof.

Terminal-state verification

Moving type $1$ from $a$ to $c$ gives
$$ (c,b,b,c,c) $$
with scaled scores
$$ (1,28,50). $$
The move is legal because its resulting winner is $c$ and $c\succ_1 b$.

The terminality check exhausts the possibilities:

Thus a terminal state and an infinite legal sequence are both reachable from the same initial state. The claimed distinction between existence of a reachable terminal state and universal termination is proved.

Minimum candidate count

For $m=1$, distinct source and destination candidates do not exist.

For $m=2$, an improving destination must be the moving type’s preferred candidate. The source is therefore its less-preferred candidate. Once that entry is emptied, no legal move can refill it. This remains valid for initially split types.

Hence each type moves at most once, giving at most $\tau$ moves. Combined with the construction, the minimum candidate count permitting a cycle is exactly three.

No issue found in Section 2.

3. Conditional move bound

The number $p(x)$ of positive entries behaves as claimed:

Every type retains positive total mass, so there are at most
$$ h=K-\tau $$
merges.

Within a phase without merges, the atom partition into cohorts remains fixed. If type $t$ has $r_t$ cohorts, those labeled cohorts occupy distinct candidates. Therefore
$$ P(r)=\prod_{t\in T}(m)_{r_t} $$
bounds the number of placements, and hence the number of numerical states in that phase. Equal cohort masses can reduce the number of numerical states; they do not invalidate the upper bound.

Under universal termination, no numerical state can repeat along a legal sequence. A repeated state would permit indefinite repetition of the intervening moves. Consequently, the bound of $P(r)-1$ nonmerging moves per phase is valid.

For a sequence with $q$ merges, the accounting
$$ \sum_{i=0}^{q}\bigl(P(r^{(i)})-1\bigr)+q = \sum_{i=0}^{q}P(r^{(i)})-1 $$
is correct.

Sorted-divisor bound

The ratio
$$ \frac{(m)_r}{(m)_{r-1}}=m-r+1 $$
is correct. Successive merges within each type produce increasing divisors. Thus the globally sorted multiset admits an ordering consistent with each type’s required merge order, and every $P_i$ is an integer.

After $i$ actual merges, the divisor product uses $i$ elements of the multiset. Its product is at least the product of the $i$ smallest elements. This justifies the bound by $P_i$, and therefore by
$$ B=\sum_{i=0}^{h}P_i-1. $$

The additional state-count bound gives
$$ U=\min\{m^K-1,B\}. $$
The displayed simpler upper bound is also valid.

The stated arithmetic sizes and conservative computation time
$$ O\!\left(L+K^3\log^2(m+1)\right) $$
are consistent with the construction. The degenerate case $m=1$ gives $h=0$ and $U=0$.

No issue found in Section 3. It proves polynomial-time computation of a valid conditional worst-case move bound. It does not prove polynomial magnitude or compute the exact maximum sequence length.

The third item in the final open_points asks about polynomial magnitude. That is a stronger question than the task’s explicit bound-computation requirement and should not be treated as an unanswered requirement of that task.

4. General decision and construction algorithms

Reachable-cycle equivalence

Both directions are correct:

Finite maximal sequences end at terminal states. Hence universal termination is exactly absence of a reachable cycle.

Polynomial-space upper bound

Attempting exactly $N$ legal moves is a correct nondeterministic test for failure of universal termination.

A successful branch visits $N+1$ states, forcing repetition. Conversely, a reachable cycle permits a sequence of $N$ moves.

The current numerical state, exact arithmetic, move choices, and counter all require polynomial space. The bounded counter ensures that every branch halts. The stated consequence of Savitch’s theorem,
$$ \mathrm{NPSPACE}=\mathrm{PSPACE}, $$
applies, and deterministic polynomial space is closed under complement.

Thus
$$ \text{universal termination belongs to }\mathrm{PSPACE} $$
is established. This supplies neither polynomial-time membership nor hardness.

Labeled exhaustive graph

The correspondence between labeled and numerical trajectories is valid:

The vertex and outgoing-edge bounds are correct. Fixed-length assignment encodings support the claimed trie lookup costs. The conservative running time
$$ O\!\left(H^3+m^K\tau m^2H^2\right) $$
is consistent with exact successor generation and graph analysis.

On an acyclic reachable graph, a reachable sink projects to a terminal numerical state. Longest-path dynamic programming computes the exact maximum legal sequence length.

Direct simulation and fixed candidate count

Only source and destination scores change. Among the three largest score-priority keys, at least one remains unaffected when two distinct candidates are excluded. The proposed competitor lookup therefore works, including exact score ties.

The simulation bound
$$ O\!\left(H^3+(U+1)\tau m^2H\right) $$
is valid under universal termination. Its dependence on $U$ does not establish polynomial-time construction in general.

Finally, distinct supported rankings imply $\tau\le m!$, so $K$ is bounded solely by $m$ when $m$ is fixed. The claimed running time $g(m)L^{O(1)}$ and polynomial-time conclusions for each fixed $m$ follow.

No issue found in Section 4.

5. Restricted convergence results

Two initially unsplit cohorts

The minimal-closed-walk argument is sound.

Two cyclically consecutive moves by one type can be shortcut as described: the cohort is unsplit, the direct transfer produces the same final state, and preference transitivity supplies legality. If the second destination equals the original source, the numerical state returns, contradicting the strict winner improvements.

Consequently, the two types alternate on a minimal closed walk.

The treatment of coincident cohorts is valid. A move separates coincident cohorts, and alternating moves cannot reunite them because that would require moving to the current winner. Thus a closed walk cannot contain a coincident state.

At every remaining state, the next mover’s source differs from the current winner. Its destination also differs from that winner. The old winner’s score stays unchanged, so electing another candidate strictly increases the score-priority key. This cannot occur around a closed walk.

Universal termination follows. With at most $m^2$ states, the move bound
$$ m^2-1 $$
and construction time
$$ O(H^3+m^4H) $$
are valid.

One supported type

Every legal move strictly improves the winner in the sole ranking, regardless of initial splitting. Thus the bound of $m-1$ moves and the stated simulation time are correct.

No issue found in Section 5.

6. Task completeness and actionable feedback

There are two major completeness gaps, both acknowledged by the prover.

The polynomial-time computation of a valid move bound is already established. No repair to that result 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.