← back to the atlas

d4-journals-jair-2013-0025 (d4-journals-jair-2013-0025)

Answer: Such a DSIC mechanism exists, with exact computation polynomial in \(H,\tau,K,L\) and the guarantee \(W_{\mathrm{online}}\ge\tfrac12W_{\mathrm{offline}}\).

The anchor (named result in the paper)

Theorem 6 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateThe mechanism with on-departure cancellation is 2-competitive with the op- timal offline allocation, for a setting with non-increasing marginal values.

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

The continuous mirror question, as graded

For a finite horizon \(H\), a stream of rational masses over a support of vehicle types, and per-capita supply revealed each period, can an on-departure mass mechanism allocate integral charging bundles to individuals, preserve dominant-strategy truthfulness under the paper’s limited-misreport assumptions, achieve \(W_{\mathrm{online}}\ge \tfrac12 W_{\mathrm{offline}}\), and compute its allocations and threshold payments in time polynomial in \(H,\tau,K,L\)?

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

A society is an atomless population given by its support: the list of the \(\tau\) types with positive binary-rational masses \(\mu_j\), normalized by \(\sum_j\mu_j=1\); \(\tau\) counts listed types, not all possible types. Let \(L\) be the total input bit length and \(m=H\) the number of resource periods.
A type is \(\theta_j=(v_j,a_j,d_j,r_j)\), where \(1\le a_j\le d_j\le H\), \(r_j\in\{1,\ldots,K\}\), and \(v_j\in\mathbb Q_{\ge0}^{K}\) is non-increasing. Each individual can receive at most \(K\) units in total and at most \(r_j\) units per period; its value for retaining \(q\) units is \(V_j(q)=\sum_{k=1}^{q}v_{j,k}\).
Arrival masses and fixed valuation/rate reports are revealed on arrival; departures are observed when they occur, without advance knowledge. Nonnegative binary-rational per-capita supply \(s_t\) is revealed at the start of period \(t\); unused supply expires, and future arrivals, departures, and supply are unknown.
Individuals receive integral charging quantities, but type masses may be split among different quantities and histories. In each period the integral of provisional quantities cannot exceed \(s_t\); only individuals currently present may charge.
An on-departure mechanism provisionally allocates greedily by active marginal values, subject to rate and total-demand bounds. At departure it may reclaim a terminal portion of each individual's provisional bundle; reclaimed units cannot be reassigned, and only retained units yield value.
For fixed other reports and an individual's availability/rate report, marginal thresholds \(p_1\le\cdots\le p_K\) are independent of its valuation report; a provisionally received unit \(k\) is cancelled when \(\hat v_k<p_k\), and retaining \(q\) units incurs payment \(\sum_{k=1}^{q}p_k\). Any random priorities are independent of reports; equal-valued competitors may be served by splitting their masses.
Admissible deviations satisfy \(a\le\hat a\le\hat d\le d\) and \(1\le\hat r\le r\), with arbitrary nonnegative non-increasing valuation reports. DSIC requires truthful reporting to maximize each individual's expected quasilinear utility against every profile of others' reports; an individual has zero mass, and deviations need not belong to the listed support.
Let \(W_{\mathrm{online}}\) be integrated value of retained bundles under truthful reports. Let \(W_{\mathrm{offline}}\) be maximum integrated value over all feasible integral individual charging schedules with full knowledge of the stream, allowing mass splitting.

Does there exist such a DSIC on-departure mass mechanism guaranteeing \(W_{\mathrm{online}}\ge\tfrac12W_{\mathrm{offline}}\) for every stream, with exact mass allocations and threshold payments computable in time polynomial in \(m=H,\tau,K,L\), or is this guarantee impossible under these requirements?

