← back to the atlas

d4-conf-atal-2015-0280 (d4-conf-atal-2015-0280)

Answer: —

The anchor (named result in the paper)

Theorem 3 — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximateGiven W, P −, FeasibleB(⃗c), and T ≥0, checking whether the minimax value is smaller than T is coNP-complete. The main theoretical contribution of this section is an O((m + k)n2−nmn) algorithm for computing the minimax value and the corresponding minimax plan, when W can be represented by k lin- ear constraints on ⃗w. More precisely, for any K ⊆{R}n, we let WK = {⃗w : ∀⃗a ∈K,⃗a · ⃗w ≥0}.

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

The continuous mirror question, as graded

Given a society μ over complete feature and cost types, with binary-rational masses summing to one, a marked target type of mass α and feature vector \(x^\star\), a budget \(B\), costs \(C\), and a rationally described allowed weight set \(W\), decide whether there is a common cohort update \(Δ ≥ 0\), with \(C · Δ ≤ B\), such that for every \(w ∈ W\), the mass whose score exceeds \(w · (x^\star+Δ)\) is less than a given threshold \(q\).

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

A society is given by its support: a list of \(\tau\) distinct feature-and-cost types \((x_i,C_i)\), each with positive binary-rational mass \(\mu_i\), with \(\sum_i\mu_i=1\). Here \(\tau\) is the support size, not the number of possible types; \(m\geq1\) is the feature dimension. Initial features lie in \(\mathbb Q^m\cap[-\tfrac12,\tfrac12]^m\), and costs lie in \(\mathbb Q_{>0}^m\).
A marked support type \(t\) has mass \(\alpha=\mu_t\), features \(x^\star=x_t\), and costs \(C=C_t\). The input also gives binary rationals \(B\geq0\) and \(q\in[0,1]\), and a nonempty allowed weight set \(W=\{w\in\mathbb R_{\geq0}^m:\sum_jw_j=1,\ Aw\leq b\}\), with \(k\) rational linear inequalities.
A common update \(\Delta\in\mathbb R_{\geq0}^m\) changes the entire marked cohort to \(x^\star+\Delta\); all other types remain fixed. Feasibility means \(C\cdot\Delta\leq B\), with budget interpreted per cohort member and no upper bound on updated features. Scores are \(w\cdot x\); equal scores tie and do not count as exceeding the target.
Decide whether some feasible \(\Delta\) satisfies \(\sum_{i\ne t:\,w\cdot x_i>w\cdot(x^\star+\Delta)}\mu_i<q\) for every \(w\in W\). State running times in \(m,\tau,k,L\), where \(L\) is the total binary input length.

Is this continuous cohort-update decision problem in \(\mathrm P\), or is it \(\mathrm{NP}\)-hard?

