Answer: Every instance admits a finite-support rational EFX+PO allocation. Existence is in \(\mathrm P\), and for \(m=2\) an allocation with at most \(\tau+2\) positive-mass cohorts can be computed in time polynomial in \(m,\tau,L\).
Theorem 5 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateGiven preprocessed input, an EFX+PO allocation can be found in O(log n + log m) time.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite set of valuation types \(T\u005c), positive rational masses \(\mu_t\u005c) summing to \(1\u005c), positive rational valuations \(v_t=(1,r_t)\u005c), and rational per-capita supplies \(q_1,q_2\in\mathbb{Q}_{\ge 0}\u005c), does there always exist, and can one compute in time polynomial in \(\tau\u005c) and input bit length \(L\u005c), a finite-support allocation \(\lambda_{t,a,b}\ge 0\u005c) of type-\(t\u005c) mass to integral bundles \((a,b)\in\mathbb{Z}_{\ge0}^2\u005c), with type masses and aggregate supplies matching the input, that is EFX across every pair of positive-mass type-and-bundle cohorts and Pareto optimal? For Pareto optimality, compare feasible allocations through type-by-type couplings of old and new bundles: no such coupling may make almost every agent weakly better off and a positive mass strictly better off.
A society is given by its support: a nonempty list \(T\) of \(\tau\) valuation types with positive binary rational masses \(\mu_t\), where \(\sum_t\mu_t=1\); \(\tau\) is the support size, not the number of possible types. There are \(m=2\) good types, positive binary rational per-capita supplies \(q_1,q_2\), and positive binary rational valuations \(v_t=(1,r_t)\). Let \(L\) be the total input bit length.
Write \(B=\mathbb Z_{\ge0}^2\) and \(u_t(a,b)=a+r_tb\). A feasible allocation assigns masses \(\lambda_{t,x}\ge0\) satisfying \(\sum_{x\in B}\lambda_{t,x}=\mu_t\) and \(\sum_{t,x}\lambda_{t,x}x=(q_1,q_2)\). The requested allocation has finite support and binary rational masses; bundle coordinates are encoded in binary.
EFX holds across every ordered pair of positive-mass cohorts \((t,x),(s,y)\): \(u_t(x)\ge u_t(y-e_c)\) for each \(c\in\{1,2\}\) with \(y_c>0\), where \(e_c\) is the corresponding unit vector. An empty envied bundle imposes no condition.
An allocation is PO if there is no feasible allocation \(\lambda'\) and type-preserving coupling \(\gamma_{t,x,y}\ge0\) with marginals \(\lambda_{t,x}\) and \(\lambda'_{t,y}\), supported on \(u_t(y)\ge u_t(x)\), such that \(\sum_{t,x,y:\,u_t(y)>u_t(x)}\gamma_{t,x,y}>0\). Competitors and couplings may have real masses and countable support; competitors need not satisfy EFX.
Does every such instance admit a finite-support rational EFX+PO allocation?
Is deciding existence in \(\mathrm P\) or NP-hard, and can an allocation, whenever one exists, be computed in time polynomial in \(m,\tau,L\)?
For finite societies with positive additive valuations and two good types, EFX+PO allocations always exist; the algorithm uses \(O(\log n+\log M)\) arithmetic operations after preprocessing, with a compressed output, and \(O(n\log n+\log M)\) including preprocessing, where \(n\) counts agents and \(M\) counts goods. [Source](https://ojs.aaai.org/index.php/AAAI/article/download/38723/42685).
No result settling the exact mass model above was located in the literature search.
Every instance admits a finite-support rational EFX+PO allocation. For \(m=2\), such an allocation can be computed in time polynomial in \(\tau\) and \(L\). Consequently, existence is in \(\mathrm P\): every valid instance is a yes-instance.
Here, “binary rational” means a rational number represented by binary-encoded numerator and denominator. The construction can return at most \(\tau+2\) positive-mass cohorts.
We use the finite-society existence theorem supplied in the question. Its application alone does not establish the result: a Pareto improvement involving fractions of cohorts need not be implementable in a particular finite population. The proof below supplies the required transfer argument.
Fix a type \(t_0\), and write \(r_0=r_{t_0}\), \(\mu_0=\mu_{t_0}\). Define
\(\displaystyle C=\frac{q_1+r_0q_2}{\mu_0}+\max\{1,r_0\},\qquad H=\left\lceil\max\{1,C,C/r_0\}\right\rceil.\)
Lemma 1. Every positive-mass bundle in any feasible EFX allocation has both coordinates at most \(H\).
Proof. Let \(y\) be a positive-mass bundle. For every positive-mass cohort \((t_0,x)\), EFX implies
\(\displaystyle u_{t_0}(x)\ge u_{t_0}(y)-\max\{1,r_0\}.\)
For nonempty \(y\), this follows by removing an available good and bounding its value by \(\max\{1,r_0\}\). For empty \(y\), the inequality follows from nonnegative utility.
Multiplying by \(\lambda_{t_0,x}\) and summing gives
\(\displaystyle \mu_0\bigl(u_{t_0}(y)-\max\{1,r_0\}\bigr)\le \sum_x\lambda_{t_0,x}u_{t_0}(x)\le q_1+r_0q_2.\)
The last inequality holds because the sum over type \(t_0\) is part of the total value of all allocated goods, evaluated using \(u_{t_0}\), and every omitted term is nonnegative.
Thus \(y_1+r_0y_2\le C\), implying \(y_1\le H\) and \(y_2\le H\). \(\square\)
The integer \(H\) has bit length polynomial in \(L\). This bound also applies to a finite EFX allocation after dividing agent counts and total supplies by its population size.
Define
\(\displaystyle J=\left\lceil 1+H\max_{t\in T}\{1+r_t,\,1+r_t^{-1}\}\right\rceil,\qquad K=18J^2.\)
Both integers have bit length polynomial in \(L\), and \(J\ge H+1\).
A *transition* is a triple \((t,x,y)\), meaning that a cohort of type \(t\) changes from bundle \(x\) to bundle \(y\). It is admissible when \(u_t(y)\ge u_t(x)\), and strict when this inequality is strict.
Lemma 2. Suppose an allocation has finite support, all its source bundles lie in \(\{0,\ldots,H\}^2\), and it fails PO under the definition in the question. Then there exist at most three admissible transitions \((t_i,x_i,y_i)\), sourced in its positive support, and positive integers \(h_i\), such that:
Proof.
Take a witnessing competitor and coupling \(\gamma\). For every positive coupling entry \((t,x,y)\), set \(U=u_t(x)\).
If the transition is weakly improving with equality, choose a coordinatewise minimal integer bundle \(z\le y\) satisfying \(u_t(z)\ge U\). If it is strict, choose such a minimal bundle satisfying \(u_t(z)>U\). These choices exist because the integer box below \(y\) is finite and contains a qualifying bundle.
Whenever \(z_c>0\), minimality gives
\(\displaystyle u_t(z-e_c)\le U.\)
For weak transitions the inequality is actually strict; the displayed weaker form suffices. Consequently,
\(\displaystyle z_1\le U+1\le H(1+r_t)+1\le J,\)
and
\(\displaystyle z_2\le U/r_t+1\le H(1+r_t^{-1})+1\le J.\)
The reduced transition remains admissible, and every originally strict transition remains strict.
Aggregate the coupling entries by their source and reduced destination. There are now only finitely many transition kinds. If \(d=z-x\), their weighted sum is coordinatewise nonpositive: reducing destinations only saves goods.
Let \(w_c\ge0\) be the saved amount of good \(c\). Select any positive-mass source cohort \((t_*,x_*)\), and add the transition \(x_*\longrightarrow x_*+e_c\) with coefficient \(w_c\). These added transitions are strict because valuations are positive, and their destinations are bounded by \(J\).
The resulting finite nonnegative combination of transitions has total resource change zero and positive total coefficient on strict transitions. All sums used here are well-defined: the original source and destination first moments are finite by feasibility.
For each transition, form the integer column
\(\displaystyle a_i=(d_{i,1},d_{i,2},s_i)^{\mathsf T},\)
where \(s_i=1\) for a strict transition and \(s_i=0\) otherwise. After normalizing the positive total strict coefficient, the preceding construction gives
\(\displaystyle \sum_i\alpha_i a_i=(0,0,1)^{\mathsf T},\qquad \alpha_i\ge0.\)
This representation can be reduced to linearly independent positive columns. Indeed, if its positive columns are dependent, choose a nonzero dependence \(\sum_i\beta_i a_i=0\), oriented so that some \(\beta_i>0\). Subtract
\(\displaystyle \varepsilon\beta_i,\qquad \varepsilon=\min_{\beta_i>0}\alpha_i/\beta_i,\)
from their coefficients. Nonnegativity and the represented vector are preserved, and at least one coefficient becomes zero. Repeating leaves at most three independent columns.
Suppose \(r\le3\) columns remain. Choose \(r\) rows on which they form an invertible square integer matrix. Cramer’s rule expresses their positive coefficients using a common nonzero integer determinant. Multiplication by its absolute value gives positive integers \(h_i\).
Each numerator determinant contains the right-hand-side column, whose entries are zero or one. The other entries have absolute value at most \(J\). Hence the Leibniz determinant formula bounds each numerator by
\(\displaystyle r!J^{r-1}\le6J^2.\)
Thus \(h_i\le6J^2\). The first two equations give resource balance; the third guarantees a strict transition. There are at most three transitions, so their total multiplicity is at most \(18J^2=K\). \(\square\)
Corollary 3. Let \(X\) be a finite PO allocation with source bundles bounded by \(H\). Let \(R\) consist of cohorts containing at least \(K\) agents in \(X\). Every mass allocation whose positive support is contained in \(R\) is PO.
Proof. Otherwise Lemma 2 supplies an integer improving reallocation using at most \(K\) agents in total, with every source in \(R\). Each source cohort contains enough distinct agents to implement its transitions. Resource balance preserves the finite society’s supplies, every affected agent weakly improves, and at least one strictly improves. This contradicts finite PO. \(\square\)
This corollary allows the masses on retained cohorts to change arbitrarily.
Let \(Q_0\) be the product of the denominators of all \(\mu_t,q_1,q_2\). Thus their products with \(Q_0\) are integers. Set
\(\displaystyle d=\tau+2,\qquad k_{\max}=\tau(H+1)^2,\qquad \Delta=Q_0d!H^d,\)
and choose
\(\displaystyle N=Q_0\bigl(k_{\max}K\Delta+1\bigr).\)
In particular,
\(\displaystyle N>k_{\max}K\Delta.\)
Construct a finite society with \(N\mu_t\) agents of type \(t\) and \(Nq_c\) goods of type \(c\). Its populations and supplies are positive integers, its total population is \(N\), and its valuations are positive and additive. Thus the supplied finite-society theorem applies.
Take a finite EFX+PO allocation \(X\). Let \(S\) be its set of distinct cohorts, and let \(n_{t,x}\) be their positive integer counts. The normalized masses
\(\displaystyle z^0_{t,x}=n_{t,x}/N\)
satisfy the original feasibility equations. Lemma 1 bounds every bundle by \(H\), so \(|S|\le k_{\max}\).
Partition \(S\) into retained and discarded cohorts:
\(\displaystyle R=\{(t,x)\in S:n_{t,x}\ge K\},\qquad D=S\setminus R.\)
Lemma 4. There is a rational feasible allocation supported entirely on \(R\).
Proof. For each cohort \((t,x)\in S\), form the column
\(\displaystyle A_{t,x}=(e_t,x_1,x_2)^{\mathsf T}\in\mathbb Z^d,\)
where \(e_t\) is the type’s unit vector in \(\mathbb R^\tau\). Write
\(\displaystyle b=(\mu_1,\ldots,\mu_\tau,q_1,q_2)^{\mathsf T}.\)
Consider the nonempty compact polytope
\(\displaystyle P=\{z\ge0:Az=b\},\)
and minimize \(\sum_{j\in D}z_j\) over \(P\). Compactness follows from the type equations, which imply \(\sum_jz_j=1\).
At any vertex of \(P\), its positive columns are linearly independent. Otherwise a dependence would permit sufficiently small perturbations in both directions, contradicting extremality. There are therefore at most \(d\) positive coordinates. Select an invertible square submatrix on those columns and independent rows. Its entries have absolute value at most \(H\), so its determinant has absolute value at most \(d!H^d\).
Because \(Q_0b\) is integral, Cramer’s rule shows that the positive coordinates of this vertex have a common denominator of magnitude at most \(\Delta\). Every positive coordinate is consequently at least \(1/\Delta\).
A linear objective on a nonempty compact polytope has an optimal vertex. Therefore, if the minimum discarded mass were positive, it would be at least \(1/\Delta\).
But the original normalized allocation satisfies
\(\displaystyle \sum_{j\in D}z^0_j<\frac{|D|K}{N}\le\frac{k_{\max}K}{N}<\frac1\Delta.\)
The minimum must thus be zero. An optimal vertex is rational, feasible, and supported on \(R\). \(\square\)
Let \(z^*\) be such a vertex. It is EFX because its positive support is a subset of the EFX support of \(X\); all relevant pairwise inequalities are inherited. It is PO by Corollary 3. Its support has at most \(d=\tau+2\) cohorts.
This proves existence, including PO against real-mass competitors with countable support.
The preceding scaling has polynomial bit length:
\(\displaystyle \log Q_0=O(L),\qquad \log H=O(L),\qquad \log J=O(L),\)
and
\(\displaystyle \log\Delta=O\bigl(L+d\log d+d\log H\bigr).\)
Hence \(\log N\), and the bit lengths of \(N\mu_t\) and \(Nq_c\), are polynomial in \(\tau,L\). We must nevertheless avoid explicitly constructing \(N\) agents.
The supplied finite algorithm permits this. After sorting agents, it uses \(O(\log n+\log M)\) arithmetic operations and outputs bundles on a constant number of intervals of agent ranks, allowing an exceptional split agent. The interval representation follows from its equitable, split, and reallocation constructions. See Definitions 4, 5, 8, Claim 1, and Theorem 5 in the [finite-society paper](https://ojs.aaai.org/index.php/AAAI/article/download/38723/42685).
We simulate that algorithm as follows:
The finite algorithm uses binary searches and explicit arithmetic formulas with integer floors and ceilings. Its intermediate numbers are counts, search indices, or products and quotients involving counts and input valuations. Their bit lengths are polynomial in \(\log N+\log(Nq_1+Nq_2)+L\). Thus the virtual simulation has polynomial bit complexity.
Lemma 4 guarantees feasibility of the final linear program. It has \(O(\tau)\) variables, \(\tau+2\) equations, and polynomial-size rational data. Standard rational linear programming and basic feasible solution extraction therefore take polynomial time.
The returned allocation has at most \(\tau+2\) positive masses. Their common denominator is bounded by \(\Delta\), as in Lemma 4, and its bundle coordinates are bounded by \(H\). Its entire output consequently has polynomial bit length.
Every valid instance admits the requested allocation. Existence is therefore in \(\mathrm P\), and, for the stipulated \(m=2\), an allocation can be computed in time polynomial in \(m,\tau,L\).
The essential transfer step is the bounded integer witness in Lemma 2. It justifies PO in the exact mass model; finite-society PO alone would not suffice.
⟨structured verdict parsed — rendered above⟩
The argument establishes universal existence and polynomial-time construction, subject to one minor empty-set case in Lemma 4. I found no false central step or gap requiring additional mathematics.
The construction addresses the exact model in USER_TASK: it preserves each type’s mass, allocates both supplies exactly, returns finitely many integer bundles with rational masses, and establishes PO against real-mass, countably supported competitors.
The finite theorem is applied to a society with integer populations \(N\mu_t\) and integer supplies \(Nq_c\). These are positive because \(N\) is a multiple of all relevant denominators and the original inputs are positive. The valuations are positive and additive, as required.
The finite and cohort definitions of EFX agree for integer bundles. The proof correctly avoids assuming that finite-agent PO alone implies the requested mass-model PO.
The EFX inequality used here is valid. For a nonempty envied bundle, removing any available good subtracts at most \(\max\{1,r_0\}\). For the empty bundle, the displayed inequality follows from nonnegative utility.
Summation over type \(t_0\) is justified even for countable support: all utility terms are nonnegative, and feasibility bounds their total by \(q_1+r_0q_2\). Dividing by the positive mass \(\mu_0\) yields the stated bound.
Because \(r_0>0\), the bound on utility bounds both bundle coordinates. The ceiling defining \(H\) is sufficient, and \(H\ge1\). Its claimed polynomial bit length follows from rational arithmetic on the input.
Assessment: correct.
A coordinatewise minimal qualifying destination exists in the finite integer box below each original destination.
The distinction between weak and strict transitions is handled correctly:
Thus the displayed weaker inequality applies in both cases. The bounds on reduced coordinates are valid, including when a coordinate is zero, and the definition of \(J\) covers them uniformly.
There are finitely many reduced transition kinds because sources have finite support and reduced destinations are bounded. Aggregation preserves admissibility and positive strict-transition mass.
Reducing destinations saves a finite, nonnegative amount of each good. The added unit-good transitions restore resource balance and have destinations bounded by \(J\). Their coefficients need not obey cohort capacities at this stage: the argument is constructing a balanced combination of transition vectors, not yet a feasible coupling. Corollary 3 subsequently supplies the required source capacities.
Normalization is legitimate because the strict-transition coefficient is positive and finite. The dependence-elimination procedure preserves nonnegativity and the represented vector, while eliminating at least one positive coefficient per iteration.
The resulting independent columns number at most three. Cramer’s rule applies to an invertible row minor. Clearing its integer determinant produces positive integer coefficients.
The determinant estimate is valid: the right-hand-side column has entries of magnitude at most one, while each other entry has magnitude at most \(J\). Consequently, each numerator is bounded by \(r!J^{r-1}\le6J^2\).
The full vector equations remain valid after clearing denominators, so the witness balances both resources and includes a strict transition. The total multiplicity bound \(18J^2\) follows.
Assessment: correct, including the passage from countable real-mass competitors to bounded integer witnesses.
Every witness uses at most \(K\) agents in total. Consequently, even if several witness transitions share one source cohort, that cohort requires at most \(K\) distinct agents.
Each retained cohort contains at least that many agents. The integer witness therefore gives an actual finite-agent reallocation preserving supplies, weakly improving every affected agent and strictly improving at least one.
This contradicts finite PO. The argument depends only on the retained support, so changing the masses on that support does not invalidate it.
Assessment: correct.
The polytope is nonempty because it contains the normalized finite allocation. It is compact because its nonnegative coordinates sum to one.
At a vertex, positive columns must be independent; the stated two-sided perturbation argument is applicable. Selecting an invertible row minor and applying Cramer’s rule gives rational coordinates with a common denominator bounded by \(\Delta\). The determinant estimate remains valid for minors smaller than \(d\), since \(H\ge1\).
Thus any positive discarded mass at an optimal vertex is at least \(1/\Delta\). The chosen population size makes the original discarded mass smaller than this threshold whenever the discarded set is nonempty.
Minor issue: the written inequality
\(\sum_{j\in D}z^0_j<|D|K/N\)
is false when \(D\) is empty: both sides are zero.
Minimum clarification needed: separate the case \(D=\varnothing\), in which the original normalized allocation already supplies the claimed feasible allocation on \(R\).
This omission does not affect the substantive argument.
The optimal vertex has at most \(\tau+2\) positive coordinates. EFX is inherited because every positive cohort belongs to the original EFX support. PO follows from Corollary 3 and applies to the full competitor class specified in the task.
The denominator and bundle-coordinate bounds ensure polynomial output bit length. The argument provides exact feasibility, not merely an approximation.
Assessment: correct.
The bounds on the binary lengths of \(Q_0,H,J,\Delta,N\), the virtual populations, and the virtual supplies are valid. Their numerical magnitudes may be exponential; their representations remain polynomial in size.
The cited algorithm supports the required simulation: Claim 1 checks split allocations using a constant number of segment endpoints; Theorem 5 uses binary searches; and its proof explicitly describes constant-size interval representations for the returned constructions. The low-supply case is covered by Observation 1. These facts support valuation lookup by virtual rank and extraction of only \(O(\tau)\) cohorts. [Finite-society paper](https://ojs.aaai.org/index.php/AAAI/article/download/38723/42685)
The bit-complexity claim is also supported by the referenced formulas: iterations use bounded counts and indices, input valuations, and explicit arithmetic with floors and ceilings. The argument does not rely solely on a unit-cost arithmetic-operation bound.
Finally, the retained-support linear program has polynomially many variables and polynomial-size rational data. Polynomial-time rational linear programming with basic feasible solution extraction supplies the requested allocation.
Assessment: correct in substance.
The prover resolves all assigned questions: every valid instance admits the requested allocation; existence is therefore in \(\mathrm P\); and an allocation can be computed in polynomial time for the stipulated two-good setting.
The only required repair is an explicit treatment of the empty discarded set in Lemma 4. No counterexample or major issue was found.
⟨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.