← back to the atlas

Existence of 2-EFX Allocations of Chores (d4-conf-aaai-2026-2231)

Answer: —

The anchor (named result in the paper)

Theorem 6 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateFor any chore division instance with $\{1,k\}$-bivalued disutilities, a $(2-1/k)$-\efx and \po allocation always exists, and can be computed in polynomial time.

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

The continuous mirror question, as graded

Given rational \(k\ge1\), finite agent types \(\Theta\) with masses \(\mu_\theta\), finite chore types \(Q\) with rational per-capita supplies \(b_q\), and \(d_{\theta q}\in\{1,k\}\), compute a finite-support distribution \(\pi_{\theta,B}\) over integral bundles \(B\in\mathbb Z_{\ge0}^{Q}\) satisfying \(\sum_B\pi_{\theta,B}=\mu_\theta\), \(\sum_{\theta,B}\pi_{\theta,B}B_q=b_q\), pointwise \((2-1/k)\)-EFX across every supported pair, and \(PO_\infty\), in time polynomial in the compressed input size.

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

A society is an atomless population given by its support: a list \(\Theta\) of \(\tau\ge1\) types with positive binary rational masses \(\mu_\theta\), normalized by \(\sum_\theta\mu_\theta=1\). Here \(\tau\) is the support size, not the number of possible types.
There are \(m=|Q|\ge1\) chore types with nonnegative rational per-capita supplies \(b_q\), rational \(k\ge1\), and additive disutilities with \(d_{\theta q}\in\{1,k\}\). Let \(L\) be the total binary input length.
An allocation is a finitely supported array \(\pi_{\theta,B}\in\mathbb Q_{\ge0}\), where \(B\in\mathbb Z_{\ge0}^{Q}\), satisfying \(\sum_B\pi_{\theta,B}=\mu_\theta\) and \(\sum_{\theta,B}\pi_{\theta,B}B_q=b_q\). It describes realized integral bundles; empty bundles are allowed. Bundle counts and masses are encoded in binary.
Write \(d_\theta(B)=\sum_q d_{\theta q}B_q\). Pointwise \((2-1/k)\)-EFX requires \(d_\theta(B)-d_{\theta q}\le(2-1/k)d_\theta(C)\) whenever \(\pi_{\theta,B}>0\), \(\pi_{\eta,C}>0\), and \(B_q>0\), including pairs of the same type.
Define \(PO_\infty\) by absence of a nonnegative real redistribution array \(\gamma_{\theta,B,C}\), over integral bundles \(B,C\), with \(\sum_C\gamma_{\theta,B,C}=\pi_{\theta,B}\) and \(\sum_{\theta,B,C}\gamma_{\theta,B,C}C_q=b_q\), such that every positive entry satisfies \(d_\theta(C)\le d_\theta(B)\) and entries satisfying strict inequality have positive total mass. Redistributions need not have finite support or satisfy EFX.

Can a pointwise \((2-1/k)\)-EFX and \(PO_\infty\) allocation be computed in time polynomial in \(m,\tau,L\), or is this computation NP-hard?

