← back to the atlas

d4-journals-jet-2025-0075 (d4-journals-jet-2025-0075)

Answer: Polynomial-time solvable, with exact rational output, using at most \(m\) linear programs.

The anchor (named result in the paper)

Corollary 2 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateWith binary weights, the equilibrium distribution can be computed by solving at most m linear programs. 7.2. Egalitarianism for agents While EDR is egalitarian from the point of view of the charities, one could also consider a rule that is egalitarian from the point of view of the agents. The conditional egalitarian rule aims to balance the agents’ utilities without disregarding their approvals. It selects the decomposable distribution that, among all decomposable distributions, maximizes the utility vector by the leximin order, that is: u(δ∗) ⪰lex u(δ) for every decomposable distribution δ.

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

The continuous mirror question, as graded

Given \(m\) charities and a finite support of types \(t\), each with mass \(\mu_t\), nonempty approval set \(A_t\), and per-person contribution \(b_t\), compute the unique per-capita EDR distribution \(\delta\). Find allocations \(x_{t,a}\ge 0\), zero for \(a\notin A_t\), such that \(\sum_{a\in A_t}x_{t,a}=\mu_t b_t\) and \(\delta_a=\sum_t x_{t,a}\); among feasible allocations, \(\delta\) lexicographically maximizes its charity amounts sorted in increasing order. Equivalently, it maximizes \(\sum_t\mu_t b_t\log(\min_{a\in A_t}\delta_a)\). This asks for the high-multiplicity EDR outcome given the paper’s finite-agent characterization, not for equilibrium in a nonatomic best-response game.

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

