← back to the atlas

Optimal Bounds for Dissatisfaction in Perpetual Voting (aaai25-33529)

Answer: —

The anchor (named result in the paper)

Theorem 2 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateFor any k, N, T, C, there is a strategy of the Decision Maker, guaranteeing that all agents are dissatisfied at most: O T 1− 1 k+1 · (C · k · ln N) 1 k+1 times in the C-conflict perpetual voting with k options, N agents and T rounds.

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

The continuous mirror question, as graded

Given \(k,T,C,B\) and rational masses over persistent observable cohorts, with online current approval sets and no future revelation, construct or decide existence of an online rule choosing \(\theta_r \in [k]\) that guarantees \(\max_q \sum_r 1[\theta_r \notin A_q^r] \le B\) whenever every positive-mass \(k\)-tuple has empty approval intersection in at most \(C\) rounds.

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

A society is given by its support: a list of \(\tau\geq1\) persistent, observable cohort types, each with positive binary-rational mass \(\mu_q\), where \(\sum_q\mu_q=1\). Here \(\tau\) is the support size, not the number of possible approval sets. Cohorts retain their identities and masses; all members of a cohort share its current approvals.
The input also specifies \(m=k\geq1\) alternatives, a horizon \(T\geq1\), and integers \(0\leq C,B\leq T\). Alternatives are explicitly listed, \(T\) is encoded in unary, and \(C,B\) in binary; \(L\) denotes total input bit length.
In round \(r\), an adaptive adversary reveals arbitrary approval sets \(A_q^r\subseteq\{1,\ldots,k\}\), possibly empty, for every cohort. A deterministic online rule then chooses one alternative \(\theta_r\), using only the input and the revealed history; no future approvals are supplied.
Adversary moves must maintain \(\sum_{s=1}^{r}\mathbf{1}\{\bigcap_{i=1}^{k}A_{q_i}^{s}=\varnothing\}\leq C\) for every ordered tuple \((q_1,\ldots,q_k)\in\{1,\ldots,\tau\}^{k}\), with repetitions allowed. Thus the restriction also covers every nonempty subset of at most \(k\) cohorts.
A rule meets the threshold if every legal adversarial play satisfies \(\max_{1\leq q\leq\tau}\sum_{r=1}^{T}\mathbf{1}\{\theta_r\notin A_q^r\}\leq B\); dissatisfaction is measured per member, without mass weighting.

Is deciding whether such an online rule exists in \(\mathrm{P}\), with running time polynomial in \(m,\tau,T,L\), or is it \(\mathrm{NP}\)-hard?

