Answer: The limiting allocation is exactly computable in polynomial time, and the welfare-threshold decision is polynomial-time solvable.
Theorem 1 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateThe approximation ratio of random priority is Θ(1/√n). Furthermore, random priority is asymptotically the best truthful-in-expectation mechanism and the best ordinal (not necessarily truthful-in- expectation) mechanism for the problem. The theorem also holds for an extension to the unit-range representation, when 0 is not required to be in the image of the function; we discuss how in Section 5.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given finite item classes \(M\), rational supplies \(\rho\in\Delta(M)\), finite complete valuation types \(T\) with normalized utilities \(u_t:M\to[0,1]\) or unit-sum utilities, a rational society distribution \(\mu\in\Delta(T)\), and a rational threshold \(r\), compute the fluid random-priority allocation \(x^{\mathrm{RP}_\infty}\) arising from integral replications \(N\mu_t\) and \(N\rho_j\), compute \(W_{\mathrm{RP}}=\sum_{t,j}x^{\mathrm{RP}_\infty}_{t,j}u_t(j)\) and \(W^*=\max\{\sum_{t,j}x_{t,j}u_t(j):\sum_jx_{t,j}=\mu_t,\ \sum_tx_{t,j}=\rho_j,\ x_{t,j}\ge0\}\), and decide whether \(W_{\mathrm{RP}}/W^*\ge r\).
Let \(M\) be finite, with rational supply shares \(\rho\in\Delta(M)\), and let \(T\) be finite, with rational type masses \(\mu\in\Delta(T)\). Each type has rational utilities \(u_t\), either in \([0,1]\) with maximum \(1\), or nonnegative with sum \(1\). Fix a strict ranking consistent with each type’s utilities to break ties.
For each eligible \(N\) with integral \(N\mu_t\) and \(N\rho_j\), uniformly order the \(N\) agents and let each take their highest-ranked available item. Let \(x^{\mathrm{RP}_\infty}_{t,j}\) be the limit of the expected number of type-\(t\) agents receiving item \(j\), divided by \(N\). Set \(W_{\mathrm{RP}}=\sum_{t,j}x^{\mathrm{RP}_\infty}_{t,j}u_t(j)\) and \(W^*=\max\{\sum_{t,j}x_{t,j}u_t(j):\sum_jx_{t,j}=\mu_t,\ \sum_tx_{t,j}=\rho_j,\ x_{t,j}\geq0\}\). Assume \(W^*>0\).
Is computing \(x^{\mathrm{RP}_\infty}\) and deciding, for rational \(r\), whether \(W_{\mathrm{RP}}/W^*\geq r\) possible in polynomial time, or is the threshold decision NP-hard?
For finite assignments, random priority has a \(\Theta(n^{-1/2})\) worst-case welfare ratio, while computing its exact allocation matrix is \(\#\mathrm{P}\)-complete. In replica economies, the continuum random-priority allocation equals the continuum probabilistic-serial allocation.
Result. Both the exact allocation \(x^{\mathrm{RP}_\infty}\) and the welfare-threshold decision are computable in polynomial time in the binary input length. In particular, the decision problem belongs to \(\mathrm{P}\); NP-hardness under polynomial-time many-one reductions would imply \(\mathrm{P}=\mathrm{NP}\).
1. Reduction to continuum probabilistic serial
Write \(m=|M|\) and \(h=|T|\). Discard zero-mass types and zero-supply items, restoring their zero rows and columns in the final output. Restrict each fixed strict ranking to the remaining items.
We use the replica-limit equivalence stated in the question: the limiting random-priority allocation is the continuum probabilistic-serial allocation. This is the relevant equivalence established by [Che and Kojima](https://www.columbia.edu/~yc2271/files/publications/psrp-Final.pdf). Its setting applies here: there are finitely many item and preference types, fixed strict rankings, and fixed masses and supplies replicated proportionally. Indeed, if \(N_0\) is the least common multiple of all denominators of \(\mu\) and \(\rho\), the eligible population sizes are exactly the positive multiples of \(N_0\).
In continuum probabilistic serial, every agent consumes at unit speed their highest-ranked remaining item. Thus a type of mass \(\mu_t\) consumes at aggregate speed \(\mu_t\). We compute aggregate masses, matching the normalization in the definition of \(x^{\mathrm{RP}_\infty}\).
2. Exact exhaustion algorithm
Initialize residual supplies \(s_j=\rho_j\), allocations \(x_{t,j}=0\), and elapsed time \(\tau=0\). While some residual supply is positive, perform the following stage.
\(q_j=\sum_{\{t:b_t=j\}}\mu_t\).
\(\delta=\min_{\{j:q_j>0\}}s_j/q_j\).
All comparisons and updates use exact rational arithmetic. Simultaneously exhausted items are all removed before the next stage.
We now prove correctness and termination.
At every stage, each positive-mass type chooses exactly one available item. Consequently, \(\sum_jq_j=\sum_t\mu_t=1\). In particular, a positive consumption rate exists. Moreover, \(q_j>0\) implies \(s_j>0\), so \(\delta>0\).
The choice of \(\delta\) makes all updated supplies nonnegative and exhausts at least one previously available item. Hence there are at most \(m\) stages.
For any time strictly before the end of a stage, none of its initially available items has been exhausted. Therefore each type continues to prefer the same item throughout that stage. The stated rates and allocation increments consequently agree exactly with continuum probabilistic serial. At the endpoint, removing all exhausted items and recomputing choices gives its next stage. Induction establishes agreement throughout the algorithm.
To verify the time horizon, initially \(\sum_js_j=1-\tau=1\). Each stage decreases total residual supply by \(\delta\sum_jq_j=\delta\), so the invariant \(\sum_js_j=1-\tau\) holds. Nonnegative residual supplies imply \(\tau\leq1\). At termination all residual supplies vanish, so \(\tau=1\).
Every type therefore consumes for total duration one, giving \(\sum_jx_{t,j}=\mu_t\). Every supply is exhausted, giving \(\sum_tx_{t,j}=\rho_j\). The output is exactly continuum probabilistic serial and, by the given equivalence, exactly \(x^{\mathrm{RP}_\infty}\).
3. Polynomial bit complexity
A polynomial number of stages alone does not establish polynomial running time: intermediate rational numbers must also have polynomial encoding length. We prove that explicitly.
Let \(L\) be the total binary input length. Choose \(Q\) as the product of the denominators of the type masses and \(R\) as the product of the denominators of the supply shares. Then all \(Q\mu_t\) and \(R\rho_j\) are integers, and \(\log_2Q+\log_2R=O(L)\).
Every stage rate has the form \(q_j=a_j/Q\), where \(a_j\) is an integer with \(0\leq a_j\leq Q\).
We maintain a common, not necessarily reduced, denominator \(D\) for all residual supplies, allocation entries, and elapsed time. Initially \(D=R\) suffices. Suppose a stage begins with this property. Write \(s_j=b_j/D\), and choose an item \(j_*\) attaining the minimum defining \(\delta\). Put \(a_*=a_{j_*}>0\) and \(b_*=b_{j_*}\). Then
\(\delta=Qb_*/(Da_*)\).
The updated residual supply of any item \(j\) is
\(s'_j=(b_ja_*-a_jb_*)/(Da_*)\).
Writing \(c_t=Q\mu_t\), the allocation increment for type \(t\) is
\(\mu_t\delta=c_tb_*/(Da_*)\).
The old entries and elapsed time can also be expressed over \(Da_*\), and the time increment has that denominator. Thus \(D'=Da_*\) is a valid new common denominator.
After \(k\leq m\) stages, we consequently have
\(D_k=R\prod_{\ell=1}^{k}a_*^{(\ell)}\), and hence
\(\log_2D_k\leq\log_2R+k\log_2Q=O((m+1)L)\).
All stored supplies, allocations, and elapsed times lie in \([0,1]\), so their numerators over this common denominator have the same polynomial bit bound. The products used for updates and rational comparisons also have polynomial bit length.
A direct implementation finds all current choices using \(O(hm)\) ranking inspections per stage and performs polynomially many arithmetic operations. There are at most \(m\) stages, and every operation involves polynomial-length integers. This proves exact polynomial-time computation of \(x^{\mathrm{RP}_\infty}\). No population of size \(N_0\) needs to be constructed.
4. Welfare optimization and exact threshold comparison
Once the allocation is known, compute
\(W_{\mathrm{RP}}=\sum_{t,j}x^{\mathrm{RP}_\infty}_{t,j}u_t(j)\)
by exact rational arithmetic. There are \(hm\) summands of polynomial encoding length, so this computation and its result have polynomial bit complexity.
The optimization defining \(W^*\) is a rational linear program with \(hm\) variables, \(h+m\) equality constraints, and nonnegativity constraints.
Its feasible set is nonempty: \(x_{t,j}=\mu_t\rho_j\) satisfies both sets of marginals. It is bounded, since every feasible entry satisfies \(0\leq x_{t,j}\leq\mu_t\leq1\). Its coefficients have polynomial encoding length because they are input rationals or integers of constant size.
The polynomial-time theorem for rational linear programming therefore applies: a finite rational optimum can be computed exactly in polynomial time in the encoding length. In particular, we can compute \(W^*\) exactly.
By the assumed strict positivity of \(W^*\), the requested condition is equivalent to
\(W_{\mathrm{RP}}-rW^*\geq0\).
This is an exact rational comparison of polynomial-length numbers, including when equality holds.
The argument applies to both utility normalizations in the question. Finite-population counting hardness does not obstruct this algorithm: the replica limit is computed through its continuum characterization, without computing finite random-priority probabilities.
⟨structured verdict parsed — rendered above⟩
The prover resolves both requested tasks. The exhaustion algorithm correctly computes the continuum allocation, its intermediate rational numbers have polynomial encoding length, and the welfare comparison uses a valid application of exact rational linear programming. I found no major or minor mathematical issues requiring repair.
The replica-limit equivalence is expressly supplied in USER_TASK, so the prover may use it without proving it again. The cited [Che–Kojima paper](https://www.columbia.edu/~yc2271/files/publications/psrp-Final.pdf) concerns the asserted asymptotic equivalence.
Removing zero-mass types and zero-supply items preserves the allocation problem. Their allocation rows or columns must be zero by nonnegativity and the marginal constraints. Restricting rankings to positive-supply items preserves choices among available items.
The statement about eligible population sizes is correct under the usual convention that rational denominators are taken in lowest terms: integrality of every replicated mass and supply is equivalent to divisibility by their least common multiple. The proof does not require constructing a population of that size.
The normalization is correct. Individual consumption speed one gives aggregate consumption speed \(\mu_t\) for type \(t\), matching allocations measured as expected counts divided by population size.
While any supply remains, every retained type has a unique highest-ranked available item. The retained masses still sum to one, hence \(\sum_j q_j=1\).
A positive-rate item necessarily has positive residual supply. Thus the minimum defining \(\delta\) is over a nonempty finite set of positive rational numbers, and \(\delta>0\).
For every item with positive rate, the minimizing property gives \(q_j\delta\leq s_j\). Zero-rate items remain unchanged. Consequently, no residual supply becomes negative, and a minimizing item is exhausted.
Exhausted items cannot subsequently be chosen. Therefore each stage removes at least one item permanently, proving the bound of at most \(m\) stages. Simultaneous exhaustion is explicitly handled.
Before the exhaustion endpoint, every initially available item remains available. Rankings are fixed, so every type’s chosen item and every aggregate rate remain constant throughout the stage. The stated allocation increments therefore match the consumption process exactly.
Recomputing choices after removing all exhausted items correctly advances the process. The induction establishing agreement is valid.
The invariant \(\sum_j s_j=1-\tau\) follows from the initial total supply and the total consumption rate. Nonnegative residual supplies imply \(\tau\leq1\), and termination implies \(\tau=1\).
Hence every retained type consumes for total duration one, establishing its row marginal \(\mu_t\). The residual-supply updates establish the column marginals \(\rho_j\). Restoring zero rows and columns completes the original allocation matrix.
The products defining \(Q\) and \(R\) have bit lengths bounded by the sum of the input denominator lengths. Their potentially large numerical values do not invalidate the polynomial bound.
Each rate has the stated form \(a_j/Q\), with \(0\leq a_j\leq Q\), because it is a sum of a subset of the type masses.
All three critical arithmetic identities are correct:
\(\delta=Qb_*/(Da_*)\),
\(s'_j=(b_ja_*-a_jb_*)/(Da_*)\), and
\(\mu_t\delta=c_tb_*/(Da_*)\).
Old allocation entries and elapsed time can also be rescaled to denominator \(Da_*\). Thus the common-denominator induction covers every stored quantity claimed.
Since \(1\leq a_*\leq Q\), the bound
\(\log_2 D_k\leq\log_2 R+k\log_2 Q\)
is valid. With at most \(m\) stages, it is polynomial in the explicit input length.
Supplies, allocations, and elapsed time all lie in \([0,1]\), so their common-denominator numerators have polynomial length as claimed. Intermediate products and cross-products for comparisons likewise have polynomial length.
The ranking scans and arithmetic-operation counts are polynomial. Thus the proof establishes polynomial running time in the binary model, rather than merely a polynomial number of arithmetic operations.
Computing \(W_{\mathrm{RP}}\) involves polynomially many rational products and sums of polynomial encoding length. The claimed exact computation bound is valid.
The transportation linear program is correctly specified. The exhibited point \(x_{t,j}=\mu_t\rho_j\) is feasible, and the row constraints imply \(0\leq x_{t,j}\leq\mu_t\), establishing boundedness.
The invoked rational-linear-programming theorem is stated sufficiently precisely for this application: a feasible, bounded linear program with explicitly encoded rational data admits exact optimal-value computation in polynomial time. The prover checks these hypotheses, and the numbers of variables and constraints are polynomial.
Since \(W^*>0\), multiplication by \(W^*\) preserves the threshold inequality. The final rational comparison therefore handles arbitrary rational \(r\), including exact equality.
Both utility normalizations are covered; neither changes the consumption algorithm or the validity of the rational objective computation. Fixed strict rankings handle utility ties.
The finite-population hardness statement does not contradict the continuum algorithm. The prover computes the supplied limiting characterization directly.
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.