Let \(A\) be a set of \(m\geq 1\) charities. A society is given by its support: a list of \(\tau\geq 1\) types with positive binary-rational masses \(\mu_t\), where \(\sum_t\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types.
Each type has a nonempty approval set \(A_t\subseteq A\) and a nonnegative binary-rational per-person contribution \(b_t\). Let \(L\) be the total binary input length.
A feasible allocation consists of real amounts \(x_{t,a}\geq 0\), with \(x_{t,a}=0\) for \(a\notin A_t\), \(\sum_{a\in A_t}x_{t,a}=\mu_t b_t\), and \(\delta_a=\sum_t x_{t,a}\). Thus \(\sum_a\delta_a=\sum_t\mu_t b_t\); charity amounts are per capita, not shares of the donated budget.
Define the equilibrium distribution rule (EDR) outcome as the unique feasible charity vector \(\delta\) whose coordinates, sorted increasingly, are lexicographically maximal. Compute this vector exactly and an allocation realizing it; the realizing allocation need not be unique. This definition uses aggregate type budgets, without individual best-response conditions.

Is exact computation of this EDR outcome and a realizing allocation polynomial-time solvable in \(m,\tau,L\), or is it NP-hard?

For finitely listed donors with binary approvals and arbitrary nonnegative contributions, the unique EDR outcome can be computed by solving at most \(m\) linear programs, and it equals the leximin-maximal feasible charity vector. [Brandt, Greger, Segal-Halevi, and Suksompong](https://arxiv.org/abs/2305.10286v4)
That result is formulated for finite donor profiles; no separate complexity result for probability-support input is asserted here.

Modeling choices made when packaging the task

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

Result

Exact computation is polynomial-time solvable in \(m,\tau,L\). Both the unique EDR charity vector and a realizing allocation have polynomial-length rational representations. The following algorithm uses at most \(m\) rational linear programs.

The proof applies directly to the aggregate-budget definition in the question.

1. Aggregate budgets and the feasible set

Define
\[ c_t=\mu_t b_t,\qquad B=\sum_{t=1}^{\tau}c_t, \]
where \(c_t\) is the aggregate budget of type \(t\). Computing these rational numbers requires polynomial time, and their total binary encoding length is polynomial in \(L\).

Let \(E=\{(t,a):a\in A_t\}\). Use allocation variables only for pairs in \(E\). The feasible constraints are
\[ x_{t,a}\geq 0,\qquad \sum_{a\in A_t}x_{t,a}=c_t,\qquad \delta_a=\sum_{t:a\in A_t}x_{t,a}. \]

These constraints have exactly the feasible allocations specified in the question. They also imply \(0\leq x_{t,a}\leq B\) and \(0\leq\delta_a\leq B\).

The feasible set is nonempty: for each type, assign its budget to any one approved charity. It is compact and convex because it is a bounded set defined by linear equalities and inequalities. Its projection onto charity vectors, denoted by \(P\), is therefore also nonempty, compact, and convex.

If \(B=0\), nonnegativity forces every allocation amount and every charity amount to be zero. Henceforth assume \(B>0\).

Equivalently, this is a finite profile with exactly \(\tau\) donors, where donor \(t\) approves \(A_t\) and contributes \(c_t\). This transformation preserves the feasible allocation set exactly. The finite-profile characterization in [Brandt, Greger, Segal-Halevi, and Suksompong, Section 7.1](https://arxiv.org/html/2305.10286v4#S7.SS1) is consistent with this interpretation. We give an explicit algorithm and bit-complexity proof below.

2. Linear representations of the smallest-coordinate sums

For any charity vector \(\delta\), write its coordinates in increasing order as
\[ \delta_{(1)}\leq\cdots\leq\delta_{(m)}. \]
Define
\[ F_k(\delta)=\sum_{i=1}^{k}\delta_{(i)},\qquad k=1,\ldots,m. \]

Lexicographically maximizing \((F_1(\delta),\ldots,F_m(\delta))\) is equivalent to lexicographically maximizing the sorted coordinates. Indeed, if two sorted vectors first differ at position \(r\), their partial sums agree before position \(r\), and the difference between their \(r\)-th partial sums equals the difference between their \(r\)-th coordinates.

We now establish the identity
\[ F_k(\delta)= \max_{0\leq z\leq B} \left(kz-\sum_{a\in A}(z-\delta_a)_+\right), \]
where \(v_+=\max\{v,0\}\).

To prove the upper bound, let \(S\) be a set of \(k\) charities with the smallest amounts. For every \(z\),
\[ kz-\sum_{a\in A}(z-\delta_a)_+ \leq \sum_{a\in S}\left(z-(z-\delta_a)_+\right) = \sum_{a\in S}\min\{z,\delta_a\} \leq F_k(\delta). \]

For equality, take \(z=\delta_{(k)}\), which belongs to \([0,B]\). Let \(r\) be the number of coordinates strictly smaller than \(z\). Then \(r<k\), and
\[ kz-\sum_{a\in A}(z-\delta_a)_+ = \sum_{\delta_a<z}\delta_a+(k-r)z = F_k(\delta). \]
This proves the identity, including when coordinates are tied.

Consequently, the inequality \(s_k\leq F_k(\delta)\) admits a linear formulation using variables \(z_k\) and \(u_{k,a}\):
\[ 0\leq z_k\leq B,\qquad 0\leq u_{k,a}\leq B,\qquad u_{k,a}\geq z_k-\delta_a, \]
\[ s_k\leq kz_k-\sum_{a\in A}u_{k,a}. \]

Every point satisfying these constraints has \(s_k\leq F_k(\delta)\). Conversely, whenever \(s_k\leq F_k(\delta)\), choose
\(z_k=\delta_{(k)}\) and \(u_{k,a}=(z_k-\delta_a)_+\); these choices satisfy all the constraints.

3. The algorithm and its correctness

Construct a single rational polytope \(Q\) with variables
\[ (x,\delta,s,z,u). \]
Its constraints are:

The polytope \(Q\) is nonempty and compact. Its projection onto \((x,\delta,s)\) consists exactly of feasible allocations and vectors satisfying
\[ 0\leq s_k\leq F_k(\delta) \quad\text{for every }k. \]
The witnesses for different values of \(k\) can be chosen independently.

Set \(Q_0=Q\). For \(k=1,\ldots,m\), solve the linear program
\[ \beta_k=\max\{s_k:(x,\delta,s,z,u)\in Q_{k-1}\}, \]
and define
\[ Q_k=Q_{k-1}\cap\{s_k=\beta_k\}. \]
Each maximum exists, and every \(Q_k\) is nonempty and compact.

We prove inductively that the charity-vector projection of \(Q_k\) is exactly
\[ P_k=\{\delta\in P:F_i(\delta)=\beta_i \text{ for }i=1,\ldots,k\}. \]

For \(k=0\), this is the definition of \(P\). Suppose it holds for \(k-1\). For every \(\delta\in P_{k-1}\), the witness construction permits \(s_i=\beta_i\) for \(i<k\) and \(s_k=F_k(\delta)\). Conversely, every point of \(Q_{k-1}\) satisfies \(s_k\leq F_k(\delta)\). Therefore
\[ \beta_k=\max_{\delta\in P_{k-1}}F_k(\delta). \]

If a point belongs to \(Q_k\), its charity vector belongs to \(P_{k-1}\) and satisfies \(F_k(\delta)\geq s_k=\beta_k\). The displayed maximum gives the reverse inequality, so \(F_k(\delta)=\beta_k\). Conversely, any charity vector in \(P_{k-1}\) with \(F_k(\delta)=\beta_k\) has witnesses placing it in \(Q_k\). This completes the induction.

Thus every charity vector projected from \(Q_m\) lexicographically maximizes \((F_1,\ldots,F_m)\), and hence its sorted coordinates. Return an optimal solution of the last linear program. Its \(x\)-coordinates already provide a realizing allocation; set unapproved entries to zero.

4. Uniqueness of the charity vector

For completeness, uniqueness follows from convexity.

The smallest-coordinate sum also satisfies
\[ F_k(\delta)= \min_{\substack{S\subseteq A\\|S|=k}} \sum_{a\in S}\delta_a. \]
It is therefore concave: the minimum of these linear functions satisfies
\[ F_k\!\left(\frac{d+e}{2}\right) \geq\frac{F_k(d)+F_k(e)}2. \]

Suppose two distinct vectors \(d,e\in P\) both have the lexicographically maximal sorted vector. Their partial sums are the same, namely \(\beta_k\). Their midpoint \(w=(d+e)/2\) belongs to \(P\), and
\[ F_k(w)\geq\beta_k \quad\text{for all }k. \]

If any inequality is strict, the first strict inequality makes \(w\) lexicographically better, contradicting maximality. Hence all are equal. Taking consecutive differences shows that \(w,d,e\) have the same sorted coordinates and therefore the same squared Euclidean norm.

But \(d\neq e\) gives
\[ \|w\|_2^2 = \frac{\|d\|_2^2+\|e\|_2^2}{2} -\frac{\|d-e\|_2^2}{4} < \frac{\|d\|_2^2+\|e\|_2^2}{2}, \]
a contradiction. Thus the algorithm returns the unique EDR charity vector.

5. Exact polynomial bit complexity

It remains to justify exact computation, including the sizes of intermediate optimum values.

The polytope \(Q\) has
\[ N=|E|+m^2+3m \]
variables and \(O(|E|+\tau+m^2)\) constraints. Since \(|E|\leq m\tau\), these quantities are polynomial in \(m,\tau\). All coefficients and right-hand sides have polynomial binary encoding length in \(m,\tau,L\).

After clearing denominators separately in each constraint, let \(H\) bound the bit length of each resulting integer coefficient and right-hand side. Such an \(H\) is polynomial in \(m,\tau,L\).

At any vertex of \(Q\), choose \(N\) linearly independent active constraints. They determine the vertex through a nonsingular integer system. Cramer’s rule expresses each coordinate as a ratio of determinants. Expanding a determinant gives the bound
\[ |\det M|\leq N!\,2^{NH}. \]
The same bound applies to the numerator determinants. Hence every vertex coordinate has encoding length
\[ O\!\left(N(H+\log N)\right), \]
which is polynomial in the input parameters.

Crucially, this bound applies uniformly throughout the algorithm. Maximizing a linear objective over a polytope selects a face, and a face of a face is a face of the original polytope. Therefore each \(Q_k\) is a nonempty face of \(Q\), and each of its vertices is a vertex of \(Q\). Since \(\beta_k\) is the \(s_k\)-coordinate of an optimal vertex of \(Q_{k-1}\), every \(\beta_k\) has the uniform polynomial encoding bound above. Adding the equalities \(s_k=\beta_k\) cannot cause uncontrolled bit-length growth.

We now apply the standard exact rational linear-programming theorem: an explicitly encoded rational linear program can be solved, with an exact rational optimum and optimal solution, in time polynomial in its encoding length. Its hypotheses hold at every stage because the program is rational, nonempty, bounded, and of polynomial encoding length. An optimal vertex can be returned, giving the same polynomial bound for the final allocation.

There are at most \(m\) such programs. Thus the entire computation, including writing the charity vector and all allocation entries, takes polynomial time in \(m,\tau,L\).

⟨structured verdict parsed — rendered above⟩

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

The prover resolves the task correctly. The argument establishes exact polynomial-time computation of both the unique EDR charity vector and a realizing allocation. I found no major or minor mathematical issues.

The replacement \(c_t=\mu_t b_t\) preserves precisely the budgets required by the task. Multiplication and summation of explicitly encoded binary rationals have polynomial bit complexity; no expansion into individual members of the population is required.

The allocation constraints match the task exactly. Nonnegativity and total budget \(B\) imply the stated bounds on allocation entries and charity amounts. Nonempty approval sets guarantee feasibility, including for zero-budget types. The feasible set is closed, bounded, and convex, so its charity-vector projection \(P\) is nonempty, compact, and convex.

The case \(B=0\) is handled correctly: every allocation entry and charity amount must be zero.

The finite-profile interpretation is consistent with the cited paper’s decomposability constraints and leximin characterization. However, the subsequent argument establishes correctness independently of that characterization. [Section 7.1 of the cited paper](https://arxiv.org/html/2305.10286v4#S7.SS1)

The equivalence between lexicographically maximizing sorted coordinates and their partial sums is correct: the first differing coordinate produces the first differing partial sum, with the same sign.

The displayed identity for \(F_k\) is valid on the relevant domain \(0\leq\delta_a\leq B\). The upper-bound argument correctly discards nonnegative penalty terms outside the chosen set \(S\). Choosing \(z=\delta_{(k)}\) attains equality. Counting only coordinates strictly below \(z\) handles ties correctly, including \(k=1\) and \(k=m\).

The auxiliary constraints express exactly the claimed existential condition \(s_k\leq F_k(\delta)\). In one direction, \(u_{k,a}\geq(z_k-\delta_a)_+\) makes the linear expression at most \(F_k(\delta)\). In the other direction, the supplied witnesses attain \(F_k(\delta)\) and satisfy \(0\leq u_{k,a}\leq B\).

The bounds on all variables make \(Q\) compact. Its claimed projection is correct: feasible charity amounts are nonnegative, and witnesses for different indices \(k\) are independent. The upper bound \(s_k\leq mB\) does not exclude any relevant partial sum.

The induction identifying the charity-vector projection of \(Q_k\) with \(P_k\) is sound. In particular, it addresses the potentially problematic distinction between fixing \(s_i\) and fixing \(F_i(\delta)\). At each stage, the previous maximum and the inequality \(s_i\leq F_i(\delta)\) force equality on the projected feasible set.

Consequently, \(\beta_k\) is exactly the maximum of \(F_k\) subject to the earlier optimal partial sums. The final optimal solution belongs to \(Q_m\), and its charity vector is leximin maximal. Its allocation coordinates already satisfy every realization constraint. Setting omitted, unapproved entries to zero is correct.

The subset-minimum representation of \(F_k\) is correct and implies the stated concavity inequality.

For two leximin-maximal vectors, their midpoint is feasible and has every partial sum at least the optimal value. A first strict inequality would contradict lexicographic maximality. Equality of all partial sums therefore gives equality of the sorted coordinate vectors and squared norms.

The squared-norm identity is correct, with the factor \(1/4\). Its strict inequality for distinct vectors contradicts equality of those norms. This establishes uniqueness of the labeled charity vector, rather than merely uniqueness of its sorted coordinates.

The variable count \(N=|E|+m^2+3m\) and constraint count are correct. The explicit LP description has polynomial length because \(|E|\leq m\tau\), and the derived rational budgets have polynomial encoding length.

Clearing denominators separately in each constraint gives integer coefficients of polynomial bit length. The active-constraint argument applies also when \(Q\) has lower affine dimension. The determinant bound \(N!\,2^{NH}\) is valid for both denominator and numerator determinants, yielding the claimed polynomial coordinate-length bound.

The uniform bound on intermediate values is justified: every \(Q_k\) is an optimal face of \(Q_{k-1}\), hence a face of \(Q\). Its vertices are vertices of \(Q\), so every \(\beta_k\) inherits the original polynomial bound. This avoids an unsupported assumption about repeated rational arithmetic remaining small.

The exact rational LP theorem is stated sufficiently precisely for its application here. Every program is explicitly encoded, rational, nonempty, bounded, and of polynomial encoding length. Polynomial-time exact optimization, including an optimal vertex, therefore supplies the required rational outputs. There are at most \(m\) programs, and writing all allocation entries also takes polynomial time.

The proof addresses the supplied support representation and aggregate-budget definition directly. It does not assume equal contributions, positive contributions, individual best responses, or an explicitly expanded population.

Zero-budget types, unsupported charities, tied amounts, and \(m=1\) are covered by the argument. No additional lemma, clarification, or repair 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.