For discrete societies with \(N\geq2\) agents and \(C\geq1\), an explicit exponential-weights online rule guarantees dissatisfaction \(O(T^{1-1/(k+1)}(Ck\ln N)^{1/(k+1)})\). This is a guaranteed bound, rather than an exact threshold-feasibility algorithm. [Kozachinskiy, Shen, and Steifer (2025)](https://ojs.aaai.org/index.php/AAAI/article/download/33529/35684)
No result settling this exact mass-cohort online existence problem was located.

Modeling choices made when packaging the task

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

Status

The uniform complexity classification remains unresolved. I prove several additional results:

I also reprove the obstruction to ordinary $\mathrm{NP}$-hardness: under polynomial-time many-one reductions, this problem is $\mathrm{NP}$-hard if and only if $\mathrm{P}=\mathrm{NP}$. This does not establish uniform polynomial-time solvability.

1. Definitions and elementary reductions

Write $[n]=\{1,\ldots,n\}$, and let
$$ V(k,\tau,T,C) $$
be the smallest dissatisfaction threshold guaranteed by a deterministic online rule. The game has finitely many histories, and threshold $T$ always succeeds, so this value exists. The decision problem asks whether
$$ V(k,\tau,T,C)\le B. $$

The masses do not affect this value. Indeed, fix any two mass assignments with the same parameters. A strategy for one assignment can be copied to the other, using identical choices on identical approval histories. Legality and cohort dissatisfaction are unchanged because neither uses masses. This copying argument works in both directions.

Repetitions in ordered tuples imply that legality is equivalent to
$$ c_S(r):=\sum_{s=1}^{r} \mathbf 1\left\{\bigcap_{q\in S}A_q^s=\varnothing\right\}\le C $$
for every nonempty $S\subseteq[\tau]$ with $|S|\le k$. An ordered tuple determines such a subset, and every such subset can be represented by a length-$k$ tuple using repetitions.

We will repeatedly use the following elementary witness property.

Empty-intersection witness. If a collection of approval sets on $[k]$ has empty intersection, some nonempty subcollection of at most $k$ sets already has empty intersection.

Proof. For each alternative $a\in[k]$, choose one cohort rejecting $a$. The distinct chosen cohorts form the required subcollection. $\square$

The adversary can reveal all-empty approvals for $C$ rounds and full approvals thereafter. Every constrained subset conflicts exactly $C$ times, and every cohort incurs dissatisfaction $C$. Consequently,
$$ V(k,\tau,T,C)\ge C. $$

If $C=0$, the witness property shows that every legal round has a globally common alternative. Choosing one gives
$$ V(k,\tau,T,0)=0. $$

2. A general upper bound by assigning conflict occurrences

Put
$$ s=\min(k,\tau), \qquad p=\sum_{j=1}^{s}\binom{\tau}{j}. $$

Theorem 1. For every instance,
$$ C\le V(k,\tau,T,C) \le \min\left\{ T,\ \left\lceil\frac{C}{\tau} \sum_{j=1}^{s}\binom{\tau}{j}\right\rceil \right\}. $$

The upper bound has an explicit deterministic online strategy. Its construction and execution take time polynomial in $Cp,\tau,k,T,L$. This is not a uniform polynomial bound because $p$ can be exponential.

2.1. Assigning the available conflict occurrences

Assume $C\ge1$; the case $C=0$ was proved above. For every constrained subset $S$, create $C$ tokens
$$ (S,1),\ldots,(S,C). $$
We assign each token to one cohort belonging to $S$. Let
$$ d=\left\lceil\frac{Cp}{\tau}\right\rceil. $$
There is an assignment giving at most $d$ tokens to each cohort.

To prove this, make a bipartite graph whose left vertices are the tokens and whose right vertices are $d$ copies of each cohort. A token belonging to $S$ is adjacent to every copy of every cohort in $S$.

Hall’s marriage theorem states that a matching covering all left vertices exists if every family of left vertices has at least as many neighbors as members. We check this condition.

Let $\mathcal F$ be any family of tokens, and let $U$ be the union of their underlying cohort subsets. Write $u=|U|$. For a nonempty family, $u\ge1$, and
$$ |\mathcal F| \le C\sum_{j=1}^{s}\binom{u}{j}, $$
where binomial coefficients vanish when $j>u$.

For $u\ge1$,
$$ \frac1u\sum_{j=1}^{s}\binom{u}{j} = \sum_{j=1}^{s}\frac1j\binom{u-1}{j-1}. $$
Every summand is nondecreasing in $u$. Since $u\le\tau$,
$$ C\sum_{j=1}^{s}\binom{u}{j} \le \frac{Cp}{\tau}\,u \le du. $$
The family’s neighborhood consists of the $d$ copies of the cohorts in $U$, so it has size $du$. Hall’s condition follows. The empty family satisfies it trivially.

Thus the required assignment exists and can be found by bipartite matching.

2.2. The online rule

In a round where $S$ conflicts for the $j$th time, consume token $(S,j)$. Legality ensures $j\le C$.

Call a cohort protected in the current round if it owns no token consumed in that round. The protected cohorts have a common approved alternative.

Indeed, suppose their approval intersection were empty. The witness property would give a conflicting subset $H$ of at most $k$ protected cohorts. The token consumed for $H$ is assigned to a member of $H$. That member would be unprotected, a contradiction.

Choose the smallest alternative approved by all protected cohorts. If there are none, choose alternative $1$.

Every dissatisfied cohort is unprotected, so it owns at least one token consumed that round. Charge its dissatisfaction to one such token. A token is consumed in only one round and has only one owner. Hence each cohort’s dissatisfaction is at most its number of assigned tokens, which is at most $d$.

This proves the upper bound. The trivial bound $T$ completes the theorem. $\square$

3. A counting lower bound and matching leading terms

Theorem 2. If $\tau\ge k\ge2$, then
$$ V(k,\tau,T,C) \ge \left\lceil \frac{\min\left\{T,\ C\binom{\tau}{k}\right\}}{\tau} \right\rceil. $$

Proof. Choose a sequence of
$$ R=\min\left\{T,\ C\binom{\tau}{k}\right\} $$
size-$k$ cohort subsets, with each subset appearing at most $C$ times.

For a round assigned to subset $S$, choose a bijection $f:S\to[k]$ and reveal
$$ A_q=[k]\setminus\{f(q)\}\quad(q\in S), \qquad A_q=[k]\quad(q\notin S). $$

A constrained subset $H$ conflicts precisely when $H=S$. To see this, empty intersection requires rejecting all $k$ alternatives. The only rejecting cohorts are the members of $S$, each rejecting a different alternative. Thus $H$ must contain all of $S$; since $|H|\le k=|S|$, it must equal $S$.

Consequently, every constrained subset conflicts at most $C$ times, so all prefixes are legal.

Whichever alternative the rule chooses, exactly one cohort is dissatisfied in that round. Fill remaining rounds with full approvals. Total cohort dissatisfaction is $R$, so some cohort incurs at least $\lceil R/\tau\rceil$. $\square$

For horizons satisfying
$$ T\ge C\binom{\tau}{k}, $$
Theorems 1 and 2 give
$$ \left\lceil\frac{C}{\tau}\binom{\tau}{k}\right\rceil \le V(k,\tau,T,C) \le \left\lceil\frac{C}{\tau} \sum_{j=1}^{k}\binom{\tau}{j}\right\rceil. $$

In particular,
$$ 0\le V(k,\tau,T,C)-\frac{C}{k}\binom{\tau-1}{k-1} \le C\sum_{j=1}^{k-1}\frac1j\binom{\tau-1}{j-1}+1. $$
Here we used
$$ \frac1\tau\binom{\tau}{j} = \frac1j\binom{\tau-1}{j-1}. $$

For every fixed $k\ge2$, this proves the asymptotically sharp statement
$$ V(k,\tau,T,C) = \frac{C}{k!}\tau^{k-1} + O_k\!\left(C\tau^{k-2}+1\right) $$
as $\tau$ tends to infinity, provided $C\ge1$ and $T\ge C\binom{\tau}{k}$. The estimate follows by expanding the fixed-degree binomial polynomial and bounding the lower-degree summands above.

This determines the leading term, not the exact finite-parameter value.

4. Exact feasibility when the support has at most one extra cohort

Theorem 3. If $\tau\le k+1$, then
$$ V(k,\tau,T,C)=C. $$
Also, if $k=1$, the same conclusion holds for every $\tau$.

Proof for $\tau\le k$. The whole cohort set is constrained, so globally empty intersection occurs at most $C$ times. Choose a globally common alternative whenever one exists. Dissatisfaction can occur only in those at most $C$ rounds. The lower bound from Section 1 gives equality.

Proof for $\tau=k+1$. Arrange the cohorts in a directed cycle. Let $\operatorname{pred}(q)$ denote the predecessor of $q$, and define
$$ S_q=[\tau]\setminus\{\operatorname{pred}(q)\}. $$
Each $S_q$ has size $k$, contains $q$, and has conflict budget $C$.

In a round, call $q$ protected if
$$ \bigcap_{p\in S_q}A_p\ne\varnothing. $$
The protected cohorts have a common alternative.

For otherwise, the witness property supplies a nonempty subset $H$ of protected cohorts with empty intersection and
$$ |H|\le k=\tau-1. $$
Thus $H$ is a proper subset of the cycle. There is some $q\in H$ whose predecessor lies outside $H$: traverse the cycle from an outside vertex until first entering $H$. Therefore $H\subseteq S_q$, which implies that $S_q$ has empty intersection. This contradicts the protection of $q$.

Choose an alternative approved by all protected cohorts. Whenever $q$ is dissatisfied, $S_q$ conflicts. Hence
$$ D_q\le c_{S_q}(T)\le C. $$
The lower bound again gives equality.

Proof for $k=1$. The only alternative is forced. A cohort is dissatisfied exactly when its approval set is empty, and its singleton conflict budget bounds this count by $C$. $\square$

Thus these regimes admit the exact polynomial-time test $B\ge C$.

5. Two alternatives: an optimal bound for long horizons

For $k=2$, singleton and pair conflicts are the only constraints. We can improve Theorem 1 by using pair tokens alone.

Theorem 4. If $k=2$ and $\tau\ge3$, then
$$ V(2,\tau,T,C) \le \min\left\{ T,\ \left\lceil\frac{C(\tau-1)}2\right\rceil \right\}. $$
The strategy is computable in time polynomial in $\tau,T,L$.

Consequently, if
$$ T\ge C\binom{\tau}{2}, $$
then
$$ V(2,\tau,T,C) = \left\lceil\frac{C(\tau-1)}2\right\rceil. $$
For $\tau\le3$, Theorem 3 already gives $V=C$ for every horizon.

5.1. A balanced orientation of pair tokens

For every unordered pair, create $C$ parallel edges, representing its successive conflict occurrences. Orient each edge toward the cohort owning that token.

First fix a directed Hamilton cycle on the $\tau$ cohorts. Orient all $C$ copies of each cycle edge in its cycle direction. Every cohort receives exactly $C$ incoming cycle tokens.

The remaining multigraph has degree
$$ C(\tau-3) $$
at every vertex. It admits an orientation with indegree at most
$$ \left\lceil\frac{C(\tau-3)}2\right\rceil $$
at every vertex.

Here is a proof of the orientation fact. In any finite undirected multigraph, the number of odd-degree vertices is even by the degree-sum identity. Add an auxiliary vertex joined once to each odd-degree vertex. All degrees become even. Orient an Euler circuit in each nontrivial connected component. Incoming and outgoing degrees are then equal. Removing the auxiliary edges leaves indegree at most half the original degree rounded upward at every original vertex.

Combining the two orientations, every cohort owns at most
$$ C+\left\lceil\frac{C(\tau-3)}2\right\rceil = \left\lceil\frac{C(\tau-1)}2\right\rceil $$
pair tokens.

Label each pair’s copies by its occurrence numbers from $1$ to $C$. For cycle pairs, all these copies have the same owner.

5.2. Protection also handles empty approvals

In each round, consume the next token of every conflicting pair. Call a cohort protected if it owns no token consumed that round.

Every protected cohort has nonempty approvals. Indeed, if $q$ has empty approvals, its pair with its cycle predecessor conflicts. The token for that pair is always directed toward $q$, making $q$ unprotected.

Moreover, the protected cohorts have a common alternative. For nonempty subsets of $\{1,2\}$, empty common intersection requires a cohort approving only $1$ and another approving only $2$. Their pair conflicts, and its consumed token belongs to one of them, contradicting that cohort’s protection.

Choose an alternative approved by all protected cohorts. Charge each dissatisfied cohort to an incoming pair token consumed that round. Tokens are never consumed twice, so the orientation bound proves the claimed dissatisfaction guarantee.

The orientation construction uses at most $C\binom{\tau}{2}$ edges. Because $C\le T$ and $T$ is unary, construction and round-by-round processing are polynomial in the stated input parameters.

Finally, Theorem 2 for $k=2$ gives the matching lower bound when the horizon contains all $C\binom{\tau}{2}$ pair rounds. $\square$

In particular, for $C=1$, $\tau\ge2$, and $T\ge\binom{\tau}{2}$,
$$ V(2,\tau,T,1)=\left\lfloor\frac{\tau}{2}\right\rfloor. $$

6. Two alternatives and one conflict: exactly when every round can be lost

This section gives an exact finite-horizon criterion at threshold $B=T-1$.

Theorem 5. Suppose $k=2$, $C=1$, and $T\ge2$. Then
$$ V(2,\tau,T,1)=T \quad\Longleftrightarrow\quad \tau\ge2^T. $$

6.1. Empty approvals cannot cause repeated dissatisfaction

Consider any rule that chooses a globally common alternative whenever one exists.

Lemma. Under this rule, a cohort that has empty approvals in some round incurs dissatisfaction exactly once in the entire play.

Proof. For $\tau=1$, every other round has nonempty approvals because the singleton conflict budget is one. The rule satisfies the cohort in those rounds.

Suppose $\tau\ge2$, and $q$ is empty in round $r$. Every pair containing $q$ conflicts in that round. Thus, by the pair budget, in every other round $s$,
$$ A_q^s\cap A_p^s\ne\varnothing \quad\text{for every }p\ne q. $$
The singleton budget also ensures $A_q^s\ne\varnothing$.

If $A_q^s=\{1,2\}$, the cohort is satisfied by any choice. If $A_q^s=\{a\}$, the displayed intersections imply that every cohort approves $a$. The rule therefore chooses $a$. Thus $q$ is satisfied in every round except $r$. $\square$

6.2. The upper direction by halving candidates

Maintain
$$ H_0=[\tau], $$
and let $H_r$ contain the cohorts that have had nonempty approvals and been dissatisfied in every one of the first $r$ rounds.

Choose a globally common alternative whenever one exists. Otherwise, among the nonempty-approval cohorts in $H_{r-1}$, choose the alternative approved by the larger number, breaking ties deterministically.

If there are $h$ such cohorts, their total number of approvals of the two alternatives is at least $h$. Hence one alternative is approved by at least $\lceil h/2\rceil$ of them. It follows that
$$ |H_r| \le \left\lfloor\frac{h}{2}\right\rfloor \le \left\lfloor\frac{|H_{r-1}|}{2}\right\rfloor. $$
A globally common choice instead makes $H_r$ empty. Inductively,
$$ |H_T|\le\left\lfloor\frac{\tau}{2^T}\right\rfloor. $$

If $\tau<2^T$, this set is empty. By the lemma, a cohort encountering empty approvals has total dissatisfaction one, which is less than $T$. Every cohort dissatisfied in all $T$ rounds would therefore belong to $H_T$, a contradiction. Thus
$$ V(2,\tau,T,1)\le T-1. $$

6.3. The lower direction by adaptive splitting

Suppose $\tau\ge2^T$. Select an active set $H_0$ of $2^T$ cohorts.

In round $r$, partition $H_{r-1}$ into equal groups $X_r,Y_r$. Give approvals $\{1\}$ to $X_r$, approvals $\{2\}$ to $Y_r$, and full approvals to all other cohorts. After the rule chooses, let $H_r$ be the dissatisfied group.

Then
$$ |H_r|=2^{T-r}, $$
and every member of $H_r$ has been dissatisfied in all first $r$ rounds. One cohort therefore loses all $T$ rounds.

Singletons never conflict. A pair conflicts only when both cohorts are active and placed in opposite groups. After such a split, at most one member remains active, so that pair cannot conflict again. Hence every pair conflicts at most once, and the adversary is legal.

This proves $V=T$ and completes the theorem. $\square$

For $T=1$, all-empty approvals give $V=1$ regardless of support size; this is why the theorem assumes $T\ge2$.

7. What the results imply about complexity

7.1. Ordinary many-one hardness would collapse $\mathrm{P}$ and $\mathrm{NP}$

Let $\mathcal E$ be the decision language, rejecting malformed inputs. Since masses and names are irrelevant, map each valid input to
$$ 1^k0\,1^\tau0\,1^T0\,1^C0\,1^B0. $$
Let $\mathcal S$ contain exactly those valid canonical strings whose parameters satisfy $V(k,\tau,T,C)\le B$.

This is a polynomial-time many-one reduction. Input validity, including positivity and normalization of binary-rational masses, can be checked by polynomial-bit rational arithmetic. Explicit listing and unary $T$ imply that $k,\tau,T$ are bounded by input length $L$; also $C,B\le T$. Thus the canonical output has polynomial length. Invalid inputs can be mapped to a fixed invalid canonical string.

There are at most $(n+1)^5$ candidate canonical strings of length at most $n$, so $\mathcal S$ is sparse.

Mahaney’s theorem states that a sparse language that is $\mathrm{NP}$-hard under polynomial-time many-one reductions implies $\mathrm{P}=\mathrm{NP}$; membership of the sparse language in $\mathrm{NP}$ is not required. This precise statement and proof appear in [Grochow, Theorem 2.1](https://arxiv.org/html/1610.05825).

Therefore, if $\mathcal E$ were $\mathrm{NP}$-hard, composing reductions would make the sparse language $\mathcal S$ $\mathrm{NP}$-hard, forcing $\mathrm{P}=\mathrm{NP}$.

Conversely, under $\mathrm{P}=\mathrm{NP}$, every $\mathrm{NP}$ language can be decided in polynomial time and reduced to any language with a fixed yes-instance and a fixed no-instance. Here one may use mass one and:

Thus
$$ \mathcal E\text{ is }\mathrm{NP}\text{-hard under polynomial-time many-one reductions} \quad\Longleftrightarrow\quad \mathrm{P}=\mathrm{NP}. $$

7.2. Polynomial-space membership

An entire approval and choice history uses polynomial space because $k,\tau,T$ are bounded by $L$.

For a proposed next approval matrix, enumerate the ordered tuples in $[\tau]^k$ one at a time. For each tuple, scan the stored history and count its empty intersections. The enumeration can take exponential time, but the tuple, intersections, and counters require only polynomial space.

Evaluate the game recursively: a history is winning if every legal next approval matrix admits an alternative leading to a winning continuation. At depth $T$, test all cohort dissatisfaction counts against $B$. Depth-first evaluation enumerates matrices and alternatives sequentially and has polynomial depth and polynomial space per frame.

This proves
$$ \mathcal E\in\mathrm{PSPACE}. $$

8. Remaining open points

The new strategies decide exact feasibility in the stated special regimes and give asymptotically sharp values for fixed $k$ with sufficiently long horizons. They do not provide an exact feasibility algorithm for arbitrary $k,\tau,T,C,B$.

In particular, the general token construction may enumerate exponentially many subsets. Even for two alternatives, the results above do not characterize every finite-horizon threshold. Consequently, uniform membership in $\mathrm{P}$ remains unproved, while ordinary many-one $\mathrm{NP}$-hardness would settle $\mathrm{P}=\mathrm{NP}$.

⟨structured verdict parsed — rendered above⟩

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

Verification report

Overall assessment: correct partial progress, with minor expositional gaps. The substantive bounds, special-case characterizations, sparsity argument, and polynomial-space membership argument withstand verification. No false central step was found.

The output does not settle USER_TASK: it establishes neither a uniform polynomial-time exact feasibility algorithm nor unconditional $\mathrm{NP}$-hardness. The prover explicitly acknowledges this limitation.

1. Definitions and elementary reductions

The definition of $V(k,\tau,T,C)$ is valid. There are finitely many approval histories and choices, and dissatisfaction never exceeds $T$, so a smallest achievable integer threshold exists.

The mass-independence argument is correct. Copying a strategy between mass assignments preserves the approval history, legality, and every cohort’s dissatisfaction. This relies on precisely the task’s unweighted dissatisfaction measure and persistent cohort identities.

The equivalence between ordered-tuple constraints and constraints on nonempty subsets of size at most $k$ is correct:

The empty-intersection witness is correct. If the intersection is empty, each alternative has a rejecting cohort, and the distinct chosen cohorts constitute a nonempty witness of size at most $k$.

The all-empty construction proves $V\ge C$, including the endpoints $C=0$ and $C=T$. For $C=0$, the witness property excludes a globally empty intersection in every legal round, establishing $V=0$.

Finding: These reductions and base cases are sound.

2. General token upper bound

Assignment of tokens

The Hall argument checks the required condition for every family of left vertices, rather than merely for families consisting of all tokens of selected subsets.

For a token family with underlying union $U$, the bound
$$ |\mathcal F|\le C\sum_{j=1}^{s}\binom{|U|}{j} $$
is correct. Its neighborhood contains exactly all $d$ copies of every cohort in $U$.

The identity
$$ \frac{1}{u}\binom{u}{j} = \frac{1}{j}\binom{u-1}{j-1} $$
and monotonicity in $u$ justify the comparison with $Cp/\tau$. Thus the neighborhood has sufficient capacity. The empty family is also explicitly handled.

Hall’s theorem is stated in the form needed, and its hypotheses are verified.

Online protection and charging

The protection argument is sound: an empty intersection among protected cohorts would supply a constrained conflicting subset whose consumed token belongs to a protected cohort, contradicting protection.

The charging argument is also sound. A dissatisfied cohort owns a consumed token, each token is consumed in only one round, and its owner is unique. Consequently, no cohort can accumulate more dissatisfaction than its assigned token count.

The construction is online: assignments are fixed in advance, and token consumption depends only on observed conflict occurrences.

The stated polynomial dependence on $Cp,\tau,k,T,L$ is consistent with the matching graph and explicit subset processing. The prover correctly declines to interpret this as a uniform polynomial bound.

Minor issue: The handling of an empty protected set is not stated consistently. “If there are none” in Section 2.2 has an ambiguous antecedent, and later protection strategies omit an explicit convention. This does not affect the bound, but the rule should specify its choice when no cohort is protected.

Finding: Theorem 1 is sound, subject to that routine clarification.

3. Counting lower bound and asymptotics

In a round associated with a size-$k$ subset $S$, each member of $S$ rejects one distinct alternative, and every other cohort approves everything.

The claim that a constrained subset $H$ conflicts exactly when $H=S$ is correct. To reject all alternatives, $H$ must contain every member of $S$; the size restriction then forces equality.

Thus every constrained subset respects its budget at every prefix. Exactly one cohort is dissatisfied per constructed round, regardless of the rule’s choice. The averaging lower bound follows.

The construction also handles $C=0$, where the constructed sequence has length zero.

For the stated long-horizon regime, both bounds apply. The conversion
$$ \frac{C}{\tau}\binom{\tau}{k} = \frac{C}{k}\binom{\tau-1}{k-1} $$
is correct, and the ceiling contributes at most the stated additive unit.

For fixed $k\ge2$, the binomial-polynomial expansion and lower-degree terms yield the claimed error
$$ O_k\!\left(C\tau^{k-2}+1\right). $$
The restrictions $C\ge1$ and $T\ge C\binom{\tau}{k}$ are explicitly present.

Finding: Theorem 2 and the asymptotic conclusions are correct. They establish bounds, not exact general feasibility.

4. Exact value for small support

For $\tau\le k$, the whole cohort set is constrained. Choosing a common alternative whenever one exists confines dissatisfaction to at most $C$ rounds. Together with the earlier lower bound, this gives equality.

For $\tau=k+1$, the cycle argument is correct:

Whenever $q$ is dissatisfied, $q$ is unprotected and $S_q$ conflicts. The resulting bound $D_q\le C$ is justified.

For $k=1$, singleton budgets directly bound the forced alternative’s dissatisfaction.

The threshold test $B\ge C$ therefore follows in these regimes.

Minor issue: As in Section 2, the strategy should specify its action when the protected set is empty and fix a deterministic choice when several alternatives qualify.

Finding: Theorem 3 is correct; the issue concerns complete specification of the rule.

5. Two-alternative upper bound and long-horizon equality

For $\tau\ge3$, the Hamilton cycle uses two distinct incident pair edges at each cohort. Orienting all $C$ copies cyclically gives exactly $C$ incoming tokens per cohort. Removing these edges leaves degree $C(\tau-3)$, as claimed.

The auxiliary-vertex orientation argument is valid:

The arithmetic
$$ C+\left\lceil\frac{C(\tau-3)}2\right\rceil = \left\lceil\frac{C(\tau-1)}2\right\rceil $$
is correct.

Minor issue: Existence of the Euler circuits is invoked implicitly. The write-up should state the standard Euler-circuit theorem being used. This is an expositional omission: the necessary even-degree and connected-component hypotheses are satisfied.

The protection argument correctly handles empty approvals: an empty cohort consumes its incoming cycle-pair token and hence cannot be protected.

Among nonempty subsets of the two alternatives, a failure of common intersection requires opposing singleton approvals. Their conflicting pair contradicts their simultaneous protection.

Charging dissatisfaction to owned pair tokens proves the bound. Since $C\le T$ and $T$ is unary, the explicit multigraph construction is polynomial in the input parameters.

The long-horizon lower bound matches exactly. The subsequent identity for $C=1$ is correct, including $\tau=2$, which is covered by Theorem 3.

Finding: Theorem 4 and its exact long-horizon consequence are sound, with the routine clarifications above.

6. Exact criterion for losing every round

Empty-approval lemma

If a cohort is empty in one round, every pair containing it conflicts then. With $C=1$, those pairs must intersect in every other round.

The proof correctly separates the possibilities for that cohort’s later nonempty approvals. Full approvals guarantee satisfaction, while singleton approvals force a globally common alternative that the rule must choose.

For $\tau=1$, the separate singleton-budget argument is correct.

Upper direction

The candidate set definition correctly excludes cohorts that have encountered empty approvals.

Among the $h$ remaining candidates with nonempty approvals, total approval incidence is at least $h$, so the chosen alternative satisfies at least $\lceil h/2\rceil$ candidates. Hence the displayed halving recurrence is justified.

The resulting bound
$$ |H_T|\le\left\lfloor\frac{\tau}{2^T}\right\rfloor $$
excludes an always-dissatisfied cohort when $\tau<2^T$. The empty-approval lemma completes the argument because $T\ge2$.

Lower direction

The adaptive split construction respects the order of moves: approvals are revealed before the rule chooses, and the next active set is selected afterward.

Every retained cohort has lost every preceding round. A pair can conflict only at the split separating its members; afterward, at most one remains active, and inactive cohorts receive full approvals. Thus no pair conflicts twice.

The endpoint $T=1$ is separately and correctly excluded from the characterization.

Finding: Theorem 5 is correct, with both directions and legality verified.

7. Complexity claims

Sparse canonicalization

The reduction discarding masses and names is valid because these data do not affect feasibility. The canonical encoding retains all relevant parameters.

The explicit alternatives and cohort list, unary horizon, and bounds $C,B\le T$ ensure polynomial output length. Polynomial-bit rational arithmetic suffices to check positivity and normalization of the listed masses.

The number of canonical strings of length at most $n$ is polynomially bounded as claimed. Mapping malformed inputs to a fixed string outside the canonical language completes the reduction.

The cited version of Mahaney’s theorem is accurate: sparse $\mathrm{NP}$-hard languages under polynomial-time many-one reductions imply $\mathrm{P}=\mathrm{NP}$, without requiring membership in $\mathrm{NP}$. The cited source states this version and proves it using such a reduction. [Grochow, Theorem 2.1](https://arxiv.org/html/1610.05825)

Reduction composition therefore justifies the forward implication.

The reverse implication is also correct. Under $\mathrm{P}=\mathrm{NP}$, any $\mathrm{NP}$ language can be decided in polynomial time and mapped to the displayed fixed yes-instance or no-instance. Both instances have the claimed feasibility status.

Finding: The equivalence concerning ordinary many-one $\mathrm{NP}$-hardness is established. It does not establish membership in $\mathrm{P}$ or unconditional hardness.

Polynomial-space membership

The stored history has polynomial size because the horizon is unary.

Enumerating ordered tuples requires polynomial space despite potentially exponential time. Scanning the history verifies all prefix budgets; conflict counts are monotone, so checking the accumulated count suffices.

The recursive quantifiers match the online game: every legal next approval matrix must admit a choice with a winning continuation. Sequential depth-first enumeration, polynomial depth, and polynomial storage per frame establish the space bound.

Finding: Membership in $\mathrm{PSPACE}$ is correctly proved.

8. Scope and actionable feedback

The major outstanding issue is task incompleteness, rather than a false mathematical claim. The prover explicitly states that arbitrary finite-horizon threshold feasibility remains unresolved. Neither asymptotic bounds nor exact special regimes determine the answer for all allowed inputs.

Minimum clarification needed for the existing results:

Resolving USER_TASK requires an additional general complexity result. That requirement cannot be met by an expositional clarification to the present arguments.

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