Answer: polynomial-time solvable
Theorem 6.5 — class: hardness
Given finitely many types \(T\), masses \(\mu_t\), strengths \(a_t>0\), current payoff rates \(u_t\geq0\), and ordered prizes \(p_1\geq\cdots\geq p_k>0\), does there exist a mass coalition \(d\) with \(0\leq d_t\leq\mu_t\) that, against every partition of the residual mass \(\mu-d\), is guaranteed a prize \(p_j> \sum_t u_t d_t\)?
A coalition is a mass vector \(d\) with \(0\le d_t\le\mu_t\); its strength is \(\sum_t a_td_t\) and its current aggregate payoff is \(\sum_tu_td_t\). A fractional partition of residual mass \(\mu-d\) is a finite family of mass vectors summing coordinatewise to \(\mu-d\). Coalitions are ranked by strength and receive the ordered prizes \(p_1\ge\cdots\ge p_k\).
Target. Given the types, masses, strengths, current payoff rates, and prizes, is deciding whether some coalition \(d\) is guaranteed—against every fractional partition of \(\mu-d\)—a prize \(p_j>\sum_tu_td_t\) NP-hard or in P?
Nearest known results. For finite-player \(k\)-prize weighted voting games, deciding whether a given outcome admits a beneficial single-coalition deviation is NP-hard. No result for the fractional-mass version above was verified.
Assume the standard weighted-voting conventions:
Write
$$ W=\sum_t a_t\mu_t,\qquad S(d)=\sum_t a_td_t,\qquad U(d)=\sum_tu_td_t. $$
The principal case is $W>0$.
For $j\in\{1,\ldots,k\}$, a coalition $d$ is guaranteed to be ranked among the first $j$ coalitions if and only if
$$ (j+1)S(d)>W. $$
The residual mass has total strength
$$ R(d)=\sum_ta_t(\mu_t-d_t)=W-S(d). $$
Under adversarial tie-breaking, $d$ fails to be among the first $j$ precisely when some residual partition contains at least $j$ coalitions whose strengths are each at least $S(d)$.
Suppose first that such coalitions exist. Because every residual coalition has nonnegative strength, their combined strength is at most the total residual strength. Consequently,
$$ R(d)\ge jS(d). $$
Thus, if $R(d)<jS(d)$, no residual partition can place $j$ coalitions weakly ahead of $d$.
Conversely, suppose
$$ R(d)\ge jS(d). $$
Partition the residual mass into the $j$ vectors
$$ x^1=\cdots=x^j=\frac{\mu-d}{j}. $$
This is a valid finite fractional partition, and every part has strength
$$ S(x^\ell)=\frac{R(d)}j\ge S(d). $$
The adversarial ranking may therefore place all $j$ residual coalitions ahead of $d$. Hence $d$ is not guaranteed a top-$j$ rank.
We conclude that the guarantee holds exactly when
$$ R(d)<jS(d). $$
Substituting $R(d)=W-S(d)$ gives
$$ W-S(d)<jS(d), $$
equivalently,
$$ (j+1)S(d)>W. $$
This proves the lemma.
Because $p_1\ge\cdots\ge p_k$, being guaranteed a rank at most $j$ guarantees a prize of value at least $p_j$.
Therefore a beneficial guaranteed deviation exists if and only if, for some $j\in\{1,\ldots,k\}$, there is a vector $d$ satisfying
$$ 0\le d_t\le\mu_t\quad\text{for every }t, $$
$$ (j+1)\sum_ta_td_t>W, $$
and
$$ \sum_tu_td_t<p_j. $$
Thus the universal quantification over all residual partitions has disappeared: fractional divisibility makes total residual strength the only relevant statistic.
For each $j\in\{1,\ldots,k\}$, solve the rational linear program
$$ \begin{aligned} \text{maximize}\quad &\varepsilon\\ \text{subject to}\quad &0\le d_t\le\mu_t &&\text{for every }t,\\ &\varepsilon\le (j+1)\sum_ta_td_t-W,\\ &\varepsilon\le p_j-\sum_tu_td_t. \end{aligned} $$
Let its optimum be $\varepsilon_j^*$.
The box $\prod_t[0,\mu_t]$ is compact, so the two strict inequalities are simultaneously satisfiable exactly when
$$ \varepsilon_j^*>0. $$
Hence the answer is yes if and only if $\varepsilon_j^*>0$ for at least one $j$.
There are $k$ linear programs, each with $|T|+1$ variables and $O(|T|)$ constraints. Rational linear programming and exact comparison of its rational optimum with zero are polynomial-time operations in the binary input length. The entire decision problem is therefore in deterministic polynomial time.
The strict strength inequality is necessary. If
$$ (j+1)S(d)=W, $$
then the residual can be divided into $j$ coalitions of strength exactly $S(d)$, all of which may be placed ahead of $d$.
If ties are instead always resolved in favor of the deviating coalition, the rank condition becomes
$$ (j+1)S(d)\ge W. $$
The problem remains polynomial-time solvable: impose this weak inequality and maximize only the payoff slack $p_j-U(d)$. Thus the complexity classification is unchanged under either standard uniform tie convention, although equality instances can have different answers.
If $W=0$ and empty coalitions are not ranked, then every coalition has strength zero. Any $d\ne\mu$ can be defeated by splitting its nonzero residual mass into $k$ tied coalitions. Only $d=\mu$ can be guaranteed first place, so the answer is yes exactly when
$$ p_1>\sum_tu_t\mu_t. $$
This case is decidable directly. If zero-mass coalitions may themselves be ranked, the model degenerates because arbitrarily many tied zero coalitions can be appended; that convention is normally excluded and is also trivially decidable.
Under the natural binary-rational encoding and pessimistic interpretation of “guaranteed,” the fractional-mass problem is polynomial-time solvable. The finite-player NP-hardness does not transfer: its indivisible subset-selection obstruction is eliminated by the ability to split every residual type proportionally.
⟨structured verdict parsed — rendered above⟩
The prover establishes a sound polynomial-time characterization for the principal case under its added assumptions: binary-rational data, $a_t\ge 0$, indexed fractional partitions, and adversarial tie-breaking.
It does not fully resolve USER_TASK as written because several of those assumptions are absent from the problem statement and materially affect the argument. In particular, the exact-rank lemma is false if negative strength coefficients are permitted. The treatment of zero-strength instances also depends on conventions that the task does not specify.
The prover assumes:
The encoding assumption is necessary to formulate a classical complexity result, but it should be identified as a condition under which the answer is obtained.
More seriously, $a_t\ge0$ is essential to the proof and is not stated in USER_TASK. The proof uses it when concluding that the strength of selected residual parts cannot exceed total residual strength.
Without nonnegativity, the rank lemma is false. For example, let $j=1$, $a=(1,-1)$, $\mu=(3,2)$, and $d=(1,0)$. Then
$$ W=1,\qquad S(d)=1,\qquad 2S(d)>W. $$
Nevertheless, the residual $(2,2)$ can be partitioned as
$$ (1,0)+(1,2), $$
whose strengths are $1$ and $-1$. The first residual coalition ties $d$ and may be placed ahead under adversarial tie-breaking. Thus the stated inequality does not guarantee first place.
This does not contradict the prover’s conditional theorem, since the prover explicitly assumes $a_t\ge0$, but it prevents that theorem from resolving the unrestricted task as written.
For $W>0$ and $a_t\ge0$, this part is correct.
$$
R(d)<jS(d)\iff (j+1)S(d)>W
$$
is correct.
The converse depends on repetitions being allowed in a “family,” which the prover makes explicit by declaring the family indexed.
Under the stated prize-order and tie conventions, this characterization is correct.
Since $p_1\ge\cdots\ge p_k$, guaranteed rank at most $j$ guarantees a prize at least $p_j$. Conversely, the set of ranks carrying a prize strictly exceeding $U(d)$ is an initial segment, so guaranteeing some beneficial prize is equivalent to guaranteeing a top-$j$ rank for some $j$ with $p_j>U(d)$.
No unjustified exchange of quantifiers occurs here.
The LP formulation is correct for the strict inequalities.
For fixed $d$, the largest feasible $\varepsilon$ is the minimum of the strength and payoff slacks. Maximizing this quantity over the compact box gives a positive optimum exactly when some $d$ makes both inequalities strict.
Although $\varepsilon$ has no explicit lower bound, this causes no problem: the objective is bounded above, and maximizing the continuous minimum of the two affine slacks over the compact $d$-box attains an optimum.
With binary-rational input and an explicit prize list, solving $k$ rational LPs and comparing their exact optima with zero is polynomial-time. This standard use of rational linear programming is valid.
The task does not specify how equal strengths are ranked. The prover proves the adversarial-tie version and briefly treats the uniformly favorable-tie version. The favorable condition
$$ (j+1)S(d)\ge W $$
is correct under the stated convention.
However, these two conventions do not constitute a formal definition for the original problem. In particular, the zero-strength cases can have different answers depending on whether ties favor or disfavor the deviating coalition. The output therefore gives conditional classifications rather than a single formally defined answer to USER_TASK.
The minimum clarification needed is an explicit tie-breaking rule, or an explicit statement that “guaranteed” quantifies over all possible tie resolutions.
The literal definition permits zero vectors as partition members unless explicitly prohibited. The prover notices this ambiguity but does not state the resulting decision criterion, saying only that the case is “trivially decidable.” That is insufficiently explicit for a complete decision theorem.
There is also a missing edge case in the branch where empty coalitions are not ranked. The claim that $d=\mu$ is guaranteed first assumes that $d$ itself is nonempty. If $\mu=0$, then $d=\mu=0$ is empty and, under the stated convention that empty coalitions are not ranked, cannot receive first prize. For example, with $\mu=0$ and $p_1>0$, the prover’s displayed test says yes even though there is no rankable coalition.
This is a localized boundary defect and does not affect the polynomial-time result for $W>0$.
The central divisibility insight is rigorous and useful: with nonnegative strengths, an adversary can place $j$ residual coalitions weakly ahead exactly when the residual has at least $jS(d)$ total strength. This removes the finite-player subset-selection obstruction and reduces the main case to rational linear programming.
To make the write-up fully verifiable, the prover must minimally:
⟨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.