Answer: —
Theorem 4 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateDYNAMIC DRF satisfies SI, DEF, DPO, and SP, and can be implemented in polyno- mial time.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given \(m\) resources, \(K\) ordered arrival cohorts with rational masses \(\rho_1,\ldots,\rho_K\) summing to \(1\), normalized positive demand vectors \(d^1,\ldots,d^K\in\mathbb{Q}_{>0}^m\), and \(q_k=\sum_{\ell\le k}\rho_\ell\), compute at each epoch \(k\) an irrevocable per-unit allocation \(a^k_\ell=y^k_\ell d^\ell\) maximizing \(M_k\) subject to \(y^k_\ell\ge M_k\), \(y^k_\ell\ge y^{k-1}_\ell\) for \(\ell<k\), and \(\sum_{\ell\le k}\rho_\ell y^k_\ell d^\ell_r\le q_k\) for every resource \(r\); determine whether the rule satisfies continuum analogues of SI, DEF, DPO, and a specified strategyproofness notion in time polynomial in \(m\), \(K\), and encoding length \(L\).
For each cohort \(k\), \(d^k\in\mathbb{Q}_{>0}^m\) is normalized by \(\max_r d^k_r=1\); a unit mass of that cohort receiving \(y d^k\) has utility \(y\). At epoch \(k\), choose \(y^k_1,\ldots,y^k_k,M_k\) maximizing \(M_k\), subject to \(y^k_\ell\ge M_k\), \(y^k_\ell\ge y^{k-1}_\ell\) for \(\ell<k\), and \(\sum_{\ell\le k}\rho_\ell y^k_\ell d^\ell_r\le q_k\) for every \(r\).
SI means \(y^k_\ell\ge1\). DEF means that if type \(i\) prefers type \(j\)'s epoch-\(k\) allocation, then \(j<i\) and \(y^k_j=y^{i-1}_j\). DPO means no feasible allocation using at most \(q_k\) of every resource Pareto-dominates the epoch-\(k\) allocation. Strategyproofness means no cohort can obtain strictly higher true utility at any epoch by reporting another normalized demand vector, holding all other reports fixed.
Target. Is computing this continuous Dynamic-DRF rule and deciding whether it satisfies SI, DEF, DPO, and strategyproofness solvable in time polynomial in \(m\), \(K\), and \(L\), or is it NP-hard?
Nearest known results. For a finite sequence of \(n\) unit-mass agents, Dynamic DRF satisfies SI, DEF, DPO, and strategyproofness and is implementable in polynomial time. No result for the stated cohort-mass formulation was verified.
1. Result and a specification issue
Under the standard DRF interpretation, the cohort formulation is polynomial-time solvable. Positive rational cohort masses do not introduce an integer optimization problem. Moreover:
I prove these statements directly below, without replacing cohorts by unit agents.
The qualification matters: the question specifies utilities only on bundles proportional to a cohort’s true demand. DEF and strategyproofness also require utilities on other bundles. The proof uses the standard extension
\(u_i(x)=\min_{1\le r\le m}x_r/d^i_r.\)
I also assume that the masses \(\rho_i>0\) and capacities \(q_k\ge0\) are rational input data, and that capacities are nondecreasing and fixed independently of reports. Let \(L\) include their binary encoding lengths. These assumptions make the rule well-defined on every admissible report profile.
2. Unique allocation at each epoch
Fix an epoch \(k\). Write
\(a_{\ell r}=\rho_\ell d^\ell_r,\qquad b_\ell=y^{k-1}_\ell\ \text{for }\ell<k,\qquad b_k=0.\)
For \(t\ge0\), define
\(F_r(t)=\sum_{\ell=1}^k a_{\ell r}\max\{b_\ell,t\}.\)
The previous allocation, extended by zero for the new cohort, is feasible: its resource consumption is at most \(q_{k-1}\le q_k\). Thus \(F_r(0)\le q_k\).
Each \(F_r\) is continuous, piecewise linear, and strictly increasing on the nonnegative real numbers. Strict increase follows because the new cohort contributes \(a_{kr}t\), with \(a_{kr}>0\). Also, \(F_r(t)\) tends to infinity. Consequently, there is a unique nonnegative number \(t_r\) satisfying
\(F_r(t_r)=q_k.\)
Set \(t_*=\min_r t_r\). Then the unique optimal allocation is
\(M_k=t_*,\qquad y^k_\ell=\max\{b_\ell,t_*\}.\)
To prove optimality, any feasible allocation with objective value \(M\ge0\) must satisfy \(y_\ell\ge\max\{b_\ell,M\}\). Therefore \(F_r(M)\le q_k\) for every resource, which implies \(M\le t_*\). Conversely, the displayed allocation is feasible and attains \(t_*\).
For uniqueness, choose a resource \(r_*\) with \(t_{r_*}=t_*\). The displayed allocation uses exactly \(q_k\) of that resource. Every feasible optimizer must be componentwise at least the displayed allocation. Increasing any component strictly increases consumption of resource \(r_*\), because every \(a_{\ell r_*}\) is positive. Hence no component can be larger.
In particular, every epoch saturates at least one resource, and
\(y^k_k=M_k,\qquad y^k_\ell=\max\{y^{k-1}_\ell,M_k\}\quad(\ell<k).\)
3. Exact polynomial-time computation
Sort the breakpoints \(b_\ell\). Between consecutive breakpoints, let \(A\) be the indices whose allocations equal the common level \(t\). On that interval,
\(F_r(t)=t\sum_{\ell\in A}a_{\ell r}+\sum_{\ell\notin A}a_{\ell r}b_\ell.\)
Thus the candidate root on that interval is
\(t=\dfrac{q_k-\sum_{\ell\notin A}a_{\ell r}b_\ell}{\sum_{\ell\in A}a_{\ell r}}.\)
The denominator is positive because \(A\) includes the new cohort. Scanning the intervals finds each \(t_r\), after which one takes their minimum. Sorting and scanning require \(O(k\log k+mk)\) rational arithmetic operations per epoch.
It remains to justify polynomial *bit* complexity; iterating rational programs alone would not establish this.
Choose a common denominator \(D\) for all input coefficients \(a_{\ell r}\) and capacities \(q_k\), and write
\(a_{\ell r}=A_{\ell r}/D,\qquad q_k=B_k/D,\)
where the integers involved have polynomial encoding length.
Suppose all previous allocation levels have a common denominator \(H\), so \(b_\ell=V_\ell/H\). A candidate level then has the form
\(t=\dfrac{B_kH-\sum_{\ell\notin A}A_{\ell r}V_\ell}{H\sum_{\ell\in A}A_{\ell r}}.\)
For the selected level, put \(S=\sum_{\ell\in A}A_{\ell r}\). All updated allocations have the common denominator \(HS\). The binary length of \(S\) is polynomial in the input length; hence the binary length of the maintained common denominator grows by only a polynomial amount at each epoch.
Numerators also have polynomial length. Indeed, normalization provides a coordinate with \(d^\ell_r=1\), and feasibility and nonnegativity imply
\(0\le y^k_\ell\le q_k/\rho_\ell.\)
Combining this magnitude bound with the denominator bound proves that every arithmetic operation uses polynomially many bits. The entire allocation sequence is therefore exactly computable in time polynomial in \(m,K,L\).
4. A structural lemma
Repeated application of the update formula gives
\(y^k_i=\max_{i\le s\le k}M_s.\)
Consequently, for \(j>i\),
\(y^k_j\le y^k_i.\)
For \(j<i\), the same recurrence gives
\(y^k_j=\max\{y^{i-1}_j,y^k_i\}.\)
Thus we have the following implication, independent of the masses:
\(y^k_j>y^k_i\quad\Longrightarrow\quad j<i\ \text{and}\ y^k_j=y^{i-1}_j.\)
This lemma supplies both DEF and the central step of strategyproofness.
5. DEF and DPO
For DEF, the utility that cohort \(i\) assigns to cohort \(j\)’s per-unit bundle is
\(u_i(y^k_jd^j)=y^k_j\min_r(d^j_r/d^i_r).\)
Choose a coordinate \(r\) with \(d^i_r=1\). Since \(d^j_r\le1\), the minimum ratio is at most one. Therefore
\(u_i(y^k_jd^j)\le y^k_j.\)
Strict preference for \(j\)’s bundle implies \(y^k_j>y^k_i\). The structural lemma then gives exactly \(j<i\) and \(y^k_j=y^{i-1}_j\), as required.
For DPO, choose a saturated resource \(r_*\). Suppose alternative per-unit bundles \(x^\ell\) Pareto-dominate the allocation. Under the stated utility function, maintaining cohort \(\ell\)’s utility requires
\(x^\ell_r\ge y^k_\ell d^\ell_r\quad\text{for every }r.\)
Strictly improving some cohort \(h\) requires strict inequality for every coordinate of that cohort, since \(d^h_r>0\). Because \(\rho_h>0\), aggregate consumption of resource \(r_*\) would then be strictly greater than
\(\sum_{\ell\le k}\rho_\ell y^k_\ell d^\ell_{r_*}=q_k.\)
This contradicts feasibility. Hence DPO holds.
6. Strategyproofness
Fix a cohort \(i\), its true demand \(d^i\), and an alternative normalized report \(\widehat d^i\). Hold all other reports, masses, and capacities fixed. Use hats for the resulting allocation sequence.
Define
\(c=\min_r\widehat d^i_r/d^i_r.\)
Positivity gives \(c>0\). Choosing a coordinate where \(d^i_r=1\) shows \(c\le1\). Cohort \(i\)’s true utility under its alternative report is
\(u_i(\widehat y^k_i\widehat d^i)=c\widehat y^k_i.\)
Suppose, toward a contradiction, that \(h\ge i\) is the first epoch with
\(c\widehat y^h_i>y^h_i.\)
If \(h=i\), the arrival formula gives \(\widehat y^h_i=\widehat M_h\).
If \(h>i\), cohort \(i\)’s reported allocation must increase at epoch \(h\). Otherwise, by the choice of \(h\) and irreversibility,
\(c\widehat y^h_i=c\widehat y^{h-1}_i\le y^{h-1}_i\le y^h_i,\)
a contradiction. The update formula again gives \(\widehat y^h_i=\widehat M_h\).
Since \(c\le1\) and allocations are nonnegative, it follows that
\(\widehat M_h=\widehat y^h_i>y^h_i.\)
We now show that every other cohort receives at least its original allocation level at epoch \(h\).
Meanwhile, cohort \(i\)’s resource consumption strictly increases in every coordinate:
\(\widehat y^h_i\widehat d^i_r\ge c\widehat y^h_i d^i_r>y^h_i d^i_r.\)
All other cohorts’ resource consumption weakly increases. The original epoch-\(h\) allocation saturates some resource, so the deviating allocation exceeds its capacity. This contradiction proves strategyproofness at every epoch.
The proof treats the entire positive mass \(\rho_i\) as the deviating cohort.
7. SI: exact checks and a universal characterization
For a fixed profile, the new cohort receives the minimum level \(M_k\). Hence SI at epoch \(k\) is equivalent to \(M_k\ge1\), or equivalently,
\(\sum_{\ell<k}\rho_\ell d^\ell_r\max\{y^{k-1}_\ell,1\}+\rho_kd^k_r\le q_k\quad\text{for every }r.\)
This is an exact polynomial-time check.
For SI on every demand profile, the exact condition is
\(q_k-q_{k-1}\ge\rho_k\quad\text{for every }k,\qquad q_0=0.\)
Sufficiency. Inductively suppose all previous cohorts have utility at least one. Keeping their previous allocations and assigning utility one to the new cohort consumes at most
\(q_{k-1}+\rho_kd^k_r\le q_{k-1}+\rho_k\le q_k\)
of resource \(r\). Thus the epoch program admits \(M_k\ge1\). The same argument starts the induction at epoch one.
Necessity. Consider the admissible profile \(d^\ell=(1,\ldots,1)\) for every cohort. At epoch \(k-1\), saturation means the aggregate allocated amount is exactly \(q_{k-1}\) on every resource. Irreversibility preserves at least that amount. Giving the new cohort utility at least one requires at least \(\rho_k\) additional units of every resource. Therefore SI requires \(q_k\ge q_{k-1}+\rho_k\). At epoch one it requires \(q_1\ge\rho_1\).
Thus, under the explicit assumptions above, deciding universal satisfaction of all four properties reduces to checking these capacity inequalities.
8. What remains unspecified in the literal statement
The utility extension is substantive. Utilities on demand rays alone do not imply strategyproofness.
For example, take two unit-mass cohorts, two resources, \(q_1=1\), \(q_2=2\), and
\(d^1=(1,1),\qquad d^2=(1,1/2).\)
The truthful rule gives both cohorts level one at epoch two. Reporting \(\widehat d^2=(1/2,1)\) also gives both reported levels one.
Now define cohort two’s true utility by \(v_2(x)=2x_2\). This satisfies every specified on-ray equality:
\(v_2(yd^2)=y.\)
Nevertheless, its truthful bundle has utility one, while its misreported bundle has utility two. Thus the on-ray utility specification permits a profitable deviation. Under Leontief utility, the preceding theorem instead proves that no profitable deviation exists.
Accordingly, the mathematical result for the standard cohort model is complete, but applying it unconditionally to the literal question requires confirming the missing utility and input assumptions.
⟨structured verdict parsed — rendered above⟩
The conditional theorem is correct: under the explicitly stated Leontief utility and input assumptions, the allocation sequence and the stated property decisions are computable in polynomial time. The literal target remains unresolved because it does not supply those assumptions. The prover correctly acknowledges this limitation and claims only partial resolution.
The prover explicitly assumes:
These assumptions are used substantively. The utility extension determines the comparisons in DEF, DPO, and strategyproofness. Nondecreasing capacities ensure that previous allocations remain feasible. Rational encoding is needed for the claimed bit complexity.
Major scope issue: These are additional hypotheses, not consequences of the literal task. This does not invalidate the conditional proof, but it prevents an unconditional answer to the requested classification.
The argument is correct under those assumptions.
The previous allocation, extended by zero, is feasible. For every resource, \(F_r\) is continuous and strictly increasing on the nonnegative domain because the new cohort contributes a term with strictly positive slope. Its initial value is at most capacity, and it is unbounded. Consequently, the asserted unique root exists, including when it is zero.
Taking the minimum resource root gives a feasible allocation. Every feasible allocation with a nonnegative objective must dominate the corresponding componentwise lower bounds, so its objective cannot exceed that minimum root. Considering only nonnegative objectives is sufficient because objective zero is feasible.
The uniqueness proof also holds: at a saturated resource, every allocation coefficient is strictly positive. Any strict component increase above the displayed optimizer would violate that resource constraint.
No gap found.
The breakpoint algorithm is valid. Sorting once and updating the slope and intercept while scanning supports the stated arithmetic-operation bound. Tied breakpoints and a root at zero require only routine endpoint handling.
The denominator argument correctly addresses the risk of growth across epochs:
The numerator bound is justified by normalization and feasibility: a coordinate with demand one gives \(y^k_\ell\le q_k/\rho_\ell\). Together with the denominator bound, this bounds the binary lengths of maintained allocations. The displayed formulas also give polynomial-length intermediate candidates.
No gap found under the stated encoding assumptions.
Iterating the update formula gives the asserted maximum over levels since arrival. The index ranges establish that later arrivals cannot have larger current levels than earlier arrivals.
For \(j<i\), splitting the recurrence at epoch \(i-1\) gives the displayed identity. If \(y^k_j>y^k_i\), that identity forces \(y^k_j=y^{i-1}_j\).
No gap found.
Under Leontief utility, the cross-bundle utility formula is correct. Normalization of both demand vectors ensures that the minimum coordinate ratio is at most one. Therefore strict preference implies a strictly larger allocation level, and the structural lemma gives exactly the two required conclusions.
No gap found under the utility assumption.
Under Leontief utility, preserving a cohort’s utility requires every resource coordinate to remain at least its original proportional amount. Strictly increasing utility requires every coordinate to increase strictly.
Positive cohort mass then makes aggregate consumption strictly larger at the original saturated resource. This contradicts feasibility even when alternatives are arbitrary per-unit bundles, rather than proportional bundles.
No gap found under the utility assumption.
The first-profitable-epoch argument is valid.
The conversion factor satisfies \(0<c\le1\), and true utility under the alternative report is exactly \(c\widehat y^k_i\). At the first profitable epoch, the deviating cohort must receive the current reported minimum level: this follows immediately at arrival, and thereafter follows from irreversibility and the absence of an earlier gain.
The two cases for other cohorts are exhaustive. Cohorts with original levels at most the deviator’s original level receive strictly larger levels in the deviating history. Cohorts with larger original levels must be earlier arrivals frozen at their pre-deviation levels, which the deviating history preserves.
The deviator’s bundle increases strictly in every resource coordinate, while every other cohort’s consumption weakly increases. Saturation yields the contradiction.
This proves the stated guarantee for a whole-cohort demand-report deviation with fixed mass and capacities. No gap found.
For a fixed profile, the arrival cohort receives the minimum level, so SI is equivalent to \(M_k\ge1\). The displayed resource inequalities are exactly the feasibility test at level one.
The universal characterization is also correct:
The epoch-one base case is explicitly covered. Zero capacities do not invalidate the argument; they simply make SI fail when relevant.
No gap found.
The calculation is correct. Under both truthful and alternative reports, epoch two gives both reported levels one. With \(v_2(x)=2x_2\), the truthful bundle has utility one and the alternatively reported bundle has utility two, while \(v_2(yd^2)=y\).
Thus the literal on-ray specification permits the claimed profitable deviation. This demonstrates that the missing utility extension is substantive. It does not refute the conditional Leontief theorem.
Major issue 1: Specify utilities on arbitrary bundles, or explicitly authorize the Leontief extension. Otherwise the requested preference and manipulation properties are not determined by the supplied data.
Major issue 2: Confirm the input domains, rational encoding, capacity monotonicity, and report independence assumed by the prover. If those assumptions are not intended, the write-up must address the actual input model and any infeasible epochs.
No additional mathematical lemma or repair is needed for the conditional theorem as written. The remaining obstacles concern whether that theorem addresses the intended task.
⟨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.