← back to the atlas

Fair Division of Chores with Budget Constraints (d4-conf-sagt-2024-0013)

Answer: Polynomial-time solvable in \(m=r\), \(\tau\), and \(L\); an envy-free allocation always exists under the unrestricted residual-support condition.

The anchor (named result in the paper)

Theorem 9 — class: algorithmic

The continuous mirror question, as graded

Given budget types \(b\in[\tau]\) with masses \(\mu_b>0\), budgets \(B_b\), and divisible chore types \(k\in[r]\) with per-capita supplies \(q_k\), find per-agent bundles \(X_b=(X_{b,k})_{k\in[r]}\) and residual supplies \(R_k=q_k-\sum_b\mu_bX_{b,k}\ge0\) such that \(\sum_k s_kX_{b,k}\le B_b\), every \(Y\le X_b\) with \(\sum_k s_kY_k\le B_{b'}\) satisfies \(\sum_k d_kY_k\le\sum_k d_kX_{b'}\), and every finite \(Y\) supported on \(\{k:R_k>0\}\) with size at most \(B_{b'}\) satisfies the same inequality; find such an allocation in time polynomial in \(\tau\), \(r\), and the encoding length.

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

A society is given by its support: the list of \(\tau\geq1\) budget types with positive masses \(\mu_b\), each mass a binary rational; \(\tau\) is the support size, not the number of possible types. Normalize \(\sum_b\mu_b=1\).
There are \(m=r\geq1\) divisible chore types, with per-capita supplies \(q_k>0\), objective unit sizes \(s_k>0\), objective unit disutilities \(d_k\geq0\), and budgets \(B_b>0\). All input numbers are binary rationals; \(L\) is their total encoding length.
For a nonnegative quantity vector \(Z\in\mathbb R_{\geq0}^r\), write \(s(Z)=\sum_k s_kZ_k\) and \(d(Z)=\sum_k d_kZ_k\); vector inequalities are componentwise.
An allocation gives every agent of type \(b\) the same bundle \(X_b\in\mathbb R_{\geq0}^r\), with \(s(X_b)\leq B_b\), and assigns residual supplies \(R_k=q_k-\sum_b\mu_bX_{b,k}\geq0\) to a housekeeper.
Envy-freeness requires, for every pair \(b,b'\), that every \(0\leq Y\leq X_b\) with \(s(Y)\leq B_{b'}\) satisfies \(d(Y)\leq d(X_{b'})\).
It also requires, for every \(b'\), that every finite vector \(Y\in\mathbb R_{\geq0}^r\) with \(Y_k=0\) whenever \(R_k=0\) and \(s(Y)\leq B_{b'}\) satisfies \(d(Y)\leq d(X_{b'})\); these test vectors have no coordinatewise bound by \(R\).

Is finding such an envy-free allocation solvable in time polynomial in \(m=r\), \(\tau\), and \(L\), or is this computational problem NP-hard?

For a finite list of agents and divisible chores, an envy-free allocation always exists and is polynomial-time computable, with housekeeper comparisons restricted to subbundles of its actual residual bundle ([Elkind–Igarashi–Teh](https://arxiv.org/html/2410.23979v1)).
No result settling the distribution-over-budget-types problem with the residual-support condition above was located.

Modeling choices made when packaging the task

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

Polynomial-time solvability

The problem is polynomial-time solvable in \(m=r\), \(\tau\), and \(L\). An envy-free allocation always exists, including under the unrestricted residual-support condition.

The construction below uses the common size and disutility functions directly. It does not require extending the finite-agent theorem of [Elkind–Igarashi–Teh](https://arxiv.org/html/2410.23979v1).

1. Size coordinates and density order

Define the density and total available size of chore \(k\) by

\[ \rho_k=\frac{d_k}{s_k}, \qquad Q_k=s_kq_k. \]

Relabel chores so that \(\rho_1\geq\cdots\geq\rho_m\), breaking ties arbitrarily. For a bundle \(X_b\), let \(v_{b,k}=s_kX_{b,k}\) denote its size in coordinate \(k\). Thus its total size and disutility are respectively \(\sum_kv_{b,k}\) and \(\sum_k\rho_kv_{b,k}\).

Let \(B_{\max}=\max_bB_b\), and define

\[ F(t)=\sum_b\mu_b\min\{B_b,t\}, \qquad H=F(B_{\max})=\sum_b\mu_bB_b. \]

The function \(F\) is continuous and strictly increasing on \([0,B_{\max}]\). Indeed, if \(0\leq t<t'\leq B_{\max}\), every summand is nondecreasing, and any type with budget \(B_{\max}\) contributes the strictly positive increment \(\mu_b(t'-t)\). Consequently, every \(u\in[0,H]\) has a unique inverse value \(F^{-1}(u)\) in this interval.

2. Construction and feasibility

Set \(C_0=0\), and, for \(k\in\{1,\ldots,m\}\), define

\[ C_k=\sum_{j=1}^kQ_j, \qquad u_k=\min\{C_k,H\}, \qquad t_k=F^{-1}(u_k). \]

Also set \(u_0=t_0=0\). Allocate

\[ v_{b,k} = \min\{B_b,t_k\}-\min\{B_b,t_{k-1}\}, \qquad X_{b,k}=\frac{v_{b,k}}{s_k}. \]

Since the sequence \(t_k\) is nondecreasing, all allocated quantities are nonnegative. Telescoping gives, for every prefix \(k\),

\[ \sum_{j=1}^kv_{b,j}=\min\{B_b,t_k\}. \]

In particular, \(s(X_b)=\min\{B_b,t_m\}\leq B_b\).

The aggregate allocated size of chore \(k\) is

\[ \sum_b\mu_bv_{b,k} = F(t_k)-F(t_{k-1}) = u_k-u_{k-1}. \]

This increment lies between \(0\) and \(Q_k\): if \(C_{k-1}\geq H\), it is zero; otherwise it equals \(\min\{Q_k,H-C_{k-1}\}\). Dividing by \(s_k>0\) proves \(\sum_b\mu_bX_{b,k}\leq q_k\). Hence the construction is feasible.

3. Envy-freeness between budget types

Fix any source type \(b\), comparison type \(c\), and test vector \(0\leq Y\leq X_b\) satisfying \(s(Y)\leq B_c\).

Write \(w_k=s_kY_k\), and define the cumulative sizes

\[ W_k=\sum_{j=1}^kw_j, \qquad V_k=\sum_{j=1}^kv_{c,j}=\min\{B_c,t_k\}. \]

Because \(Y\leq X_b\),

\[ W_k\leq\sum_{j=1}^kv_{b,j} =\min\{B_b,t_k\}\leq t_k. \]

Also, nonnegativity and the test budget imply \(W_k\leq s(Y)\leq B_c\). Combining these bounds gives \(W_k\leq V_k\) for every \(k\).

Summation by parts yields

\[ d(Y) = \sum_{k=1}^m\rho_kw_k = \rho_mW_m+ \sum_{k=1}^{m-1}(\rho_k-\rho_{k+1})W_k. \]

The identity follows by substituting \(w_k=W_k-W_{k-1}\), with \(W_0=0\), and collecting terms. Every coefficient on the right is nonnegative, since the densities are nonnegative and nonincreasing. Therefore,

\[ d(Y) \leq \rho_mV_m+ \sum_{k=1}^{m-1}(\rho_k-\rho_{k+1})V_k = \sum_{k=1}^m\rho_kv_{c,k} = d(X_c). \]

This proves every required comparison between budget types. For \(m=1\), the displayed sums with upper limit \(m-1\) are empty, and the argument remains valid.

4. The unrestricted residual-support condition

Let \(R_k=q_k-\sum_b\mu_bX_{b,k}\). From the aggregate allocation formula,

\[ \sum_{k=1}^ms_kR_k = C_m-u_m = \max\{C_m-H,0\}. \]

If \(R=0\), the support condition forces every housekeeper test vector to be zero, so all comparisons hold.

Suppose instead that some residual coordinate is positive. Since all \(s_k>0\), the preceding identity implies \(C_m>H\). Let

\[ h=\min\{k:C_k>H\}. \]

For \(k<h\), both \(C_{k-1}\) and \(C_k\) are at most \(H\), so chore \(k\) is fully allocated. Thus every residual-supported coordinate has index at least \(h\), and consequently density at most \(\rho_h\).

On the other hand, \(u_h=H\), so \(t_h=B_{\max}\). For every \(k>h\), both \(t_k\) and \(t_{k-1}\) equal \(B_{\max}\), giving \(v_{b,k}=0\). Every bundle therefore uses only coordinates with density at least \(\rho_h\). Moreover, every budget is filled:

\[ s(X_b)=\min\{B_b,t_m\}=B_b. \]

It follows that

\[ d(X_b)=\sum_{k=1}^h\rho_kv_{b,k} \geq \rho_h\sum_{k=1}^hv_{b,k} = \rho_hB_b. \]

Now fix any comparison type \(b\) and any finite nonnegative vector \(Y\) supported on the residual coordinates with \(s(Y)\leq B_b\). Every coordinate used by \(Y\) has density at most \(\rho_h\), so

\[ d(Y)\leq\rho_hs(Y)\leq\rho_hB_b\leq d(X_b). \]

This argument imposes no coordinatewise bound by \(R\), and therefore proves exactly the stronger housekeeper condition in the question.

5. Exact polynomial-time computation

It remains to verify that the construction has polynomial bit complexity.

Let the distinct budgets be \(0=\beta_0<\beta_1<\cdots<\beta_J=B_{\max}\), where \(J\leq\tau\). On each interval \([\beta_j,\beta_{j+1}]\), define

\[ A_j=\sum_{b:B_b\leq\beta_j}\mu_bB_b, \qquad M_j=\sum_{b:B_b>\beta_j}\mu_b. \]

Here \(M_j>0\), and

\[ F(t)=A_j+M_jt. \]

For \(u<H\), locate an interval satisfying \(F(\beta_j)\leq u<F(\beta_{j+1})\). Its inverse value is exactly

\[ F^{-1}(u)=\frac{u-A_j}{M_j}. \]

For \(u=H\), return \(B_{\max}\).

Thus the algorithm sorts the chores and budget breakpoints, computes rational sums, locates the inverse intervals, and evaluates the allocation formula. It uses polynomially many rational operations and outputs \(m\tau\) rational coordinates.

All intermediate quantities have polynomial encoding length. Specifically, \(Q_k\), \(C_k\), \(H\), \(A_j\), \(M_j\), and the breakpoint values are sums of polynomially many products of input rationals. Such sums admit common denominators of polynomial bit length. Each inverse value then requires one subtraction and one division, and each output coordinate requires two minima, one subtraction, and one division. These operations preserve polynomial bit length. Exact arithmetic therefore takes time polynomial in \(m\), \(\tau\), and \(L\).

The proof covers arbitrary positive rational masses, repeated budgets, equal densities, and zero disutilities.

⟨structured verdict parsed — rendered above⟩

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

The prover’s claim is proved. The construction satisfies feasibility, all comparisons between budget types, and the unrestricted residual-support condition. Its exact rational implementation runs in polynomial time. I found no mathematical gaps requiring repair.

1. Coordinates, density order, and inverse function

Because every \(s_k>0\), the transformation \(v_{b,k}=s_kX_{b,k}\) is well-defined and preserves nonnegativity and componentwise comparisons. The identities for size and disutility follow directly from the definitions.

The density ordering satisfies \(\rho_1\geq\cdots\geq\rho_m\geq0\), including when densities coincide or disutilities vanish.

The claimed strict increase of \(F\) on \([0,B_{\max}]\) is correct. A type attaining \(B_{\max}\) exists and has positive mass. For any \(0\leq t<t'\leq B_{\max}\), its contribution increases by precisely \(\mu_b(t'-t)>0\), while all other contributions are nondecreasing.

Together with continuity, \(F(0)=0\), and \(F(B_{\max})=H\), this justifies the unique inverse on the entire stated domain, including both endpoints.

2. Construction and feasibility

Each \(u_k\) belongs to \([0,H]\), so every inverse value used in the construction exists. Monotonicity of the cumulative supplies and of \(F^{-1}\) gives nondecreasing \(t_k\). Thus every allocation coordinate is nonnegative.

The prefix identity
\[ \sum_{j=1}^k v_{b,j}=\min\{B_b,t_k\} \]
is a valid telescoping sum, since \(t_0=0\) and budgets are positive. At \(k=m\), it proves budget feasibility.

The aggregate allocation identity is also exact:
\[ \sum_b\mu_bv_{b,k}=u_k-u_{k-1}. \]
The stated case distinction correctly bounds this increment between \(0\) and \(Q_k\), including when a cumulative supply equals \(H\). Division by positive \(s_k\) therefore establishes supply feasibility coordinate by coordinate.

3. Comparisons between budget types

The proof fixes arbitrary source and comparison types and an arbitrary admissible test vector. It therefore addresses the required universal quantifiers.

For every prefix, componentwise domination gives \(W_k\leq t_k\). Nonnegativity and the comparison budget give \(W_k\leq B_c\). Consequently,
\[ W_k\leq\min\{B_c,t_k\}=V_k. \]

The summation-by-parts identity is correct. Its coefficients are nonnegative: \(\rho_m\geq0\) and \(\rho_k-\rho_{k+1}\geq0\). Replacing each \(W_k\) by its upper bound \(V_k\) is therefore justified and yields precisely \(d(Y)\leq d(X_c)\).

The explicitly stated empty-sum convention handles \(m=1\). Equal densities and zero densities cause no problem.

4. Unrestricted residual-support comparisons

The residual-size identity follows from supply feasibility and the aggregate allocation formula:
\[ \sum_k s_kR_k=C_m-u_m=\max\{C_m-H,0\}. \]
Because residual coordinates are nonnegative and sizes are positive, a positive residual coordinate implies \(C_m>H\). Thus the index \(h\) used in the proof exists whenever needed.

For every \(k<h\), the construction allocates the entire supply of coordinate \(k\). Hence all residual-supported coordinates have indices at least \(h\), and their densities are at most \(\rho_h\).

Conversely, \(t_h=B_{\max}\), and all allocation coordinates with indices greater than \(h\) vanish. Every budget is filled because \(t_m=B_{\max}\). These facts justify the lower bound
\[ d(X_b)\geq\rho_hB_b. \]

The boundary case \(C_{h-1}=H\) is covered: allocation at coordinate \(h\) may be zero, but the claimed allocation-support and density bounds still hold.

For every admissible housekeeper test vector, the residual-support restriction therefore gives
\[ d(Y)\leq\rho_hs(Y)\leq\rho_hB_b\leq d(X_b). \]
No step assumes \(Y\leq R\). This proves exactly the stronger condition in the task.

When \(R=0\), the support restriction forces \(Y=0\), and the comparison holds because all disutilities are nonnegative.

5. Exact polynomial-time computation

The piecewise-affine description of \(F\) is correct on each consecutive breakpoint interval. Here \(\beta_0=0\) is the introduced endpoint, and the interval indices run from \(0\) to \(J-1\). On each such interval, a positive-mass type has budget greater than its left endpoint, so \(M_j>0\).

The inverse formula is valid, including at lower interval endpoints. The separate treatment of \(u=H\) covers the terminal endpoint.

The bit-complexity argument is sufficient. The sums and products forming the supplies, cumulative supplies, budget totals, affine coefficients, and breakpoint values have polynomial encoding length. Each inverse and output coordinate then uses only a fixed number of further rational operations. Exact sorting and interval comparisons also operate on rationals of polynomial encoding length.

There are polynomially many operations and \(m\tau\) output coordinates. Thus the stated polynomial running time follows.

6. Scope and repair feedback

The proof covers the entire specified input domain and establishes existence as well as polynomial-time construction. It invokes no external theorem, so verification does not depend on extending the cited finite-agent result.

No repair or additional clarification 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.