← back to the atlas

d4-conf-wine-2008-0064 (d4-conf-wine-2008-0064)

Answer: \(\mathrm P\)

The anchor (named result in the paper)

Theorem 4 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateWhen the valuations of the agents have scaling based correlation, for any p and n > p+1, the linear redistribution mechanism obtained by solving LP (9) is worst case optimal among all Groves redistribution mechanisms that are feasible, individually rational, deterministic, and anonymous.

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

The continuous mirror question, as graded

Given a finite value set \(V\), a society distribution \(\mu\) over \(V\), slot-quality classes with per-capita capacities \(\kappa_j\), and qualities \(\alpha_1\ge\cdots\ge\alpha_q>0\), choose a rank-weight measure \(\lambda\) to maximize \(e\) subject, for every \(\mu\), to \(0\le R_\lambda(\mu)\le T_a(\mu)\) and \(R_\lambda(\mu)\ge eT_a(\mu)\), where \(R_\lambda(\mu)=\int_0^1 Q_\mu(u)\,d\lambda(u)\) and \(T_a\) is the per-capita limit of finite-auction Clarke surplus. Define tagged-agent allocation and payment by the corresponding finite-agent limit and require unilateral DSIC.

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

Let \(V\subset\mathbb Q_{\ge0}\) be finite, containing zero and a positive value, with \(m=|V|\). A society is given by its support: the list of its \(\tau\) positive-mass types, each mass a binary rational; masses sum to one. Thus \(\tau\) is the support size, not the number of possible types.
There are \(q\) slot classes with binary-rational capacities \(\kappa_j>0\) and qualities \(\alpha_1\ge\cdots\ge\alpha_q>0\); put \(s_j=\sum_{h=1}^j\kappa_h\), require \(s_q<1\), and set \(\alpha_{q+1}=0\). Agents have unit demand, value \(\alpha_jv\) for class \(j\), and have quasilinear utility.
Write \(Q_\mu\) for the descending, right-continuous quantile on \([0,1)\), with \(Q_\mu(1)=\min\operatorname{supp}\mu\). Define the per-capita Clarke surplus by \(T_a(\mu)=\sum_{j=1}^q s_j(\alpha_j-\alpha_{j+1})Q_\mu(s_j)\).
For a tagged agent, fix a bid-independent tie priority \(z\in(0,1)\), uniformly distributed across each type's mass. Reporting \(b\in V\) gives rank \(u=\mu(\{v>b\})+z\mu(\{b\})\), quality \(A_\mu(b,z)=\sum_{j:u<s_j}(\alpha_j-\alpha_{j+1})\), and Clarke payment \(P_\mu(b,z)=\sum_{j:u<s_j}(\alpha_j-\alpha_{j+1})Q_\mu(s_j)\). These specify the finite-agent limit using the larger-rank side at every cutoff; a unilateral report leaves \(\mu\) fixed.
Choose one finite signed Borel measure \(\lambda\) on \([0,1]\), independent of \(\mu\). Every agent receives the same rebate \(R_\lambda(\mu)=\int_0^1Q_\mu(u)\,d\lambda(u)\), and pays \(P_\mu(b,z)-R_\lambda(\mu)\). Require unilateral DSIC for every fixed priority, nonnegative rebates, and weak budget balance.
Given a binary-rational threshold \(\eta\in[0,1]\), is deciding whether there exist \(\lambda\) and \(e\in[\eta,1]\) satisfying \(0\le R_\lambda(\mu)\le T_a(\mu)\) and \(R_\lambda(\mu)\ge eT_a(\mu)\) for every rational-mass society on \(V\), with the stated DSIC requirement, in \(\mathrm P\) or \(\mathrm{NP}\)-hard? State running times in \(m,\tau,q\) and total binary input length \(L\).
For finite scaling-based assignment with \(n>p+1\), an LP computes linear rebates claimed to be worst-case optimal among feasible, individually rational, deterministic, anonymous Groves redistribution mechanisms; the [journal version](https://arxiv.org/pdf/1401.3884) retains this result. No result settling this exact mass-and-tagged-agent decision problem was identified in the search.

Modeling choices made when packaging the task

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

Result and interpretation

The decision problem is in \(\mathrm P\). For a tagged agent belonging to a positive-mass type of the society, every valid instance is feasible, with optimal guarantee \(e=1\).

I use “tagged agent” in this population sense: its true value belongs to \(\operatorname{supp}\mu\), while its report may be any element of \(V\), including an absent type. Section 5 also resolves the stronger interpretation allowing hypothetical true types absent from the society.

The immediate witness is an atomic measure representing the surplus itself. The substantive verification is DSIC, especially at exact cutoffs.

1. A universal rebate measure

Put \(\Delta_j=\alpha_j-\alpha_{j+1}\). By the quality ordering, \(\Delta_j\ge 0\). Let \(\delta_x\) denote the unit Dirac measure at \(x\), and choose

\(\displaystyle \lambda_*=\sum_{j=1}^{q}s_j\Delta_j\,\delta_{s_j}.\)

This is a finite nonnegative Borel measure on \([0,1]\), depending only on the slot parameters. In particular, it is independent of \(\mu\). Its total mass satisfies

\(\displaystyle \lambda_*([0,1])=\sum_{j=1}^{q}s_j\Delta_j\le\sum_{j=1}^{q}\Delta_j=\alpha_1.\)

For every society, integration against this atomic measure gives exactly

\(\displaystyle R_{\lambda_*}(\mu)=\sum_{j=1}^{q}s_j\Delta_jQ_\mu(s_j)=T_a(\mu).\)

All summands are nonnegative. Consequently, choosing \(e=1\) satisfies

\(\displaystyle 0\le R_{\lambda_*}(\mu)\le T_a(\mu),\qquad R_{\lambda_*}(\mu)\ge eT_a(\mu)\)

for every rational-mass society and every supplied \(\eta\in[0,1]\).

This conclusion uses the stated allowance of arbitrary finite signed Borel measures, which includes atomic nonnegative measures.

2. DSIC, including cutoff equalities and absent reports

Fix a society \(\mu\), a true value \(v\in\operatorname{supp}\mu\), and a priority \(z\in(0,1)\). Write

\(\displaystyle H(x)=\mu(\{w>x\}),\qquad M(x)=\mu(\{x\}),\qquad u(b)=H(b)+zM(b).\)

For each cutoff, put \(t_j=Q_\mu(s_j)\). Right continuity of the descending finite-support quantile implies

\(\displaystyle H(t_j)\le s_j<H(t_j)+M(t_j).\)

Indeed, the quantile equals a support value \(t\) on the half-open interval \([H(t),H(t)+M(t))\). Thus equality at the left endpoint uses the stipulated larger-rank side.

We now check truthful allocation separately for each quality increment.

\(\displaystyle u(v)=H(v)+zM(v)<H(v)+M(v)\le H(t_j)\le s_j.\)

Truth-telling therefore wins this increment.

\(\displaystyle u(v)\ge H(v)\ge H(t_j)+M(t_j)>s_j.\)

Truth-telling therefore loses this increment.

Because a unilateral report leaves \(\mu\) fixed, the rebate is report-independent. Utility from reporting \(b\) is therefore

\(\displaystyle U(v;b,z)=R_\lambda(\mu)+\sum_{j=1}^{q}\Delta_j(v-t_j)\mathbf 1_{\{u(b)<s_j\}}.\)

For each \(j\), truth-telling selects the increment whenever its coefficient is positive and rejects it whenever its coefficient is negative. When the coefficient is zero, either selection is optimal. Thus every summand under truth-telling is at least its value under any report \(b\in V\). Summing proves

\(\displaystyle U(v;v,z)\ge U(v;b,z)\qquad\text{for every }b\in V.\)

The argument permits reports with \(M(b)=0\), and holds for every fixed \(z\in(0,1)\). Hence the stipulated mechanism is DSIC for supported tagged agents, for any report-independent rebate—and specifically for \(\lambda_*\).

3. Budget balance and optimality

Within each positive-mass type, uniform priority maps agents uniformly onto that type’s rank interval. These intervals partition \([0,1)\), apart from endpoints of population measure zero. Therefore population rank is uniform, and the fraction receiving increment \(j\) is exactly \(s_j\).

Since each recipient pays \(\Delta_jt_j\) for that increment, aggregate per-capita Clarke payment is

\(\displaystyle \sum_{j=1}^{q}s_j\Delta_jt_j=T_a(\mu).\)

Giving every agent rebate \(T_a(\mu)\), in a population of total mass one, makes aggregate net payment zero. Thus weak budget balance holds with equality.

The guarantee \(e=1\) is optimal because the admissible interval already requires \(e\le1\). It is also nonvacuous: for any positive \(h\in V\), the society \(\mu=\delta_h\) has

\(\displaystyle T_a(\delta_h)=h\sum_{j=1}^{q}s_j\Delta_j>0,\)

since \(s_q>0\) and \(\Delta_q=\alpha_q>0\).

4. Running times and the finite-agent comparison

For inputs promised to satisfy the hypotheses, the decision algorithm simply returns YES. This takes constant time after input access, or \(\mathcal O(L)\) time if the entire encoding is read.

An explicit witness consists of at most \(q\) rational atoms and \(e=1\). Computing cumulative capacities and atom weights requires \(\mathcal O(q)\) rational arithmetic operations. Each intermediate number has \(\mathcal O(L)\) bits; a conservative schoolbook bound is \(\mathcal O(qL^2)\) bit operations and \(\mathcal O(qL)\) output bits.

There is no enumeration over the \(m\) values or over support sizes \(\tau\). If one separately evaluates the constructed rebate on a supplied society, sorting its \(\tau\) support values and scanning the cumulative masses against the \(q\) cutoffs takes \(\mathcal O(\tau\log(\tau+1)+q)\) rational operations. With \(L\) including that society’s encoding, a conservative bit bound is \(\mathcal O((\tau\log(\tau+1)+q)L^2)\).

The cited finite-agent paper’s Section 4.1 constructs rebates from the other agents’ reports, and Theorem 4 states its scaling-based optimality result. [Gujar and Narahari, journal version](https://arxiv.org/pdf/1401.3884). Here, by explicit assumption, even the full-population surplus is unchanged by a unilateral report. That assumption makes the exact-surplus rebate report-independent and explains why the finite-agent optimization is unnecessary.

5. Stronger interpretation: hypothetical absent true types

If DSIC is instead required for every \(v\in V\) at every fixed \(\mu\), including \(M(v)=0\), the answer remains in \(\mathrm P\), but feasibility changes: it holds exactly when \(m=2\).

To prove infeasibility for \(m\ge3\), choose \(0<v<h\) in \(V\) and set

\(\displaystyle \mu=s_q\delta_h+(1-s_q)\delta_0.\)

This is an admissible rational-mass society. Its thresholds satisfy \(t_j=h\) for \(j<q\), and \(t_q=0\).

The absent true type \(v\), reporting truthfully, has rank \(u(v)=s_q\) and receives no increment. Set \(s_0=0\) and choose

\(\displaystyle \frac{s_{q-1}}{s_q}<z<1.\)

Reporting \(h\) gives rank \(zs_q\in(s_{q-1},s_q)\). It wins exactly the last increment, whose quality is \(\Delta_q=\alpha_q>0\) and whose price is zero. Its utility gain is \(\alpha_qv>0\). The report-independent rebate cancels, so no choice of \(\lambda\) can restore DSIC.

For \(m=2\), write \(V=\{0,h\}\). Societies containing both types are covered by Section 2. In \(\mu=\delta_0\), the absent type \(h\) truthfully wins every increment at zero price. In \(\mu=\delta_h\), the absent type \(0\) truthfully loses every increment, all of whose prices are \(h\). Truth-telling is optimal in both cases. Thus \(\lambda_*\) is feasible under this stronger interpretation exactly when \(m=2\).

Both interpretations are therefore completely settled in polynomial time.

⟨structured verdict parsed — rendered above⟩

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

The prover resolves the decision problem correctly under the natural interpretation that a tagged agent belongs to the society. Its additional analysis also correctly settles the stronger interpretation allowing absent true types. No major or minor mathematical issues were found.

The prover explicitly restricts its main DSIC claim to true values \(v\in\operatorname{supp}\mu\), while allowing every report \(b\in V\). This is consistent with the task’s description of agents distributed across positive-mass types.

This interpretation is substantive rather than a degenerate restriction: every actual agent is covered, including every fixed priority \(z\in(0,1)\). Section 5 separately checks the alternative quantification over all hypothetical true values in \(V\).

The quality ordering gives \(\Delta_j\ge0\). Every cutoff satisfies \(0<s_j<1\), so all the proposed atoms lie in the allowed domain. The measure
\[ \lambda_*=\sum_{j=1}^{q}s_j\Delta_j\,\delta_{s_j} \]
is finite and independent of the society.

The total-mass bound is valid because \(s_j<1\) and \(\sum_j\Delta_j=\alpha_1\). Integration against the atomic measure yields exactly the defined surplus for every society, with no continuity assumption on the quantile needed.

Since all values are nonnegative, the surplus and rebate are nonnegative. Choosing \(e=1\) therefore satisfies every required rebate inequality and every permitted threshold \(\eta\).

For finite positive-mass support, the descending, right-continuous quantile takes value \(t\) on
\[ [H(t),H(t)+M(t)). \]
Consequently, the claimed inequalities
\[ H(t_j)\le s_j<H(t_j)+M(t_j) \]
are correct. The strict upper inequality remains valid when a cutoff coincides with a support-block boundary: the right-continuous convention selects the following block.

The endpoint convention at rank \(1\) causes no issue because every cutoff is strictly below \(1\).

Each of the three cases is valid:

The utility expression follows directly from the specified allocation and payment formulas. The rebate cancels in comparisons because a unilateral report leaves the society fixed.

Truth-telling maximizes each increment’s contribution separately. Summing these inequalities is legitimate even though a report selects several increments simultaneously. The comparison places no positive-mass restriction on the alternative report, so absent reports are covered.

Equal qualities also cause no problem: increments with \(\Delta_j=0\) contribute zero.

Uniform priority within each type induces uniform rank on that type’s interval. Weighting these intervals by their masses gives uniform population rank, with endpoints having population measure zero.

Thus the population fraction winning increment \(j\) is exactly \(s_j\), and its aggregate payment is \(s_j\Delta_jt_j\). Summing gives the defined surplus. Paying that amount to every agent in a population of total mass one produces aggregate net payment zero.

This argument concerns the truthful population represented by the society, as intended by the task. It does not require hypothetical absent types to contribute population mass.

The admissible interval itself imposes \(e\le1\), so the feasible witness with \(e=1\) is optimal.

For a society concentrated at any positive \(h\in V\), every cutoff quantile equals \(h\). The surplus is strictly positive because the last term has \(s_q>0\) and \(\Delta_q=\alpha_q>0\). The optimal guarantee therefore is not merely a consequence of universally zero surplus.

On promised valid inputs, returning YES is a correct decision algorithm. The stated constant-time decision and linear-time full-input reading bounds are consistent.

Constructing cumulative capacities and atom weights requires the stated linear number of rational arithmetic operations. With ordinary reduced rational representations, their bit lengths remain bounded by a constant multiple of the total input length. The stated conservative bit-operation and output-size bounds are valid.

The supplied-society evaluation bound correctly accounts for sorting its positive-mass support, scanning cutoffs, and accumulating the rebate. The analysis uses the actual support size \(\tau\), without confusing it with the number of possible types.

The cited paper’s Section 4.1 indeed defines rebates using the other agents’ reports, and Theorem 4 states the scaling-based optimality result described by the prover. [Journal version](https://arxiv.org/pdf/1401.3884).

The prover uses this reference only for comparison. Its continuous conclusion does not depend on applying that theorem or transferring its hypotheses to the present model.

For \(m\ge3\), the required values \(0<v<h\) exist. The proposed two-point society has positive rational masses. Its thresholds are correctly identified: earlier cutoffs lie inside the upper block, while the last cutoff selects zero by right continuity.

The absent true type’s truthful rank equals \(s_q\), so it wins no increment. The specified priority interval is nonempty because capacities are positive; this remains true when \(q=1\), using \(s_0=0\). Reporting \(h\) wins exactly the last increment at zero price, giving the claimed strictly positive utility gain. No report-independent rebate can remove this violation.

For \(m=2\), the prover exhausts all support possibilities. The two single-type societies have the stated allocation and payment behavior for the absent true type. Together with Section 2, this establishes feasibility exactly when \(m=2\) under the stronger interpretation.

No additional clarification or repair is needed to verify the mathematical conclusion.

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