Answer: Solvable in time polynomial in \(m,\tau,L\).
Theorem O.3 — class: hardness
Given an explicit alternative set \(\mathcal A\), rational type masses \(\mu_t>0\) summing to \(1\), rational valuations \(v_t(A)\), and a disagreement alternative \(D\), compute the lexicographically maximal ascending utility quantile among per-type utilities \(u_t\) satisfying \(\sum_t\mu_tu_t=B=\max_{A\in\mathcal A}\sum_t\mu_tv_t(A)\), \(u_t\ge v_t(D)\), and \(\sum_t x_tu_t\le\max_{A\in\mathcal A}\sum_t x_tv_t(A)\) for every \(x\in\prod_t[0,\mu_t]\), where \(B\) is maximum welfare. The selected alternative must attain \(B\), and transfers \(p_t=u_t-v_t(A^*)\) must balance in mass.
A society is given by its support: the list of the \(\tau\ge1\) types with positive masses \(\mu_t\in\mathbb Q_{>0}\), encoded in binary and summing to \(1\). Here \(\tau\) is the support size, not the number of possible types.
The input also gives an explicit nonempty alternative set \(\mathcal A\), with \(m=|\mathcal A|\), a disagreement alternative \(D\in\mathcal A\), and valuations \(v_t(A)\in\mathbb Q\) of either sign; \(L\) is the total binary input length.
Each type receives a common utility \(u_t\in\mathbb R\). Define \(B=\max_{A\in\mathcal A}\sum_t\mu_tv_t(A)\). Feasibility requires \(\sum_t\mu_tu_t=B\), \(u_t\ge v_t(D)\), and \(\sum_tx_tu_t\le\max_{A\in\mathcal A}\sum_tx_tv_t(A)\) for every \(x\in\prod_t[0,\mu_t]\); coalitions may contain any fraction of each type.
Normalize disagreement utilities before the fairness comparison: let \(g_t=u_t-v_t(D)\). The ascending mass quantile is \(Q_g(q)=\min\{z:\sum_{t:g_t\le z}\mu_t>q\}\) for \(q\in[0,1)\). Compare two such step functions on their common breakpoint partition, preferring the larger value on the first interval where they differ.
The computational problem is to report infeasibility or compute an exact feasible utility vector maximizing this quantile lexicographically, together with any \(A^*\) attaining \(B\) and unrestricted signed transfers \(p_t=u_t-v_t(A^*)\), satisfying \(\sum_t\mu_tp_t=0\).
Is this computational problem solvable in time polynomial in \(m,\tau,L\), or is it NP-hard?
For finite societies, computing the corresponding disagreement-normalized lexicographic welfare-sharing solution is NP-hard even with polynomially many explicit alternatives and a deterministic disagreement alternative; submodularity of coalition maximum welfare permits a strongly polynomial algorithm. [Discrete results](https://arxiv.org/pdf/1909.11346)
No complexity result for exactly the mass formulation above was located in the literature search.
Result. The problem is solvable in time polynomial in \(m,\tau,L\). Fractional coalitions yield a polynomial-size description of the feasible set, and successive linear programs compute its unique lexicographically maximal mass quantile.
1. Fractional coalitions characterize the feasible utility vectors
Write \(v^A=(v_t(A))_{t=1}^{\tau}\), \(\mu=(\mu_t)_{t=1}^{\tau}\), and let
\(\mathcal O=\{A\in\mathcal A:\mu\cdot v^A=B\}\).
This set is nonempty and can be computed by exact rational arithmetic.
We first prove the characterization
\[
\text{feasible utilities}
=
\operatorname{conv}\{v^A:A\in\mathcal O\}
\cap\{u:u_t\ge v_t(D)\text{ for every }t\}.
\]
Here and below, an equation displayed on its own line is understood with the same mathematical delimiters as the surrounding text.
More explicitly, the claimed equality is
\(\mathcal U=\operatorname{conv}\{v^A:A\in\mathcal O\}\cap\{u:u_t\ge v_t(D)\ \forall t\}\).
For necessity, suppose \(u\) satisfies efficiency and every fractional-coalition inequality. Fix an arbitrary direction \(h\in\mathbb R^\tau\), and consider
\(x(\varepsilon)=\mu/2+\varepsilon h\).
Because every \(\mu_t\) is positive, \(x(\varepsilon)\) lies in \(\prod_t[0,\mu_t]\) for sufficiently small positive \(\varepsilon\). At \(\varepsilon=0\), every alternative in \(\mathcal O\) has coalition welfare \(B/2\), whereas every alternative outside \(\mathcal O\) has strictly smaller welfare. Since there are finitely many alternatives, these strict inequalities persist for sufficiently small positive \(\varepsilon\). Consequently,
\(\max_{A\in\mathcal A}x(\varepsilon)\cdot v^A=B/2+\varepsilon\max_{A\in\mathcal O}h\cdot v^A\).
The coalition inequality and \(\mu\cdot u=B\) give
\(B/2+\varepsilon h\cdot u\le B/2+\varepsilon\max_{A\in\mathcal O}h\cdot v^A\).
Subtracting \(B/2\) and dividing by \(\varepsilon\) yields
\(h\cdot u\le\max_{A\in\mathcal O}h\cdot v^A\).
This holds for every \(h\in\mathbb R^\tau\). The convex hull of the finitely many vectors \(v^A\), \(A\in\mathcal O\), is compact and convex. If \(u\) were outside it, the strict separation theorem would supply a direction \(h\) violating the preceding inequality. Thus \(u\) belongs to that convex hull. Disagreement domination supplies the remaining inequalities in the characterization.
For sufficiency, suppose
\(u=\sum_{A\in\mathcal O}\theta_Av^A\),
where \(\theta_A\ge0\) and \(\sum_A\theta_A=1\), and suppose \(u_t\ge v_t(D)\). Then
\(\mu\cdot u=\sum_A\theta_A B=B\).
For every coalition \(x\),
\(x\cdot u=\sum_A\theta_A(x\cdot v^A)\le\max_{A\in\mathcal A}x\cdot v^A\).
All feasibility requirements therefore hold.
2. A polynomial-size feasibility formulation
Define \(d_t=v_t(D)\) and \(s_t(A)=v_t(A)-d_t\). By the characterization above, the feasible gain vectors form
\(\mathcal P=\operatorname{conv}\{s(A):A\in\mathcal O\}\cap\mathbb R^\tau_{\ge0}\).
In particular, feasibility is exactly the feasibility of the following rational linear system:
It has at most \(m+\tau\) variables and polynomially many constraints, with coefficients of polynomial binary encoding length. Exact rational linear programming therefore decides feasibility in polynomial time.
If this system is infeasible, the algorithm reports infeasibility. Otherwise, \(\mathcal P\) is a nonempty compact convex polytope.
3. Successive minimum-gain optimization
We now give an algorithm for any nonempty compact convex polytope \(\mathcal P\subseteq\mathbb R^\tau_{\ge0}\) with the preceding explicit formulation.
Initially, put \(C_0=\mathcal P\) and \(R_0=\{1,\ldots,\tau\}\). The set \(R_j\) will contain the types whose gains have not yet been fixed.
At stage \(j\), provided \(R_{j-1}\ne\varnothing\), compute
\(\ell_j=\max_{g\in C_{j-1}}\min_{t\in R_{j-1}}g_t\).
This is a linear program: maximize \(z\), subject to \(g\in C_{j-1}\) and \(g_t\ge z\) for every \(t\in R_{j-1}\). Compactness ensures attainment. Define
\(C_j=\{g\in C_{j-1}:g_t\ge\ell_j\ \forall t\in R_{j-1}\}\)
and
\(I_j=\{t\in R_{j-1}:g_t=\ell_j\text{ for every }g\in C_j\}\).
Each membership test for \(I_j\) is another linear program: maximize \(g_t\) over \(C_j\). Since every such gain is at least \(\ell_j\), the type belongs to \(I_j\) exactly when this maximum equals \(\ell_j\).
We claim that \(I_j\) is nonempty. Otherwise, for every \(t\in R_{j-1}\), there would be a point \(g^{(t)}\in C_j\) with \(g^{(t)}_t>\ell_j\). Their average belongs to \(C_j\) by convexity. For each remaining coordinate, every summand is at least \(\ell_j\) and one is strictly larger. Hence the average has every remaining gain strictly larger than \(\ell_j\), contradicting its definition.
Fix the gains of types in \(I_j\) at \(\ell_j\), and put \(R_j=R_{j-1}\setminus I_j\). At least one type is removed at every stage, so the process stops after at most \(\tau\) stages. Its final set \(C_K\) contains exactly one gain vector, denoted \(\widehat g\): every coordinate has been fixed.
The successive levels are strictly increasing whenever another stage exists. Indeed, for every \(t\in R_j\), its exclusion from \(I_j\) supplies a point of \(C_j\) with \(g_t>\ell_j\). Averaging these points gives a point with every coordinate in \(R_j\) strictly above \(\ell_j\). Thus \(\ell_{j+1}>\ell_j\).
4. Proof of optimality for the mass quantile
Let \(g\in\mathcal P\) differ from \(\widehat g\). Since \(C_K=\{\widehat g\}\), there is a first stage \(j\) for which
\(g\in C_{j-1}\) but \(g\notin C_j\).
Set
\(r=\min_{t\in R_{j-1}}g_t\).
Then \(r<\ell_j\).
Let \(F=I_1\cup\cdots\cup I_{j-1}\), and let \(M=\sum_{t\in F}\mu_t\). The gains of every type in \(F\) agree between \(g\) and \(\widehat g\).
If \(j>1\), membership in \(C_{j-1}\) also implies \(r\ge\ell_{j-1}\). Thus every gain of a type in \(F\) is at most \(r\). Meanwhile, every type outside \(F\) has gain at least \(r\) under \(g\) and at least \(\ell_j\) under \(\widehat g\).
It follows that the two quantile functions agree for \(q<M\). To justify the possible boundary tie: additional remaining types can have gain \(\ell_{j-1}\) under \(g\), but they merely extend the last already fixed plateau; they cannot change a quantile value before the total fixed mass \(M\).
At \(q=M\), the strict inequality in the quantile definition gives
\(Q_g(M)=r\) and \(Q_{\widehat g}(M)=\ell_j\).
For the first equality, the fixed types contribute mass \(M\), and the remaining types attaining \(r\) contribute additional positive mass. For the second, the nonempty set \(I_j\) contributes positive mass at \(\ell_j\). Also \(M<1\), because \(R_{j-1}\ne\varnothing\).
Both functions are finite step functions, so these unequal values persist on a nonempty interval beginning at \(M\). Hence their first differing interval favors \(\widehat g\), since \(\ell_j>r\).
Therefore \(\widehat g\) strictly defeats every distinct feasible gain vector under the specified mass-quantile comparison. It is the unique maximizer. The argument uses positivity of the masses, without expanding them into individual agents.
5. Polynomial bit complexity
The algorithm uses at most \(\tau\) stage linear programs and at most \(\tau(\tau+1)/2\) coordinate tests. We must additionally bound the encoding lengths of the recursively computed levels.
Let
\(H=\max\bigl(\{0\}\cup\{s_t(A):t=1,\ldots,\tau,\ A\in\mathcal O\}\bigr)\).
Every feasible gain and every computed level lies in \([0,H]\).
For any stage \(j\), consider a single auxiliary polytope with variables \(\theta,g,h_1,\ldots,h_j\). Include the original feasibility formulation and add:
This is a nonempty bounded rational polytope with polynomially many variables and constraints. Its coefficients come from the original formulation, \(H\), and the integers \(0,1,-1\). In particular, its description does not contain any previously computed level.
Sequentially maximizing \(h_1,\ldots,h_j\) over this polytope gives precisely \(\ell_1,\ldots,\ell_j\). Here is the verification. Once \(h_1,\ldots,h_{k-1}\) equal their computed levels, the constraints place \(g\) in \(C_{k-1}\) and require every type in \(R_{k-1}\) to have gain at least \(h_k\). Therefore \(h_k\le\ell_k\). Conversely, any point of \(C_j\), together with \(h_k=\ell_k\), satisfies all auxiliary constraints. Thus every bound is attained.
Each sequential maximization selects a nonempty face of the preceding face. The final face contains a vertex of the auxiliary polytope, whose \(h\)-coordinates are the computed levels. Standard determinant bounds for vertices of rational polytopes consequently give polynomial binary encoding length for every \(\ell_k\), uniformly in \(j\).
All linear programs actually solved by the algorithm therefore have polynomial encoding length. The polynomial-time theorem for rational linear programming applies: feasibility, exact bounded optima, and exact rational feasible points can all be computed in time polynomial in their encoded descriptions. Together with the polynomial number of calls, this proves polynomial running time in \(m,\tau,L\).
6. Utilities, transfers, and the discrete distinction
Return \(u_t=d_t+\widehat g_t\). Choose any \(A^*\in\mathcal O\), and set \(p_t=u_t-v_t(A^*)\). These are exact rational outputs of polynomial encoding length. Their budget balance follows from
\(\sum_t\mu_tp_t=\mu\cdot u-\mu\cdot v^{A^*}=B-B=0\).
The discrete hardness result concerns coalitions consisting of subsets of whole agents; see [Babaioff and Feige, Theorem O.3](https://arxiv.org/pdf/1909.11346). The decisive additional condition here is the availability of every sufficiently small perturbation of the interior coalition \(\mu/2\). It forces efficient utilities into the convex hull of welfare-maximizing valuation vectors, producing the polynomial-size formulation above.
⟨structured verdict parsed — rendered above⟩
The argument establishes the claimed polynomial-time result. I found no false step or major gap. There is one minor omission: the bit-complexity argument invokes determinant bounds without stating the quantitative theorem being used.
The necessity argument is valid.
The sufficiency argument is also valid. A convex combination of maximizing valuation vectors has total welfare \(B\), and its welfare for any coalition cannot exceed the maximum coalition welfare. Disagreement domination is imposed separately.
Signed valuations cause no difficulty in either direction. The characterization does not assume nonnegative valuations or expand rational masses into individual agents.
Finding: Correct.
Translating utilities by the disagreement vector correctly gives
\(\mathcal P=\operatorname{conv}\{s(A):A\in\mathcal O\}\cap\mathbb R^\tau_{\ge0}\).
The formulation has the claimed polynomial size. Computing weighted welfare totals, identifying \(\mathcal O\), and subtracting disagreement valuations all require only polynomial-length rational arithmetic. The convex hull is compact, and intersection with the closed nonnegative orthant preserves compactness.
The algorithm explicitly checks feasibility before beginning the optimization stages. Thus it does not silently assume that disagreement domination is achievable.
Finding: Correct.
Every optimization stage is well-defined:
The coordinate-maximization tests correctly identify \(I_j\), because each tested coordinate is already bounded below by \(\ell_j\) throughout \(C_j\).
The averaging argument proving that \(I_j\) is nonempty is valid. If every remaining coordinate could exceed \(\ell_j\) somewhere in \(C_j\), averaging the finitely many witness points would make all remaining coordinates exceed \(\ell_j\) simultaneously, contradicting its optimality.
The analogous averaging argument correctly establishes strict increase of successive levels when coordinates remain.
Termination and uniqueness of the final vector follow as written: at least one coordinate is removed per stage, and each removed coordinate is constant throughout the corresponding set and every subsequent subset. Once all coordinates are removed, the nonempty final set is a singleton.
Finding: Correct.
This section addresses the actual weighted quantile objective, rather than merely asserting that ordinary coordinate leximin suffices.
For any distinct feasible vector, the first stage it fails exists because the final nested set is a singleton. At that stage, its minimum remaining gain \(r\) is strictly below \(\ell_j\).
The comparison before and at the fixed mass \(M\) is correct:
There is no endpoint problem: remaining types exist at this stage, so positivity of their masses implies \(M<1\). Finitely many positive masses also ensure that the differing values persist on an interval of positive length.
Consequently, the first differing interval favors \(\widehat g\). The proof establishes strict superiority over every distinct feasible vector, including vectors that might otherwise have the same weighted distribution.
Finding: Correct. The masses need not be equal.
The number of linear-programming calls is correctly bounded. The sizes of the remaining coordinate sets decrease by at least one per stage, giving the stated triangular bound on coordinate tests.
The auxiliary-polytope construction avoids inserting recursively computed levels into its coefficients. Its claimed properties hold:
The sequential-maximization argument is valid. At an intermediate maximization of \(h_k\), coordinates assigned to later fixed groups equal later level variables, and those variables are at least \(h_k\). Coordinates still remaining are bounded below by \(h_j\), hence also by \(h_k\). Thus all coordinates in \(R_{k-1}\) satisfy the required lower bound. Earlier groups already have their computed values.
The successive maximizing sets are nonempty faces. Their final face contains a vertex of the original auxiliary polytope, so the computed levels occur among that vertex’s coordinates. This is the appropriate argument for controlling their encoding lengths uniformly.
Minor issue: “Standard determinant bounds for vertices of rational polytopes” is not stated quantitatively. Under the requested strict standard for invoked theorems, the write-up should specify the bound it uses and identify its dimension and coefficient-length parameters.
Minimum clarification: State a precise rational-vertex encoding bound and explicitly note that its parameters are polynomially bounded for the auxiliary formulation. This is a routine expositional addition; it requires no new mathematical argument.
The rational linear-programming theorem is otherwise stated with the capabilities needed here: polynomial-time feasibility testing, exact bounded optimal values, and exact rational feasible points. The formulated programs satisfy those conditions.
The returned utilities have the required disagreement-normalized gains. Choosing any member of \(\mathcal O\) supplies a welfare-maximizing alternative. The signed transfers satisfy the required identity and mass-weighted budget balance exactly. Their rational encoding lengths follow from the preceding bounds.
The discrete citation is accurate: Theorem O.3 concerns finitely many agents, polynomially many alternatives, and a designated disagreement alternative; its hardness statement does not concern the fractional-coalition formulation audited here. [Babaioff and Feige, Theorem O.3](https://arxiv.org/pdf/1909.11346)
The argument also covers the permitted edge cases, including a single type, a single alternative, and zero feasible gains. None requires an additional substantive argument.
The prover resolves the assigned computational problem in substance. The feasible-set characterization, weighted-quantile optimality, and polynomial-time algorithm are sound. The only requested repair is to make the invoked rational-vertex encoding bound explicit.
⟨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.