For finite populations, on-departure cancellation is DSIC under these limited misreports and achieves \(W_{\mathrm{online}}\ge\tfrac12W_{\mathrm{offline}}\); its implementation takes \(O(N^2r_{\max}+Nr_{\max}v_{\max}+Nv_{\max})\) operations per period. [Robu et al.](https://parkes.seas.harvard.edu/sites/g/files/omnuum8711/files/2025-05/robu_jair13.pdf)
No result settling this exact atomless, integral-bundle online mechanism question was located in the literature search.

Modeling choices made when packaging the task

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

1. Result

Such a mechanism exists. It can be implemented with exact rational mass allocations and threshold payments in time polynomial in \(H,\tau,K,L\), and it satisfies

\(W_{\mathrm{online}}\ge \tfrac12 W_{\mathrm{offline}.\)

The proof below works directly in the atomless model. The finite-population result cited in the question is established in [Robu et al., Theorem 6](https://parkes.seas.harvard.edu/sites/g/files/omnuum8711/files/2025-05/robu_jair13.pdf).

The essential simplification is that an individual’s report cannot change the aggregate allocation: an individual has zero mass. Consequently, its departure prices can be constructed from the aggregate period cutoffs without rerunning counterfactual markets.

2. Provisional allocation and period cutoffs

Represent the permitted mass splitting by giving each individual an auxiliary priority \(u\in[0,1)\), uniformly distributed within every type and independent of reports. Formally, type \(j\) has the product representation \(\{j\}\times[0,1)\), with measure \(\mu_j\,du\). An individual keeps its priority when deviating.

This is an exact mass-splitting representation. The mechanism uses the same splitting rule for every arriving cohort and does not inspect unreported departure times.

At the start of period \(t\), an individual with provisional endowment \(n\) and reported rate \(\hat r\) offers the active marginal units

\(\hat v_{n+1},\ldots,\hat v_{\min(n+\hat r,K)}.\)

Allocate greedily among these marginal units. Resolve equal values by increasing priority \(u\). Because marginal values are non-increasing, each individual’s selected units form a prefix of its active units.

The following specifies the aggregate allocation precisely.

At a boundary priority, either choice is harmless because that priority has zero mass.

Every provisionally allocated marginal unit therefore has reported value at least \(\lambda_t\). Moreover, if \(g_t\) denotes the total provisional allocation in period \(t\), then

\(\lambda_t g_t=\lambda_t s_t.\) (1)

Indeed, a positive cutoff occurs only when supply is exhausted; a zero cutoff makes both sides zero.

For any fixed profile of other reports, changing one zero-mass individual’s report changes neither \(\lambda_t\) nor the aggregate priority boundary.

3. Departure thresholds

Fix an individual’s reported window \(I=[\hat a,\hat d]\) and rate \(\hat r\). Define its opportunity multiset

\(\mathcal O(I,\hat r)=\biguplus_{t\in I:\,s_t>0}\{\lambda_t\}^{\hat r},\)

where each positive-supply period contributes \(\hat r\) copies of its cutoff. Let

\(M=\min\{K,|\mathcal O(I,\hat r)|\}.\)

For \(1\le k\le M\), let \(p_k\) be the \(k\)-th smallest element of this multiset. If \(M<K\), pad the threshold vector by setting \(p_k=p_M\) for \(k>M\); when \(M=0\), set every threshold to zero. The padded thresholds are never charged, because no individual receives more than \(M\) provisional units.

These thresholds are finite, nonnegative, non-decreasing, and independent of the individual’s valuation report. Write

\(P(q)=\sum_{k=1}^{q}p_k,\qquad P(0)=0.\)

At departure, cancel precisely the provisionally received units satisfying \(\hat v_k<p_k\). Since \(\hat v_k-p_k\) is non-increasing in \(k\), the cancelled units form a terminal portion. Charge \(P(q)\) for the retained prefix of length \(q\).

Only past cutoffs, the reported rate, and the observed reported departure are needed.

4. Truthful reporting attains the best threshold-menu utility

Fix the aggregate stream generated by everyone else’s reports. For this section, use an individual’s truthful window, rate, and valuation \(v\). Let \(n\) be its provisional quantity at departure.

Define

\(b=\max\bigl(\{0\}\cup\{k\le M:v_k>p_k\}\bigr).\)

Claim. The individual receives at least \(b\) provisional units.

To prove this, fix \(k\le M\) with \(v_k>p_k\). There are at least \(k\) opportunity slots with cutoff strictly below \(v_k\). While the individual’s endowment is below \(k\), every positive-supply period satisfying \(\lambda_t<v_k\) allocates to it at least

\(\min\{r,k-n_t\}\)

units: those active marginal values are all at least \(v_k\), hence strictly above the cutoff. Other periods cannot decrease its provisional endowment. The available slots therefore suffice to reach \(k\). Applying this to every such \(k\) proves the claim.

Let

\(Q=\max\bigl(\{0\}\cup\{k\le M:v_k\ge p_k\}\bigr).\)

The retained quantity is \(q=\min\{n,Q\}\). The claim gives \(q\ge b\). Thus the retained bundle includes every strictly positive marginal surplus and excludes every negative marginal surplus. Any additional retained units have zero marginal surplus. Consequently, truthful utility equals

\(U(v;I,r)=\max_{0\le \ell\le M}\{V(\ell)-P(\ell)\} =\sum_{k=1}^{M}\max\{v_k-p_k,0\}.\) (2)

This conclusion holds for every individual priority, including priorities that lose some cutoff ties.

Valuation deviations

With the window and rate fixed, any valuation report produces some retained quantity \(\hat q\le M\), charged \(P(\hat q)\). Its utility at the true valuation is therefore at most the maximum in (2).

Availability and rate deviations

An admissible availability/rate deviation removes periods from the opportunity multiset and possibly reduces the multiplicity contributed by each remaining period. Hence its opportunity multiset is a submultiset of the truthful one.

Let \(\hat M,\hat p_k,\hat P\) describe the deviation. Then \(\hat M\le M\), and for every \(k\le\hat M\),

\(\hat p_k\ge p_k.\)

For any retained quantity \(\hat q\le\hat M\), including one induced by an arbitrary simultaneous valuation deviation,

\(V(\hat q)-\hat P(\hat q) \le V(\hat q)-P(\hat q) \le U(v;I,r).\)

Truthful reporting attains the last expression by (2). This proves DSIC under all the permitted deviations. The argument does not require a deviation to belong to the listed support.

5. A bound on cancellation losses

Consider a truthful individual receiving \(n\) provisional units and retaining \(q\). Assign to each provisional unit the cutoff of the period in which it was charged. Let \(C_i\) be the sum of these cutoff costs.

We prove

\(C_i\le V_i(q)+P_i(q).\) (3)

Every provisional marginal unit \(k\) was allocated at a cutoff at most \(v_{i,k}\). Thus the cutoff cost of the first \(q\) units is at most \(V_i(q)\).

If \(n=q\), this already proves (3). Suppose \(n>q\). Cancellation implies

\(v_{i,q+1}<p_{i,q+1}.\)

Therefore at most \(q\) slots in the individual’s entire opportunity multiset have cutoff at most \(v_{i,q+1}\). Otherwise its \((q+1)\)-st smallest cutoff would be at most \(v_{i,q+1}\).

Every cancelled unit \(k>q\) was charged at a cutoff satisfying

\(\lambda_t\le v_{i,k}\le v_{i,q+1}.\)

The actual charging schedule maps these units into distinct opportunity slots: at most \(r_i\) units were charged in any period. Their cutoff costs are consequently bounded by the sum of all opportunity slots priced at most \(v_{i,q+1}\).

All those slots occur among the \(q\) cheapest slots. Since cutoffs are nonnegative, their sum is at most \(P_i(q)\). Combining the bounds for retained and cancelled units proves (3).

The same counting argument also gives \(n-q\le q\): at most half an individual’s provisional units are cancelled.

6. Welfare guarantee

Let

\(P_{\mathrm{on}}=\int P_i(q_i)\,d\mu(i),\qquad C=\int C_i\,d\mu(i).\)

Integrating (3) gives

\(C\le W_{\mathrm{online}}+P_{\mathrm{on}}.\) (4)

By (1),

\(C=\sum_{t=1}^{H}\lambda_t g_t =\sum_{t=1}^{H}\lambda_t s_t.\) (5)

Now consider any feasible offline schedule. Write \(z_{i,t}\) for its integral allocation to individual \(i\) in period \(t\), and \(\ell_i=\sum_t z_{i,t}\).

In a zero-supply period, feasibility and nonnegativity imply \(z_{i,t}=0\) almost everywhere. Discarding these null exceptions, each individual’s offline schedule uses \(\ell_i\) distinct slots from its opportunity multiset. Since \(P_i(\ell_i)\) is the cost of its cheapest \(\ell_i\) slots,

\(P_i(\ell_i)\le\sum_t\lambda_t z_{i,t}.\)

Equation (2) also gives

\(V_i(\ell_i)-P_i(\ell_i)\le U_i.\)

Combining these inequalities and integrating,

\(\int V_i(\ell_i)\,d\mu(i) \le \int U_i\,d\mu(i)+\sum_t\lambda_t\int z_{i,t}\,d\mu(i) \le \int U_i\,d\mu(i)+\sum_t\lambda_t s_t.\)

Truthful utility and payment satisfy

\(\int U_i\,d\mu(i)=W_{\mathrm{online}}-P_{\mathrm{on}}.\)

Using (4) and (5), every feasible offline schedule therefore has welfare at most

\(W_{\mathrm{online}}-P_{\mathrm{on}}+C \le 2W_{\mathrm{online}}.\)

Each type has finitely many integral schedules. Their mass distributions form a nonempty compact polytope, so the offline maximum is attained. Applying the preceding inequality to that maximum proves

\(\boxed{W_{\mathrm{online}}\ge\tfrac12W_{\mathrm{offline}}}.\)

7. Exact polynomial-time implementation

The use of one priority coordinate across all periods permits a compact representation.

Number of states

Maintain a common partition of \([0,1)\) by priority boundaries introduced in previous periods. Within each cell, every member of an arrival cohort has the same provisional charging history.

In a period, all strictly above-cutoff units are allocated. Equal-cutoff units are allocated exactly to individuals below one global priority boundary \(z_t\). Thus each period introduces at most one new partition endpoint.

After \(H\) periods there are at most \(H+1\) cells. There are at most \(\tau\) arrival cohorts, so there are \(O(\tau H)\) cohort-cell states. Storing their complete charging histories takes \(O(\tau H^2)\) entries.

Cohorts are formed from observed arrival information. Cohorts with identical arrival, valuation, and rate reports can be combined; their active masses are updated when departures occur. This does not require advance knowledge of departures.

Computing a period

For each active cohort-cell state, list at most \(K\) active marginal values, weighted by that cell’s mass. Sorting these weighted values identifies \(\lambda_t\).

Let \(A_t\) be the mass of marginal units strictly above \(\lambda_t\). Define

\(F_t(z)=\text{mass of active marginal units equal to }\lambda_t \text{ belonging to priorities below }z.\)

On every current partition cell, \(F_t\) is affine. Its slope is a sum of active cohort masses multiplied by integer counts of equal-cutoff units. It is continuous because each single priority has zero mass.

In the supply-constrained case, the required boundary solves

\(F_t(z_t)=s_t-A_t.\)

The cutoff definition ensures that this equation has a solution. Sweeping the partition cells finds a solution by rational arithmetic. Updating the cells then assigns integral individual quantities and exactly respects supply.

Bit complexity

Let \(D\) be a common denominator for all input masses and supplies. Taking the product of their denominators gives \(\log D=O(L)\). Every active cohort mass is an integer multiple of \(1/D\).

Suppose all existing partition endpoints have a common denominator \(R\). On a cell with positive slope, write the slope of \(F_t\) as \(B/D\). Since total population mass is one and each individual offers at most \(K\) units,

\(1\le B\le DK.\)

The boundary equation produces an endpoint whose denominator divides \(RB\). Thus a common endpoint denominator after all periods has bit length at most

\(O\bigl(H(L+\log K)\bigr).\)

Cell masses consequently have polynomial bit length. Each cutoff is either zero or an input marginal value. Thresholds are obtained by sorting at most \(HK\) cutoff copies per departing type, and payments sum at most \(K\) thresholds.

There are polynomially many states, sorting operations, and rational arithmetic operations, all on numbers of polynomial bit length. Complete charging histories, retained quantities, exact mass allocations, and threshold payments therefore have polynomial-size representations and can be computed in time polynomial in \(H,\tau,K,L\).

8. Sharpness within the required greedy class

The factor cannot be uniformly improved for mechanisms whose provisional allocation must be greedy.

Take \(H=2\), \(K=1\), supplies \(s_1=s_2=\tfrac12\), and two types of mass \(\tfrac12\):

Choose any positive binary-rational \(\varepsilon\). Greedy provisional allocation gives all first-period supply to \(A\). In period two, \(A\) has exhausted its demand and \(B\) has departed. Cancellation can only reduce welfare, so any such mechanism has

\(W_{\mathrm{online}}\le\tfrac12(1+\varepsilon).\)

Offline serves \(B\) first and \(A\) second, attaining the maximum possible value

\(W_{\mathrm{offline}}=1+\tfrac12\varepsilon.\)

Hence the ratio is at most

\(\dfrac{1+\varepsilon}{2+\varepsilon},\)

which approaches \(\tfrac12\) as \(\varepsilon\) decreases to zero.

⟨structured verdict parsed — rendered above⟩

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

The construction settles the intended atomless problem. The incentive argument, cancellation bound, welfare comparison, and polynomial bit-complexity argument are sound as written. I found one minor typographical issue and no major mathematical issue.

The prover claims existence of a DSIC mechanism with integral individual quantities, exact rational mass splitting, and polynomial computation. Its argument addresses these requirements directly.

The cited finite-population theorem is correctly identified: Theorem 6 states a competitive guarantee for on-departure cancellation with non-increasing marginal values. The prover does not use this theorem to justify passage to an atomless population; its atomless proof is independent. Consequently, there is no unverified transfer from the finite model. [Robu et al., Theorem 6](https://parkes.seas.harvard.edu/sites/g/files/omnuum8711/files/2025-05/robu_jair13.pdf)

The product representation gives each listed type a uniform priority coordinate and preserves its total mass. The allocation rule uses reported valuations, reported rates, current presence, provisional quantities, and priorities. It does not use an unobserved departure date.

On a fixed priority cell, individuals with the same arrival, valuation, and rate reports have identical provisional histories. This remains true when departure groups are distinguished afterward: uniformity within each true type ensures that departures remove the corresponding mass uniformly across priority cells.

Non-increasing valuations make the strictly above-cutoff units a prefix of the active marginals. Selecting all cutoff-valued units below a common priority boundary preserves that prefix property. Choices at the boundary concern zero mass.

The identity
\[ \lambda_t g_t=\lambda_t s_t \]
is valid in every specified case. A positive cutoff requires exhausted supply; when the cutoff is zero, both products vanish.

Changing one zero-mass individual’s report does not change the aggregate marginal-unit distribution or its cutoff and priority boundary. This is the independence needed in the subsequent incentive argument.

Each positive-supply period contributes exactly the reported rate’s number of opportunity slots. Every actual provisional schedule uses distinct such slots, so its total quantity is at most
\[ M=\min\{K,|\mathcal O(I,\hat r)|\}. \]

The sorted thresholds are nonnegative and non-decreasing. Their construction depends on the aggregate cutoffs and the individual’s availability/rate report, but not its valuation report.

Padding beyond \(M\) has no effect because those indices cannot be provisionally received. The case \(M=0\) is also covered.

Since reported marginal values decrease and thresholds increase, the differences
\[ \hat v_k-p_k \]
are non-increasing. Cancelling exactly the negative differences therefore cancels a terminal portion, as required.

The key provisional-allocation claim is valid. If
\[ v_k>p_k, \]
at least \(k\) opportunity slots have cutoff strictly below \(v_k\). Whenever the individual has fewer than \(k\) units, the active marginals needed to reach \(k\), up to its period rate, are strictly above that period’s cutoff and must be allocated. The chronological allocation therefore reaches \(k\).

The strict inequality is used correctly: the claim does not assume that a losing cutoff tie will be served.

Because marginal surpluses are non-increasing, the retained bundle contains every strictly positive surplus, contains no negative surplus, and may contain zero-surplus units. Thus the claimed equality
\[ U(v;I,r) =\max_{0\le \ell\le M}\{V(\ell)-P(\ell)\} =\sum_{k=1}^{M}\max\{v_k-p_k,0\} \]
follows.

For a valuation deviation with fixed availability and rate, the resulting retained quantity remains an option in this same menu. Its true utility cannot exceed the truthful maximum.

An admissible availability/rate deviation removes opportunity slots. Hence
\[ \hat M\le M,\qquad \hat p_k\ge p_k \quad\text{for }k\le\hat M. \]
The comparison of utilities remains valid for simultaneous valuation deviations. This covers deviations outside the listed support.

The proof establishes utility maximization for every priority realization, which is sufficient for the required expected-utility DSIC condition.

The bound
\[ C_i\le V_i(q)+P_i(q) \]
is justified.

Each retained provisional unit was charged at a cutoff at most its truthful marginal value, so retained cutoff costs sum to at most \(V_i(q)\).

If cancellation occurs, then \(q+1\le n\le M\), so the threshold used in
\[ v_{i,q+1}<p_{i,q+1} \]
is an actual order statistic, not a padded entry. This inequality implies that at most \(q\) opportunity slots have cutoff at most \(v_{i,q+1}\).

Every cancelled unit uses a distinct slot with cutoff at most that value. All such slots lie among the \(q\) cheapest slots, and nonnegative cutoffs make their total cost at most \(P_i(q)\).

The additional conclusion
\[ n-q\le q \]
follows from the same count. In particular, the argument also handles \(q=0\): cancellation of a positive provisional quantity would contradict the slot count.

The treatment of zero-supply periods is correct. Offline quantities must vanish almost everywhere in each such period; the finite union of these null exceptions can be discarded.

An offline schedule therefore uses distinct opportunity slots and satisfies \(\ell_i\le M_i\). Its cutoff cost is at least the cost of its cheapest \(\ell_i\) slots:
\[ P_i(\ell_i)\le\sum_t\lambda_t z_{i,t}. \]
The truthful menu maximum also gives
\[ V_i(\ell_i)-P_i(\ell_i)\le U_i. \]

Integrating these inequalities and applying supply feasibility yields the stated offline welfare bound. The substitutions
\[ C=\sum_t\lambda_t s_t,\qquad \int U_i\,d\mu(i)=W_{\mathrm{online}}-P_{\mathrm{on}} \]
are valid. Together with the cancellation-cost bound, they establish
\[ W_{\mathrm{offline}}\le 2W_{\mathrm{online}}. \]

The attainment statement is also justified: each type has finitely many integral schedules, and distributions over those schedules subject to the mass and supply constraints form a nonempty compact polytope.

The state bound follows from the specified tie rule. Each constrained period introduces at most one global priority endpoint; other allocations are constant within existing cells. Thus there are at most \(H+1\) cells and \(O(\tau H)\) cohort-cell states.

Unknown departures do not invalidate this representation. Histories depend on observable arrival, valuation, and rate information. Departures update active cohort densities when observed, without requiring departure information earlier.

The weighted sorting procedure identifies the period cutoff. The cutoff-tie mass function is continuous and affine on every current cell, so the boundary equation can be solved exactly by the stated rational sweep.

The denominator calculation is correct. With input common denominator \(D\) and endpoint common denominator \(R\), the boundary equation has residual denominator dividing \(DR\). Dividing by a positive slope \(B/D\) produces an endpoint denominator dividing \(RB\). The bound
\[ 1\le B\le DK \]
follows from total population mass one and at most \(K\) active units per individual. Over \(H\) periods, the stated polynomial bound on endpoint bit lengths follows.

Cutoffs are zero or input marginal values. Sorting at most \(HK\) opportunity copies per departing type and summing at most \(K\) thresholds also uses polynomial arithmetic and bit lengths. The claimed exact allocation and payment representations are therefore supported.

The two-type example is feasible and its calculations are correct. Greedy provisional allocation exhausts type \(A\)’s demand in period one, leaving no eligible unmet demand in period two. Offline serves \(B\) first and \(A\) second.

The resulting upper bound
\[ \frac{1+\varepsilon}{2+\varepsilon} \]
tends to one half as positive binary-rational \(\varepsilon\) tends to zero. This supports the stated sharpness within the required greedy class.

In Section 1, the first displayed welfare inequality has an unclosed subscript group in its LaTeX source. The intended inequality is unambiguous and appears correctly later.

Severity: minor. Correct that expression to
\[ W_{\mathrm{online}}\ge\tfrac12W_{\mathrm{offline}}. \]
No additional mathematical 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.