The discrete minimax-rank threshold decision problem is stated to be \(\mathrm{coNP}\)-complete ([source](https://www.cs.rpi.edu/~magdon/ps/conference/RankingsAAMAS2015.pdf)). No result settling exactly the mass-based cohort-update problem was identified in the literature search.

Modeling choices made when packaging the task

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

1. Proven classification

The problem is \(\mathrm{coNP}\)-complete under polynomial-time many-one reductions, even with a strictly positive budget. It admits an exact algorithm with running time
\((\tau^2+k+m)^{O(m)}\operatorname{poly}(L)\), so it is polynomial-time solvable for every fixed feature dimension.

Consequently, the requested dichotomy requires a reduction convention:

The cited paper states the related discrete rank result in Theorem 3. The proof below establishes the mass-based result directly, including positive budgets. [Computing Manipulations of Ranking Systems](https://www.cs.rpi.edu/~magdon/ps/conference/RankingsAAMAS2015.pdf)

2. The strict mass condition defines closed halfspaces

Let \(I=\{i:i\ne t\}\) and \(\beta=\sum_{i\in I}\mu_i=1-\alpha\).

Two boundary cases are immediate:

Henceforth assume \(0<q\leq\beta\). In particular, \(I\) is nonempty.

For \(w\in W\), define
\[ \]
\(h(w)=\max_{\substack{S\subseteq I\\ \sum_{i\in S}\mu_i\geq q}}\ \min_{i\in S}w\cdot x_i.\)

The maximum exists because its indexing family is finite and nonempty.

Lemma 1. For every \(y\in\mathbb R^m\) and \(w\in W\),
\[ \]
\(\sum_{\substack{i\in I\\w\cdot x_i>w\cdot y}}\mu_i<q \quad\Longleftrightarrow\quad w\cdot y\geq h(w).\)

Proof. Suppose first that \(w\cdot y<h(w)\). A maximizing subset \(S\) has mass at least \(q\), and every member satisfies
\(w\cdot x_i\geq h(w)>w\cdot y\).
Thus the exceeding mass is at least \(q\).

Conversely, if the exceeding mass is at least \(q\), take
\(S=\{i\in I:w\cdot x_i>w\cdot y\}\).
This is a nonempty finite set, so
\(\min_{i\in S}w\cdot x_i>w\cdot y\).
It follows that \(h(w)>w\cdot y\). These two implications prove the equivalence. \(\square\)

In particular, ties are handled exactly as required. Successful updates are precisely the points of
\[ \]
\(P_0\cap\bigcap_{w\in W}\{\Delta:w\cdot\Delta\geq h(w)-w\cdot x^\star\},\)
where
\[ \]
\(P_0=\{\Delta\in\mathbb R_{\geq0}^m:C\cdot\Delta\leq B\}.\)

Thus the set of successful updates is convex. The strict mass threshold produces a nonstrict score inequality, rather than an open halfspace.

3. A finite linear program and its running time

Write \(r=|I|=\tau-1\). Consider the following hyperplanes in weight space:

Their number is at most
\(H=k+m+\binom r2\).
Identically zero equations can be ignored.

For each choice of \(m-1\) of these hyperplanes, combine their equations with \(\sum_jw_j=1\). If this system has a unique solution and that solution belongs to \(W\), retain it. Let \(V\) be the resulting finite set. Then
\[ \]
\(|V|\leq\binom H{m-1}.\)

For \(m=1\), the empty choice gives the unique simplex weight.

Lemma 2. An update satisfies the mass condition for every \(w\in W\) if and only if it satisfies
\[ \]
\(v\cdot\Delta\geq h(v)-v\cdot x^\star\qquad\text{for every }v\in V.\)

Proof. Necessity follows from \(V\subseteq W\).

For sufficiency, let \(\sigma\) be a permutation of \(I\), and consider the possibly empty polytope
\[ \]
\(P_\sigma=\{w\in W:w\cdot x_{\sigma(1)}\geq\cdots\geq w\cdot x_{\sigma(r)}\}.\)

These polytopes cover \(W\), including all score ties. Let \(\ell_\sigma\) be the smallest index satisfying
\[ \]
\(\sum_{a=1}^{\ell_\sigma}\mu_{\sigma(a)}\geq q.\)

For every \(w\in P_\sigma\),
\[ \]
\(h(w)=w\cdot x_{\sigma(\ell_\sigma)}.\)

Indeed, the first \(\ell_\sigma\) types form a subset of sufficient mass whose minimum score is the displayed value. Conversely, the total mass of types with strictly larger score is at most
\(\sum_{a=1}^{\ell_\sigma-1}\mu_{\sigma(a)}<q\).
Therefore every subset of sufficient mass contains a type with score no larger than that value.

Every vertex of a nonempty \(P_\sigma\) belongs to \(V\). To verify this even when \(P_\sigma\) has lower dimension, suppose that the simplex equality and the active boundary equations at a vertex do not have rank \(m\). There is then a nonzero direction preserving all these equations. Moving a sufficiently small distance in either direction also preserves the inactive inequalities, contradicting extremality. Consequently, \(m-1\) active equations can be chosen together with the simplex equality to determine the vertex uniquely. All these equations occur in the enumerated list.

On \(P_\sigma\), the required inequality becomes
\[ \]
\(w\cdot(x^\star+\Delta-x_{\sigma(\ell_\sigma)})\geq0.\)

This is linear in \(w\). Every nonempty \(P_\sigma\) is a bounded polytope, hence the convex hull of its vertices. If the inequality holds at those vertices, it holds throughout \(P_\sigma\). Since the polytopes cover \(W\), the result follows. \(\square\)

The decision problem therefore reduces exactly to the rational linear program
\[ \]
\(\Delta\geq0,\qquad C\cdot\Delta\leq B,\qquad v\cdot\Delta\geq h(v)-v\cdot x^\star\quad(v\in V).\)

Each retained weight has encoding length polynomial in \(m,L\): it solves a full-rank rational linear system of dimension \(m\), so the claim follows from determinant bounds and Cramer’s rule.

For each \(v\), compute \(h(v)\) by sorting rival scores in nonincreasing order and finding the first cumulative mass reaching \(q\). Exact rational arithmetic has polynomial bit complexity here.

Enumerating the candidate systems and solving the final rational linear program takes
\[ \]
\(\left(\binom H{m-1}+1\right)^{O(1)} \operatorname{poly}(m,\tau,k,L) \ \subseteq\ (\tau^2+k+m)^{O(m)}\operatorname{poly}(L).\)

This proves polynomial-time solvability for every fixed \(m\).

4. Membership in \(\mathrm{coNP}\)

We now show that a NO instance has a polynomial-size certificate, without enumerating all of \(V\).

For \(v\in V\), write
\[ \]
\(K_v=\{\Delta:v\cdot\Delta\geq h(v)-v\cdot x^\star\}.\)

By Lemma 2, a NO instance satisfies
\(P_0\cap\bigcap_{v\in V}K_v=\varnothing\).

We apply Helly’s theorem: a finite family of convex subsets of \(\mathbb R^m\) with empty intersection has a subfamily of at most \(m+1\) sets with empty intersection. Its hypotheses hold because \(P_0\) and every \(K_v\) are convex and the family is finite.

Moreover, the halfspaces \(K_v\) alone have a common point. Let \(\mathbf1\) denote the vector with every coordinate equal to one. Since all initial features lie in the given cube and \(v\) is a simplex weight,
\[ \]
\(h(v)-v\cdot x^\star\leq\tfrac12-(-\tfrac12)=1 =v\cdot\mathbf1.\)

Thus \(\mathbf1\in K_v\) for every \(v\). Any subfamily with empty intersection must consequently include \(P_0\).

It follows that there exist \(s\leq m\) weights \(v^{(1)},\ldots,v^{(s)}\in V\) such that
\[ \]
\(P_0\cap K_{v^{(1)}}\cap\cdots\cap K_{v^{(s)}}=\varnothing.\)

These weights form a polynomial-size NO certificate: each has polynomial encoding length by Section 3. A verifier:

All three steps take polynomial time in \(m,\tau,k,L\). Soundness follows from Lemma 1 even if the supplied weights are not vertices. Completeness follows from Helly’s theorem and the finite formulation.

The case \(q=0\) is directly recognizable. Therefore the problem belongs to \(\mathrm{coNP}\).

5. Direct \(\mathrm{coNP}\)-hardness with positive budget

We give a polynomial-time many-one reduction from 3UNSAT, the complement of 3SAT. Use formulas with \(n\geq1\) variables and \(c\geq1\) clauses, each having three literal occurrences. This restricted form remains \(\mathrm{coNP}\)-complete.

5.1 Linear predicates encoding satisfiability

Introduce \(z\in[0,1]^n\). For every variable \(j\), introduce two predicates:
\[ \]
\(z_j>\tfrac9{10},\qquad z_j<\tfrac1{10}.\)

For every clause, introduce the predicate
\[ \]
\(\ell_1(z)+\ell_2(z)+\ell_3(z)>\tfrac12,\)
where a positive literal has value \(z_j\), and a negative literal has value \(1-z_j\).

There are \(N=2n+c\) predicates. Write them as
\(a_i\cdot z-b_i>0\), for \(1\leq i\leq N\). Their coefficients satisfy
\[ \]
\(|a_{ij}|\leq3,\qquad |b_i|\leq\tfrac52.\)

Lemma 3. There exists \(z\in[0,1]^n\) satisfying at least \(n+c\) predicates if and only if the formula is satisfiable.

Proof. For each variable, at most one of its two predicates can hold. Thus at most \(n\) variable predicates and at most \(c\) clause predicates hold.

Reaching \(n+c\) forces exactly one predicate for every variable and all clause predicates. Assign variable \(j\) true when \(z_j>\tfrac9{10}\), and false when \(z_j<\tfrac1{10}\). If a clause were false under this assignment, each of its three literal values would be less than \(\tfrac1{10}\). Their sum would be less than \(\tfrac3{10}<\tfrac12\), contradicting its predicate. Hence the assignment satisfies the formula.

Conversely, represent any satisfying assignment by \(z_j\in\{0,1\}\). Exactly one variable predicate holds for every variable, and every clause has literal sum at least one. All \(c\) clause predicates therefore hold. \(\square\)

5.2 Embedding the predicates into legal features and weights

Set \(m=n+1\), indexing coordinates by \(0,1,\ldots,n\). Define
\[ \]
\(W=\{w\in\mathbb R_{\geq0}^{n+1}: \sum_{j=0}^nw_j=1,\ w_j\leq\tfrac1{2n}\text{ for }1\leq j\leq n\}.\)

This uses \(k=n\) additional inequalities and is nonempty. The map
\(z_j=2nw_j\) maps \(W\) onto \([0,1]^n\): for any such \(z\), choose
\[ \]
\(w_j=\tfrac{z_j}{2n}\quad(1\leq j\leq n),\qquad w_0=1-\sum_{j=1}^n\tfrac{z_j}{2n}\geq\tfrac12.\)

Let \(P\) be the least power of two satisfying \(P\geq20(n+1)\), and put \(\rho=1/P\).

The marked type has features \(x^\star=0\) and costs \(C=\mathbf1\). For predicate \(i\), create a rival with features
\[ \]
\((x_i)_0=-\rho b_i,\qquad (x_i)_j=\rho(2na_{ij}-b_i)\quad(1\leq j\leq n).\)

Then, for corresponding \(w,z\),
\[ \]
\(w\cdot x_i=\rho(a_i\cdot z-b_i).\)

Thus rival \(i\) strictly exceeds the unchanged target exactly when its predicate holds.

All initial features satisfy the required bounds, since
\[ \]
\(|(x_i)_j|\leq\rho(6n+\tfrac52) \leq\tfrac{6n+\tfrac52}{20(n+1)}<\tfrac12,\)
and the coordinate-zero bound is smaller.

Give rival \(i\) costs \(C_i=(i+1)\mathbf1\). These costs are positive, and all feature-and-cost types are distinct even if some predicates coincide.

5.3 Masses and a strictly positive budget

Let \(D\) be the least power of two strictly greater than \(N\). Set
\[ \]
\(\mu_i=\tfrac1D\quad(1\leq i\leq N),\qquad \alpha=1-\tfrac ND,\qquad q=\tfrac{n+c}{D},\qquad B=\tfrac{\rho}{32}>0.\)

All masses are positive dyadic rationals and sum to one. The threshold and budget are also dyadic rationals. The support size is \(\tau=N+1\).

For the zero update, exceeding mass is at least \(q\) exactly when at least \(n+c\) predicates hold.

5.4 Correctness, including all feasible updates

If the formula is unsatisfiable, Lemma 3 shows that every \(w\in W\) has at most \(n+c-1\) rivals exceeding the unchanged target. Consequently,
\[ \]
\(\sum_{\substack{i\ne t\\w\cdot x_i>0}}\mu_i \leq\tfrac{n+c-1}{D}<q.\)

The feasible update \(\Delta=0\) succeeds, so the constructed instance is YES.

If the formula is satisfiable, choose its Boolean vector \(z\) and the corresponding \(w\). Exactly \(n\) variable predicates hold, each with value \(a_i\cdot z-b_i=\tfrac1{10}\). Every clause predicate has value at least \(\tfrac12\). Hence at least \(n+c\) rivals have score at least \(\rho/10\).

For every feasible update, the marked cost vector gives
\(\sum_j\Delta_j\leq B\). Therefore
\[ \]
\(w\cdot(x^\star+\Delta)=w\cdot\Delta \leq\sum_j\Delta_j \leq B=\tfrac{\rho}{32}<\tfrac{\rho}{10}.\)

Those \(n+c\) rivals still strictly exceed the updated target. Their mass is at least \(q\), so this weight defeats every feasible update. The constructed instance is NO.

We have proved
\[ \]
\(\text{formula is unsatisfiable} \quad\Longleftrightarrow\quad \text{constructed cohort-update instance is YES}.\)

All constructed rational numbers have polynomial encoding length, and the construction has polynomial size. This establishes \(\mathrm{coNP}\)-hardness, including for \(B>0\). Together with Section 4, it proves \(\mathrm{coNP}\)-completeness.

6. What this establishes about the requested alternatives

Let \(\mathcal D\) denote this decision language.

Because \(\mathcal D\) is \(\mathrm{coNP}\)-complete,
\[ \]
\(\mathcal D\in\mathrm P\quad\Longleftrightarrow\quad \mathrm P=\mathrm{NP}.\)

For the forward implication, polynomial-time decidability of \(\mathcal D\) would imply \(\mathrm{coNP}\subseteq\mathrm P\); taking complements yields \(\mathrm{NP}\subseteq\mathrm P\). The converse follows because \(\mathrm P=\mathrm{NP}\) also implies \(\mathrm P=\mathrm{coNP}\).

Likewise,
\[ \]
\(\mathcal D\text{ is }\mathrm{NP}\text{-hard under many-one reductions} \quad\Longleftrightarrow\quad \mathrm{NP}=\mathrm{coNP}.\)

Indeed, many-one hardness together with \(\mathcal D\in\mathrm{coNP}\) would imply \(\mathrm{NP}\subseteq\mathrm{coNP}\), since \(\mathrm{coNP}\) is closed under polynomial-time many-one preimages. Taking complements gives the reverse inclusion. Conversely, equality of the classes makes \(\mathrm{coNP}\)-completeness imply \(\mathrm{NP}\)-hardness.

Under Turing reductions, hardness is unconditional: construct the instance above, query the cohort-update oracle once, and negate its answer to decide 3SAT.

Thus the exact \(\mathrm{coNP}\)-classification and the fixed-dimension algorithm are fully proved. Under the conventional many-one interpretation, I do not claim an unconditional resolution of the literal “\(\mathrm P\) or \(\mathrm{NP}\)-hard” alternatives.

⟨structured verdict parsed — rendered above⟩

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

Verification report

Verdict: the claimed coNP-completeness and fixed-dimension polynomial-time algorithm are proved. No major or minor mathematical issues were found. The output correctly distinguishes this classification from unconditional NP-hardness under many-one reductions.

The prover’s final "claim": "partial" refers to the literal alternatives in the question. It does not indicate a gap in the coNP-completeness proof.

1. Boundary cases and the mass threshold

Both preliminary cases are correct:

Under the subsequent assumption \(0<q\leq1-\alpha\), the indexing family defining \(h(w)\) is finite and nonempty. Every indexed subset is nonempty, so its minimum score is defined.

Lemma 1 correctly proves both implications. If the target score is below \(h(w)\), a maximizing subset supplies exceeding mass at least \(q\). Conversely, exceeding mass at least \(q\) supplies a finite nonempty subset whose minimum score is strictly above the target score.

The strictness is handled correctly: equality of the target score with \(h(w)\) satisfies the required condition. Thus the halfspaces in update space are closed, and the asserted convexity follows.

Issues: none.

2. Finite reduction to a linear program

Ordering cells and the threshold

The polytopes \(P_\sigma\) cover \(W\), because every finite collection of scores admits a nonincreasing ordering, including ties.

The index \(\ell_\sigma\) exists because total rival mass is at least \(q\). The formula

\(h(w)=w\cdot x_{\sigma(\ell_\sigma)}\)

is valid throughout \(P_\sigma\). The prefix through \(\ell_\sigma\) supplies sufficient mass. Types with strictly larger scores lie within the preceding prefix, whose mass is smaller than \(q\). This reasoning remains valid when the threshold falls within a tied score group.

Vertex enumeration

The list of candidate hyperplanes includes every possible active boundary equation of every \(P_\sigma\):

The rank argument correctly handles lower-dimensional cells. If the simplex equality together with all active equations had rank below \(m\), a nonzero direction would preserve them. Sufficiently small displacements in both directions would also preserve every inactive inequality, contradicting extremality.

Consequently, each vertex is determined by the simplex equality and \(m-1\) listed equations and therefore belongs to \(V\). Duplicate or identically zero score equations do not undermine this argument.

Each nonempty \(P_\sigma\) is bounded because it lies in the simplex. The invoked bounded-polytope theorem applies: it is the convex hull of its vertices. The required score inequality is linear on that cell, so verification at its vertices suffices.

This proves Lemma 2 without enumerating the permutations themselves.

Edge cases

The case \(m=1\) is explicitly covered by the empty hyperplane choice. A singleton or otherwise lower-dimensional \(W\) is covered by the active-equation argument. The case of a single rival introduces no difficulty.

Issues: none.

3. Encoding lengths and running time

The candidate-count bound

\(\lvert V\rvert\leq\binom{H}{m-1}\)

is valid: each chosen system contributes at most one unique solution.

All candidate systems are rational. The stated determinant and Cramer’s-rule bounds give polynomial encoding length for every retained weight. Checking membership in \(W\), sorting exact rational scores, and accumulating rational masses all have polynomial bit complexity in the stated input parameters.

The final LP has rational coefficients and explicitly listed constraints. Standard polynomial-time rational LP feasibility therefore applies to its total encoding length.

The resulting bound

\(\left(\binom{H}{m-1}+1\right)^{O(1)}\operatorname{poly}(m,\tau,k,L)\)

supports the claimed bound

\((\tau^2+k+m)^{O(m)}\operatorname{poly}(L)\).

In particular, it is polynomial for every fixed \(m\). No exponential permutation enumeration is hidden in the algorithm.

Issues: none.

4. Membership in coNP

The application of Helly’s theorem is precise and its hypotheses are satisfied: the family consists of finitely many convex subsets of \(\mathbb R^m\).

The common-point calculation for the score halfspaces is correct. Since each weight is a simplex weight and all initial features lie in the specified cube,

\(h(v)-v\cdot x^\star\leq1=v\cdot\mathbf1\).

Hence every \(K_v\) contains \(\mathbf1\). An empty-intersection subfamily must include \(P_0\), leaving at most \(m\) score halfspaces.

The certificate therefore contains at most \(m\) rational weights, each of polynomial encoding length. Its verification requires only:

All are polynomial-time operations. Soundness correctly does not require verifying that the supplied weights are vertices: any weights in \(W\) yield necessary halfspaces by Lemma 1. Vertex membership is used only to establish the existence of short certificates.

The exceptional case \(q=0\) is directly recognizable. The case \(q>1-\alpha\) contains no NO instances.

Issues: none.

5. Direct hardness reduction

Predicate construction

Lemma 3 is correct. At most one variable predicate holds for each variable, so reaching \(n+c\) satisfied predicates forces one predicate per variable and every clause predicate.

The induced Boolean assignment is well defined. A clause false under that assignment has each literal value strictly below \(1/10\), hence total literal value below \(3/10<1/2\), contradicting its predicate. Conversely, a satisfying Boolean assignment satisfies exactly one variable predicate per variable and every clause predicate.

The argument allows repeated literal occurrences. The coefficient bounds \(\lvert a_{ij}\rvert\leq3\) and \(\lvert b_i\rvert\leq5/2\) are correct.

Weight and feature embedding

The proposed \(W\) is nonempty and maps onto the full cube through \(z_j=2nw_j\). The displayed inverse construction has \(w_0\geq1/2\), so all coordinates are legal.

Substitution into the feature definition confirms

\(w\cdot x_i=\rho(a_i\cdot z-b_i)\).

The feature bound is valid because

\(6n+5/2<10(n+1)\)

for \(n\geq1\). Thus every initial feature lies strictly inside the permitted cube.

The rival costs are positive and pairwise distinct. They also differ from the marked cost vector, so the support types are distinct even when feature vectors coincide.

Masses and budget

The choice \(D>N\) ensures positive marked mass. All rival masses are positive, and the masses sum to one.

The threshold satisfies \(0<q<1\), since \(n+c<N<D\). The construction uses positive dyadic masses, threshold, and budget. The support size is exactly \(N+1\).

Reduction correctness and quantifiers

For an unsatisfiable formula, Lemma 3 bounds the number of exceeding rivals by \(n+c-1\) at every weight. Therefore the zero update succeeds.

For a satisfiable formula, the selected Boolean weight gives at least \(n+c\) rivals score at least \(\rho/10\). Every feasible update satisfies

\(w\cdot\Delta\leq\sum_j\Delta_j\leq\rho/32<\rho/10\).

These rivals therefore strictly exceed the updated target for every feasible update.

The quantifiers are correct: the satisfiable case constructs one weight defeating all feasible updates, which is sufficient to disprove the required existential-update, universal-weight condition.

The construction has polynomial size and polynomial encoding length. It establishes a many-one reduction from 3UNSAT, with strictly positive budget.

Issues: none.

6. Complexity conclusions and cited source

The coNP membership and hardness arguments establish coNP-completeness.

The subsequent consequences are correct:

The claim about the cited paper is accurate: its Theorem 3 states coNP-completeness of the related minimax-value threshold decision problem. The present proof does not rely on transferring that theorem to the cohort problem. [Computing Manipulations of Ranking Systems](https://www.cs.rpi.edu/~magdon/ps/conference/RankingsAAMAS2015.pdf)

The output thus supplies a rigorous complexity classification while correctly explaining why the question’s literal many-one dichotomy requires qualification.

Required repair or clarification: none.

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