For explicitly listed finite agents and indivisible chores, a \((2-1/k)\)-EFX and Pareto-optimal allocation always exists and is computable in polynomial time; exact EFX and Pareto optimality are also attainable in polynomial time when \(k=2\). [Lin, Wu, and Zhou](https://arxiv.org/html/2501.04550v1)
No result settling this precise support-encoded atomless problem was located.

Modeling choices made when packaging the task

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

Partial resolution: a polynomial-time algorithm for every integer $k$

The general question for arbitrary rational $k$ remains unresolved. However, the support-encoded problem is polynomial-time solvable whenever $k$ is an integer, even when $k$ is large and encoded in binary.

For noninteger rational $k>1$, I also prove polynomial-time constructions in two additional regimes. A polynomial-time flow computation produces a number $E$ satisfying
$$ S\le E\le kS, \qquad S:=\sum_q b_q. $$
The constructions succeed:

$$ E\ge \frac{k(3k-2)}{k-1}. $$

In particular, sufficiently large total supply is handled for every rational $k>1$.

All arguments below concern realized integral bundles and establish $PO_\infty$ directly.

1. Preprocessing and an efficiency certificate

Delete every zero-supply chore type. Nonnegativity and supply conservation force its coordinate to vanish in every positive allocation or redistribution entry. If $S=0$, assigning everyone the empty bundle is exact EFX and $PO_\infty$.

Assume henceforth that $S>0$. Normalize any type that evaluates every active chore at $k$ by dividing its disutilities by $k$. Thus write
$$ d_{\theta q}=r_\theta c_{\theta q}, \qquad r_\theta\in\{1,k\}, \qquad c_{\theta q}\in\{1,k\}, $$
so that every type has an active chore with normalized cost one. Positive scaling preserves all EFX and individual improvement comparisons.

For positive payments $p_q$, define
$$ a_\theta:=\min_q\frac{c_{\theta q}}{p_q}. $$
Call an allocation compatible with these payments if every assigned chore satisfies
$$ c_{\theta q}=a_\theta p_q. $$
Writing
$$ P(B):=\sum_qp_qB_q, $$
compatibility implies
$$ c_\theta(B)=a_\theta P(B) $$
for every supported bundle of type $\theta$, whereas every integral bundle $C$ satisfies
$$ c_\theta(C)\ge a_\theta P(C). $$

Lemma 1. Every finitely supported allocation compatible with positive payments is $PO_\infty$. Moreover, if its supported bundles satisfy
$$ P(B)-p_q\le\beta P(C) $$
for every supported pair $B,C$ and every $q$ occurring in $B$, then it is pointwise $\beta$-EFX.

Proof. Set
$$ w_\theta:=\frac1{r_\theta a_\theta}>0. $$
Then
$$ w_\theta d_{\theta q}\ge p_q, $$
with equality on every assigned coordinate. Consequently, the allocation’s weighted total disutility is
$$ \sum_{\theta,B}\pi_{\theta,B}w_\theta d_\theta(B) =\sum_qp_qb_q. $$

Any weakly improving redistribution actually has finite support. Indeed, only the finitely many positive source records can contribute. From a source record $(\theta,B)$, an allowed destination satisfies
$$ d_\theta(C)\le d_\theta(B). $$
Since every original per-chore disutility is at least one,
$$ |C|\le d_\theta(B), $$
leaving only finitely many integral destinations.

Thus all relevant sums are finite. Supply conservation and the coordinate inequalities give
$$ \sum_{\theta,B,C}\gamma_{\theta,B,C}w_\theta d_\theta(C) \ge\sum_qp_qb_q. $$
A weak improvement with positive-mass strict improvement would make the left side strictly smaller than the original weighted total, a contradiction.

For fairness, compatibility and the assumed payment inequality give
$$ c_\theta(B)-c_{\theta q} =a_\theta\bigl(P(B)-p_q\bigr) \le\beta a_\theta P(C) \le\beta c_\theta(C). $$
Multiplication by $r_\theta$ proves the original EFX inequality. This applies equally to same-type comparisons. $\square$

2. A flow construction with two payment levels

Assume $k>1$. For a positive rational parameter $t$, form a directed network with:

Compute a maximum flow $f$, and let $H$ and $T$ be, respectively, the chore and type vertices reachable from the source in its residual network. Let
$$ J:=Q\setminus H. $$

All chore-to-type arcs retain positive forward residual capacity: their flow is at most the total flow, which is at most $S$, while their capacity is $S+1$.

The following properties hold.

Property 1 also implies that no cost-one arc joins a chore in $H$ to a type outside $T$. Therefore all flow reaching $T$ comes from $H$, and all flow reaching types outside $T$ comes from $J$. In particular,
$$ \sum_{q\in H}f_{q\theta}=\mu_\theta t \quad(\theta\in T), $$
and
$$ \sum_{\theta\notin T}f_{q\theta}=b_q \quad(q\in J). $$

Set
$$ p_q= \begin{cases} k,&q\in H,\\ 1,&q\in J. \end{cases} $$

Every type in $T$ has a cost-one neighbor in $H$: its saturated sink arc carries positive flow, coming from such neighbors. Hence its minimum normalized cost-to-payment ratio is $1/k$.

Every type outside $T$ evaluates all chores in $H$ at $k$. Its active cost-one chore must therefore belong to $J$, and its minimum ratio is one. Consequently, the following assignments are compatible with these payments:

These observations will supply every efficiency certificate below.

The flow computation is polynomial in binary input length. For example, the [Edmonds–Karp algorithm](https://web.eecs.umich.edu/~pettie/matching/Edmonds-Karp-network-flow.pdf) uses $O(VA^2)$ arithmetic operations for a network with $V$ vertices and $A$ arcs. Here both are polynomial in $m,\tau$. Clearing the rational capacity denominators requires only polynomially many bits, so the arithmetic also has polynomial bit complexity.

Equal payment per person

Now use $t=S$. Write
$$ b_H:=\sum_{q\in H}b_q, \qquad b_J:=\sum_{q\in J}b_q, \qquad M_T:=\sum_{\theta\in T}\mu_\theta, $$
and define
$$ E:=kb_H+b_J. $$
Since $b_H+b_J=S$,
$$ S\le E\le kS. $$

Lemma 2. One can compute rational aggregate assignments $x_{\theta q}\ge0$ satisfying
$$ \sum_\theta x_{\theta q}=b_q, \qquad \sum_qp_qx_{\theta q}=\mu_\theta E, $$
using only compatible coordinates.

Proof. Put
$$ \lambda:=\frac{E}{kS}\le1. $$
For types in $T$, assign
$$ x_{\theta q}=\lambda f_{q\theta}. $$
These assignments use only cost-one chores in $H$, and each such type receives payment
$$ k\lambda\mu_\theta S=\mu_\theta E. $$

For types outside $T$, retain all flow on chores in $J$. This allocates their entire supply. The remaining supply of each chore in $H$ is
$$ r_q=b_q-\lambda\sum_{\theta\in T}f_{q\theta}\ge0. $$

The remaining payment capacity of an outside type is
$$ \delta_\theta =\mu_\theta E-\sum_{q\in J}f_{q\theta}\ge0, $$
because its original total flow is at most $\mu_\theta S$ and $E\ge S$.

The total remaining payment capacity equals the payment of the remaining chores:
$$ \sum_{\theta\notin T}\delta_\theta =(1-M_T)E-b_J =kb_H-M_TE =k\sum_{q\in H}r_q. $$
Greedily distribute the remaining $H$-supply among outside types with count capacities $\delta_\theta/k$. Every such assignment is compatible. The resulting matrix $x$ has the claimed properties. $\square$

This lemma is a fractional construction. The next sections convert it into finitely supported arrays of integral bundles.

3. Complete construction for integer $k$

Theorem 3. For every integer $k\ge1$, a pointwise $(2-1/k)$-EFX and $PO_\infty$ allocation is computable in time polynomial in $m,\tau,L$.

3.1 The case $k=1$

All disutilities equal bundle cardinality. Let
$$ r=\lfloor S\rfloor, \qquad f=S-r. $$
For each type and chore, add the records
$$ \pi_{\theta,re_q} =\mu_\theta(1-f)\frac{b_q}{S}, \qquad \pi_{\theta,(r+1)e_q} =\mu_\theta f\frac{b_q}{S}, $$
merging coincident bundles.

Their type masses sum to $\mu_\theta$, and their contribution to chore $q$ is
$$ \frac{b_q}{S}\bigl((1-f)r+f(r+1)\bigr)=b_q. $$
Every bundle has cardinality $r$ or $r+1$, so removing any chore leaves at most $r$ chores. This proves exact EFX. Payments $p_q=1$ make every coordinate compatible, so Lemma 1 proves $PO_\infty$.

Assume henceforth that $k>1$.

3.2 Total supply at most one

This construction works for every rational $k>1$, not only integers.

Use the flow network of Section 2 with $t=1$. Its total flow is $F\le S\le1$. Residual supply occurs only in $H$, and residual population capacity occurs only outside $T$. Their totals satisfy
$$ S-F\le1-F. $$
Thus greedily assign all residual chore supply as singleton bundles to the remaining outside-type capacity. Retain the flow assignments as singletons, and assign any unused population mass the empty bundle.

The assignments are compatible by Section 2. Every nonempty bundle is a singleton, so deleting its chore leaves zero cost. The allocation is exact EFX and, by Lemma 1, $PO_\infty$.

Henceforth assume $S>1$, and compute $H,T,E$ using $t=S$.

3.3 The case $E\le k$

This case also works for every rational $k>1$.

Since
$$ kb_H+b_J=E\le k $$
and $S>1$, necessarily $b_H<1$. Indeed, $b_H\ge1$ would force $b_H=1$, $b_J=0$, and $S=1$.

Define
$$ \ell:=\frac{b_J}{1-b_H}. $$
Then
$$ \ell-S=\frac{b_H(S-1)}{1-b_H}\ge0, $$
and $E\le k$ gives $\ell\le k$. Thus
$$ 1<S\le\ell\le k. $$

Assign every type in $T$ exclusively singleton chores from $H$, using aggregate assignments
$$ y_{\theta q}:=\frac{f_{q\theta}}{S}. $$
Their row sums are $\mu_\theta$, and their total consumption of $H$-supply is $M_T$.

For an outside type, let
$$ L_\theta:=\sum_{q\in J}f_{q\theta}, \qquad \nu_\theta:=\frac{L_\theta}{\ell}. $$
Because $L_\theta\le\mu_\theta S$ and $\ell\ge S$,
$$ 0\le\nu_\theta\le\mu_\theta. $$

Use population mass $\nu_\theta$ for cost-one chores from $J$. Its bundles have cardinalities $\lfloor\ell\rfloor$ and $\lceil\ell\rceil$, with mean $\ell$. Their chore composition can be chosen explicitly: conditional on this population portion, select chore $q$ with probability $f_{q\theta}/L_\theta$, then give the selected cardinality entirely in that chore. The expected aggregate count of $q$ is precisely $f_{q\theta}$. If $L_\theta=0$, omit this portion.

Assign the remaining mass $\mu_\theta-\nu_\theta$ a singleton from $H$. This completion is feasible. For each $q\in H$, the residual supply after assigning $T$ is nonnegative because $S>1$, and its total is
$$ b_H-M_T. $$
The total remaining outside population mass is exactly
$$ \sum_{\theta\notin T}(\mu_\theta-\nu_\theta) =1-M_T-\frac{b_J}{\ell} =b_H-M_T. $$
A greedy transportation assignment therefore completes the construction.

All assignments are compatible. Supported bundles are either:

A singleton has zero payment after deletion. Deleting a chore from a low-payment bundle leaves payment at most $\lfloor\ell\rfloor$. Every supported comparison bundle has payment at least $\lfloor\ell\rfloor$, because
$$ k\ge\ell\ge\lfloor\ell\rfloor. $$
Thus the allocation is exact payment-EFX. Lemma 1 proves exact EFX and $PO_\infty$.

3.4 The case $E>k$ with integer $k$

Compute the aggregate assignment $x$ from Lemma 2. Put
$$ r:=\left\lfloor\frac Ek\right\rfloor, \qquad z:=kr, \qquad \lambda:=\frac{E-z}{k}. $$
Here $r\ge1$, $z$ is an integer, and $0\le\lambda<1$.

For every positive $x_{\theta q}$, create the two records
$$ \pi_{\theta,(z/p_q)e_q} \mathrel{+}=(1-\lambda)\frac{p_qx_{\theta q}}E, $$
$$ \pi_{\theta,((z+k)/p_q)e_q} \mathrel{+}=\lambda\frac{p_qx_{\theta q}}E. $$
Both bundle counts are integers: $p_q$ is either $1$ or $k$, while $z=kr$.

The type-mass equations follow from Lemma 2:
$$ \sum_B\pi_{\theta,B} =\frac1E\sum_qp_qx_{\theta q} =\mu_\theta. $$
For a fixed type and chore, the assigned aggregate count is
$$ \frac{x_{\theta q}}E \bigl((1-\lambda)z+\lambda(z+k)\bigr) =x_{\theta q}, $$
because $E=z+\lambda k$. Summing over types proves supply conservation.

Every supported bundle has payment $z$ or $z+k$. Deleting any occurring chore leaves payment at most $z+k-1$. Write
$$ \alpha:=2-\frac1k. $$
Since $r\ge1$,
$$ z+k-1 \le z+(k-1)r =\alpha z. $$
Every comparison bundle has payment at least $z$. Therefore
$$ P(B)-p_q\le\alpha z\le\alpha P(C). $$
Compatibility is preserved because the construction uses only coordinates with $x_{\theta q}>0$. Lemma 1 establishes both pointwise $\alpha$-EFX and $PO_\infty$.

The cases above exhaust all integer $k$ and all supplies. $\square$

Why the integer hypothesis matters here. The construction simultaneously uses bundle payments $z$ and $z+k$ for both payment categories. When $k$ is an integer, these payments are realizable by integral counts of either category. For noninteger $k$, the low-payment counts $z$ and $z+k$ need not be integers, so this construction does not apply.

4. A large-payment construction for arbitrary rational $k$

The preceding sections already establish exact EFX for $S\le1$ and for $S>1$, $E\le k$. The following handles another range without assuming integer $k$.

Theorem 4. For rational $k>1$, if the value $E$ from Lemma 2 satisfies
$$ E\ge T(k):=\frac{k(3k-2)}{k-1}, $$
a pointwise $(2-1/k)$-EFX and $PO_\infty$ allocation can be computed in polynomial time. In particular, the condition holds whenever $S\ge T(k)$.

Proof. For each type define its per-capita aggregate counts in the two payment categories:
$$ u_\theta:=\frac1{\mu_\theta}\sum_{q:p_q=1}x_{\theta q}, \qquad v_\theta:=\frac1{\mu_\theta}\sum_{q:p_q=k}x_{\theta q}. $$
Lemma 2 gives
$$ u_\theta+kv_\theta=E. $$

We first construct a distribution on integral category totals $U,V$ with
$$ \mathbb E[U]=u_\theta, \qquad \mathbb E[V]=v_\theta, \qquad E-k\le U+kV\le E+k $$
at every positive-probability outcome.

Write
$$ a=\lfloor u_\theta\rfloor,\quad x=u_\theta-a, \qquad b=\lfloor v_\theta\rfloor,\quad y=v_\theta-b. $$
Thus $0\le x,y<1$.

If $x+y\le1$, use the outcomes
$$ (a,b),\quad(a+1,b),\quad(a,b+1) $$
with probabilities
$$ 1-x-y,\quad x,\quad y. $$
If $x+y>1$, use
$$ (a+1,b),\quad(a,b+1),\quad(a+1,b+1) $$
with probabilities
$$ 1-y,\quad1-x,\quad x+y-1. $$
Direct calculation gives the required expectations in both cases.

For the payment bound, subtract the base payment $a+kb$. In the first case the outcome offsets belong to $[0,k]$, while their mean $x+ky$ also belongs to $[0,k]$. In the second case the offsets belong to $[1,k+1]$, and
$$ 1<x+ky<k+1. $$
Hence every outcome differs from its mean payment $E$ by at most $k$.

To realize chore coordinates, conditional on $(U,V)$ choose one low-payment chore with probabilities proportional to $x_{\theta q}$ within that category, and put all $U$ chores on it. Do the same independently for the high-payment category and its $V$ chores. An absent category has count zero and needs no choice. This produces integral bundles with precisely the aggregate coordinate expectations $x_{\theta q}/\mu_\theta$.

Giving these bundles their corresponding population masses preserves every type mass and every chore supply. It also preserves compatibility.

For every supported bundle,
$$ E-k\le P(B)\le E+k. $$
Since every occurring chore has payment at least one,
$$ P(B)-p_q\le E+k-1. $$
The threshold assumption is exactly the inequality
$$ E+k-1 \le\left(2-\frac1k\right)(E-k). $$
Indeed, after rearrangement it becomes
$$ \frac{k-1}{k}E\ge3k-2. $$
Every supported comparison bundle has payment at least $E-k$. Lemma 1 proves the required EFX guarantee and $PO_\infty$.

Finally, $E\ge S$, so $S\ge T(k)$ implies the stated condition. $\square$

5. Binary complexity and the remaining question

All these constructions have polynomial binary complexity.

The networks have polynomially many vertices and arcs. Their rational capacities have polynomial encoding length, as do the resulting flows. Greedy transportation completes residual assignments using polynomially many rational operations.

Every subsequent formula uses rational sums, products, divisions, and floors of polynomial-length numbers. For example,
$$ E\le kS, $$
so the integers appearing in bundle counts have polynomial binary length even when their numerical values are large.

The integer-$k$ construction in Section 3.4 has at most $2\tau m$ positive records. The exact-EFX constructions have polynomial support. The construction in Theorem 4 has at most three category-count outcomes per type and at most $m^2$ coordinate choices per outcome, hence at most $3\tau m^2$ records. Duplicate bundles are merged.

Thus the integer-$k$ result is a polynomial-time algorithm in the requested binary model, rather than an algorithm whose running time depends polynomially on the numerical value of $k$ or the expanded population size.

For the full task, the remaining regime consists of noninteger rational $k>1$, with $S>1$ and the constructed payment value in the interval
$$ k<E<\frac{k(3k-2)}{k-1}. $$
The arguments here neither give a general construction for that regime nor establish NP-hardness. In particular, the integer-$k$ theorem does not settle the arbitrary-rational-$k$ question.

⟨structured verdict parsed — rendered above⟩

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

Assessment: valid partial resolution. The claimed algorithms for integer $k$ and the stated additional rational-$k$ regimes are correct. I found no false step or substantive proof gap in those results. The full arbitrary-rational-$k$ task remains unresolved, as the prover explicitly acknowledges.

1. Preprocessing and normalization

Deleting zero-supply coordinates is valid: nonnegativity and conservation force those coordinates to vanish in every positive allocation or redistribution entry.

When $S=0$, every realized bundle must be empty. The proposed allocation therefore satisfies exact EFX and $PO_\infty$.

For $S>0$, the normalization is valid on the remaining active coordinates. Dividing an all-$k$ type’s disutilities by $k$ preserves its weak and strict improvement comparisons and its EFX inequalities. Every normalized type has an active cost-one chore. No unmentioned restriction on the original type support is introduced.

2. Lemma 1: the efficiency and fairness certificate

The weighted coordinate inequality
$$ w_\theta d_{\theta q}\ge p_q $$
and equality on assigned coordinates follow directly from the definition of $a_\theta$ and compatibility.

The treatment of unrestricted redistribution support is sound. There are only finitely many positive source records. For each such record, weak improvement requires
$$ |C|\le d_\theta(B). $$
Because the number of chore coordinates is finite, this permits only finitely many integral destination bundles. Zero source records cannot contribute positive entries because their row sums are zero and entries are nonnegative. Thus every weakly improving redistribution under consideration actually has finite support.

Consequently, the weighted-sum comparison is justified. Supply conservation gives the lower bound by total payment, whereas positive-mass strict improvement makes weighted total disutility strictly smaller. All weights are positive, so this is a contradiction. The argument establishes precisely the requested $PO_\infty$ property.

The fairness implication is also correct for the factors used in the constructions:
$$ c_\theta(B)-c_{\theta q} =a_\theta(P(B)-p_q) \le\beta a_\theta P(C) \le\beta c_\theta(C). $$
Compatibility is required only for the source bundle’s assigned coordinates; the lower bound for the comparison bundle holds for every bundle. Same-type comparisons are included.

3. The residual-flow construction

All capacities are finite, nonnegative rationals. Each chore-to-type arc has flow at most $S$, so capacity $S+1$ leaves positive forward residual capacity.

The four residual-network properties are valid:

These properties justify the stated separation of flow between $H,T$ and their complements.

For a type in $T$, its positive saturated sink flow supplies a cost-one neighbor in $H$, giving minimum ratio $1/k$. A type outside $T$ has no cost-one neighbor in $H$, and its normalized cost-one chore must lie in $J$, giving minimum ratio one. Thus all three listed classes of compatible assignments are correctly identified.

The maximum-flow complexity claim is valid. Edmonds–Karp has the stated arithmetic-operation bound $O(VA^2)$. [MIT’s algorithm notes](https://ocw.mit.edu/courses/6-046j-design-and-analysis-of-algorithms-spring-2015/ba74f89434fc261d9366ebf136c04b52_MIT6_046JS15_Recitation7.pdf) confirm this bound. Clearing the rational capacity denominators requires polynomial binary length here, so the application also has polynomial bit complexity.

4. Lemma 2: equal aggregate payment

The bounds
$$ S\le E\le kS $$
follow from nonnegative $b_H,b_J$ and $b_H+b_J=S$. Therefore the scaling factor satisfies
$$ 0<\lambda=\frac{E}{kS}\le1. $$

For each type in $T$, scaling its saturated flow gives payment $\mu_\theta E$ and uses only compatible coordinates.

For outside types, retaining the $J$ flow allocates all $J$ supply. Both remaining chore supplies and remaining payment capacities are nonnegative. In particular,
$$ \sum_{q\in J}f_{q\theta}\le\mu_\theta S\le\mu_\theta E. $$

The balance calculation is correct:
$$ \sum_{\theta\notin T}\delta_\theta =(1-M_T)E-b_J =kb_H-M_TE =k\sum_{q\in H}r_q. $$

The remaining assignment has no coordinate restrictions: every $H$ chore is compatible with every outside type. Hence the stated greedy transportation completion is justified. Empty sets and zero residual totals cause no division or feasibility problem.

5. The constructions for small supply and small payment

For $k=1$, the proposed records preserve both type masses and supplies. When $r=0$, coincident empty bundles must be merged by summing masses, as the text specifies. Every supported cardinality is $r$ or $r+1$, so deletion leaves cardinality at most $r$, while every comparison bundle has cardinality at least $r$. Exact EFX follows.

For $S\le1$, flow counts can be used directly as singleton population masses. Reachable types have no remaining capacity, and residual chores lie in $H$. The inequality
$$ S-F\le1-F $$
ensures sufficient outside population capacity. All residual assignments are compatible, and singleton deletion leaves zero disutility even when the comparison bundle is empty.

For $S>1$ and $E\le k$, the deduction $b_H<1$ is correct, so $\ell$ is well-defined. The calculations establishing
$$ 1<S\le\ell\le k $$
are correct.

The assignments to types in $T$ have the required row masses. For outside types,
$$ 0\le\nu_\theta\le\mu_\theta $$
follows from $L_\theta\le\mu_\theta S$ and $\ell\ge S$. The stated pure-chore mixtures have the required coordinate expectations. The zero-$L_\theta$ case is explicitly handled.

Residual $H$ supply is coordinatewise nonnegative, and its total equals the remaining outside population mass. The completion is therefore feasible.

Finally, deleting from a low-payment bundle leaves payment at most $\lfloor\ell\rfloor$, and every comparison bundle has payment at least that amount. Singleton deletion leaves zero. Exact payment-EFX, exact EFX, and $PO_\infty$ follow.

6. The integer-$k$ construction for $E>k$

Here $r\ge1$. Both proposed bundle counts are integral because $p_q$ is either $1$ or integer $k$, and $z=kr$.

The population-mass calculation is correct. The supply calculation uses the exact identity
$$ (1-\lambda)z+\lambda(z+k)=E, $$
so each coordinate preserves its aggregate assignment $x_{\theta q}$.

The fairness estimate is valid:
$$ z+k-1 \le z+(k-1)r =\left(2-\frac1k\right)z. $$
Its first inequality follows from $r\ge1$ and $k>1$. Every supported comparison bundle has payment at least $z$.

The construction preserves compatibility. Lemma 1 therefore proves the requested properties. Together with the preceding cases, this establishes the full claimed theorem for integer $k$.

The explanation of why this particular construction does not directly extend to noninteger $k$ is accurate.

7. The large-payment construction for rational $k$

Both three-outcome distributions have nonnegative probabilities summing to one and give the claimed expectations.

Their payment bounds are correct. In the first case, the outcome offsets and their mean lie in $[0,k]$. In the second case, they lie in $[1,k+1]$. Each interval has width $k$, establishing
$$ E-k\le U+kV\le E+k. $$

The conditional chore choices preserve every coordinate expectation. A category with zero aggregate count has zero realized count in every positive-probability outcome, so omitting its chore choice is valid.

The threshold calculation checks:
$$ E+k-1 \le\left(2-\frac1k\right)(E-k) $$
is equivalent to
$$ \frac{k-1}{k}E\ge3k-2. $$
Also, the threshold ensures $E-k>0$. The payment comparison therefore establishes the required EFX bound. Compatibility again supplies $PO_\infty$.

The sufficient condition involving $S$ follows correctly from $E\ge S$.

8. Binary complexity

The complexity discussion is adequate for these explicit constructions. The flow computation has polynomially bounded rational encodings. The subsequent formulas have bounded algebraic depth, and greedy transportation uses sums, differences, and comparisons of polynomial-length rational quantities.

Bundle counts have polynomial binary length even when numerically large. The stated support bounds are valid, including the bound $3\tau m^2$ for the category-rounding construction. No expansion into individual agents or individual chore units is required.

9. What remains unresolved and required feedback

The output establishes genuine polynomial-time results for every integer $k$ and the stated additional rational-$k$ regimes. It supplies neither a general algorithm nor a hardness result for noninteger rational $k>1$ when
$$ S>1, \qquad k<E<\frac{k(3k-2)}{k-1}. $$

This is an acknowledged limitation, not an unjustified claim. No repair of the verified subcase proofs is necessary. To resolve USER_TASK, the next submission must address this remaining regime or establish hardness for the full computation problem with a specified reduction notion.

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