← back to the atlas

d4-conf-sigecom-2007-0021 (d4-conf-sigecom-2007-0021)

Answer: \(\kappa^*=1\). The unique optimal rule is \(r^*(\mu)=\alpha p_\alpha(\mu)\) for every rational distribution. Construction and support-based evaluation are polynomial-time; every guarantee \(\kappa\in[0,1]\) is achievable.

The anchor (named result in the paper)

Theorem 2 — class: other

PDF text-layer excerpt — equations and symbol order may be approximateFor any m and n with n ≥m+2, the worst- case optimal mechanism among the family of linear VCG redistribution mechanisms is worst-case optimal among all mechanisms that are deterministic, anonymous, strategy-proof, efficient and satisfy the non-deficit constraint. While we needed individual rationality earlier in the pa- per, this theorem does not mention it, that is, we can not find a mechanism with better worst-case performance even if we sacrifice individual rationality.

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

The continuous mirror question, as graded

Given rational \(\alpha\in(0,1)\), a finite value set \(V\), and a rational distribution \(\mu\) over \(V\), allocate mass \(\alpha\) to the highest values, splitting ties as needed, and charge winners the cutoff value \(p_\alpha(\mu)\) per unit. Among deterministic anonymous strategyproof VCG-rebate rules that return the same per-capita rebate \(r(\mu)\) to all agents and satisfy \(0\le r(\mu)\le\alpha p_\alpha(\mu)\), maximize \(\kappa\) subject to \(r(\mu)\ge\kappa\alpha p_\alpha(\mu)\) for every \(\mu\); what is the optimal rule and how efficiently can it be computed from the support?

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

Fix rational \(\alpha\in(0,1)\) and a finite set \(V\subseteq\mathbb{Q}_{\ge0}\) containing a positive value; write \(m=|V|\). Agents form an atomless society of total mass \(1\), have unit demand, and have quasilinear utility.
A society is given by its support: the list of the \(\tau\) types with positive mass, each with its mass as a binary rational. Here \(\tau\) is the support size, not the number \(m\) of possible types; masses sum to \(1\). Let \(L\) be the total input bit length.
For a reported distribution \(\mu\), define \(p=p_\alpha(\mu)=\max\{v\in\operatorname{supp}(\mu):\mu([v,\infty))>\alpha\}\). Allocate fraction \(x(b,\mu)=1\) for reports \(b>p\), fraction \(0\) for \(b<p\), and fraction \((\alpha-\mu((p,\infty)))/\mu(\{p\})\) for \(b=p\); charge \(p\) per allocated unit.
Ties are split deterministically into equal fractional allocations. A rebate rule is a deterministic function \(r\) on all rational distributions over \(V\), returning the same per-capita rebate to every agent, with \(0\le r(\mu)\le\alpha p_\alpha(\mu)\).
Strategyproofness concerns unilateral reports by individual agents of zero mass: \(\mu\) stays fixed, and truthful reporting must maximize \((v-p)x(b,\mu)+r(\mu)\) over \(b\in V\) for every true value \(v\in V\). No coalition incentive condition is imposed.
For fixed \((\alpha,V)\), the rule must guarantee \(r(\mu)\ge\kappa\alpha p_\alpha(\mu)\) for every rational distribution \(\mu\) over \(V\), with \(\kappa\in[0,1]\); this inequality also governs profiles with zero revenue.

What is the optimal worst-case redistribution fraction \(\kappa\), and which admissible rules attain it? Can an optimal rule be constructed and evaluated from the support in polynomial time in \(m,\tau,L\), or is deciding whether a given rational guarantee \(\kappa\) is achievable NP-hard?

For \(n\ge q+2\) finite unit-demand agents competing for \(q\ge1\) units, the optimal linear rebate rule is optimal among all deterministic, anonymous, efficient, strategyproof, non-deficit mechanisms, even without individual rationality; its guarantee is \(1-\binom{n-1}{q}/\sum_{j=q}^{n-1}\binom{n-1}{j}\). [Guo–Conitzer](https://cs.adelaide.edu.au/~mingyu/publication/ec174-guo.pdf)
Continuum economies have general VCG characterization and existence results. [Makowski–Ostroy](https://www.sciencedirect.com/science/article/pii/0304406892900194) No result settling this specific uniform-rebate optimization was located.

Modeling choices made when packaging the task

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

Result

Under the stated zero-mass notion of strategyproofness, the optimal guarantee is \( \kappa^*=1 \). The unique admissible rule attaining it is
\( r^*(\mu)=\alpha p_\alpha(\mu) \)
for every rational distribution \( \mu \) over \( V \).

This rule can be constructed and evaluated in polynomial time from the support. Indeed, every prescribed guarantee \( \kappa\in[0,1] \) is achievable. The optimization simplifies because a unilateral report leaves both the price and the rebate unchanged.

1. The price and allocation are well defined

Fix a rational distribution \( \mu \) over \( V \). Its support is nonempty. If \( z \) is its smallest support value, then \( \mu([z,\infty))=1>\alpha \). Thus the set defining \( p=p_\alpha(\mu) \) is nonempty and finite.

Write \( A=\mu((p,\infty)) \) and \( B=\mu(\{p\}) \). Since \( p \) belongs to the support, \( B>0 \), and the definition of \( p \) gives \( A+B>\alpha \).

We also have \( A\le\alpha \). If there is no support value above \( p \), then \( A=0 \). Otherwise, let \( w \) be the smallest support value above \( p \). Then \( \mu([w,\infty))=A \). If \( A>\alpha \), the value \( w>p \) would qualify in the maximization defining \( p \), a contradiction.

Consequently, the fraction allocated at the price,
\( \beta=(\alpha-A)/B \),
satisfies \( 0\le\beta<1 \). This includes the boundary case \( A=\alpha \), where \( \beta=0 \).

The total allocated mass is exactly
\( A+B\beta=A+\alpha-A=\alpha \).
Since every allocated unit is charged \( p \), total revenue is therefore
\( R(\mu)=\alpha p_\alpha(\mu) \).

Because the society has total mass one, a uniform per-capita rebate \( r(\mu) \) redistributes total amount \( r(\mu) \). Thus the prescribed bound \( r(\mu)\le R(\mu) \) is exactly the non-deficit condition.

2. Every rebate satisfying the pointwise bounds is strategyproof

Let \( r \) be any deterministic function satisfying
\( 0\le r(\mu)\le R(\mu) \)
on every rational distribution.

Fix \( \mu \) and a true value \( v\in V \), including a value outside the support. By the stipulated zero-mass deviation convention, every report \( b\in V \) leaves \( \mu \), \( p \), and \( r(\mu) \) unchanged. Utility is
\( u_v(b;\mu)=(v-p)x(b,\mu)+r(\mu) \),
where \( 0\le x(b,\mu)\le1 \).

There are three cases.

\( u_v(v;\mu)-u_v(b;\mu)=(v-p)(1-x(b,\mu))\ge0 \).

\( u_v(v;\mu)-u_v(b;\mu)=(p-v)x(b,\mu)\ge0 \).

Hence truthful reporting maximizes utility in all cases. No restriction linking rebates at different distributions follows from the stated incentive condition.

3. Optimal guarantee and all attaining rules

Define \( r^*(\mu)=R(\mu)=\alpha p_\alpha(\mu) \). This is deterministic, satisfies the pointwise bounds, and is strategyproof by Section 2. It guarantees
\( r^*(\mu)\ge1\cdot\alpha p_\alpha(\mu) \)
at every distribution, including those with zero revenue. Therefore \( \kappa^*=1 \).

For completeness, even if guarantees above one were allowed, they would be impossible. Choose a positive value \( v_+\in V \) and the rational distribution \( \mu=\delta_{v_+} \). Then \( p_\alpha(\mu)=v_+ \) and \( R(\mu)=\alpha v_+>0 \). Combining a guarantee \( r(\mu)\ge\kappa R(\mu) \) with \( r(\mu)\le R(\mu) \) forces \( \kappa\le1 \).

If an admissible rule attains guarantee one, then at every distribution,
\( R(\mu)\le r(\mu)\le R(\mu) \).
Thus \( r(\mu)=R(\mu) \) everywhere. In particular, zero-revenue profiles also force \( r(\mu)=0 \). The optimal rule is therefore unique as a function on the entire specified domain.

More generally, for any fixed \( \kappa\in[0,1] \), the rules attaining that guarantee are exactly the deterministic functions satisfying
\( \kappa R(\mu)\le r(\mu)\le R(\mu) \)
at every rational distribution. Sufficiency follows from Section 2; necessity follows directly from the guarantee and budget bounds.

4. Exact polynomial-time evaluation

Suppose the input support consists of distinct values \( z_1,\ldots,z_\tau \) with positive rational masses \( w_1,\ldots,w_\tau \).

Use the following algorithm:

The algorithm stops because the final accumulated mass is one. At each visited value, the accumulated mass is precisely the mass weakly above that value. Therefore the first strict crossing is the largest support value qualifying in the price definition. Equality with \( \alpha \) does not trigger stopping.

To verify polynomial bit complexity, write the masses as \( w_i=a_i/d_i \) and use the common denominator \( D=\prod_{i=1}^{\tau}d_i \). Its bit length is at most the sum of the denominator bit lengths, hence is bounded by the input length \( L \). Each mass becomes the integer numerator \( a_i(D/d_i) \) over \( D \). Every accumulated numerator is at most \( D \), because the masses sum to one.

If \( \alpha=c/e \), a tail numerator \( N \) exceeds the threshold exactly when \( eN>cD \). These integer comparisons, the rational comparisons used in sorting, and the final rational multiplication all have polynomial bit complexity. Sorting uses \( O(\tau\log\tau) \) comparisons, followed by a linear scan. Since \( \alpha \) and \( V \) are fixed, their encoding costs are constants; including their encodings also gives a polynomial bound.

Thus the rule is evaluable in polynomial time in \( m,\tau,L \). Its construction is the universal formula above, with no optimization search. Within the specified guarantee domain \( \kappa\in[0,1] \), the achievability decision always returns yes.

5. Relation to the finite-agent result

The finite-agent comparison does not obstruct this conclusion. Guo–Conitzer explicitly explains that equal redistribution of revenue can alter incentives in finite auctions because an individual bid can change the revenue being redistributed. [Guo–Conitzer, Section 1](https://cs.adelaide.edu.au/~mingyu/publication/ec174-guo.pdf)

Here, the task expressly fixes the reported distribution under every unilateral deviation. Section 2 proves that this removes the corresponding incentive restriction for every allowed rebate function. The conclusion therefore follows directly from the specified model.

⟨structured verdict parsed — rendered above⟩

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

The prover’s output fully resolves the task under its explicitly stated zero-mass notion of strategyproofness. The optimal guarantee, uniqueness claim, and polynomial-time evaluation argument are correct. No major or minor mathematical issues were found.

The smallest support value has weak upper-tail mass \(1>\alpha\), so the finite set defining \(p_\alpha(\mu)\) is nonempty and has a maximum.

With \(A=\mu((p,\infty))\) and \(B=\mu(\{p\})\), membership of \(p\) in the support gives \(B>0\), and its qualification gives \(A+B>\alpha\). The argument proving \(A\le\alpha\) is valid: if a support value exists above \(p\), the smallest such value has weak upper-tail mass exactly \(A\); \(A>\alpha\) would contradict maximality of \(p\).

Consequently, \(0\le(\alpha-A)/B<1\). The strict upper bound follows from \(A+B>\alpha\). The boundary case \(A=\alpha\) is explicitly and correctly handled.

The allocated mass is \(A+B(\alpha-A)/B=\alpha\). Charging \(p\) per allocated unit therefore produces revenue \(R(\mu)=\alpha p_\alpha(\mu)\).

Since the population has total mass one, a uniform per-capita rebate \(r(\mu)\) has total cost \(r(\mu)\). Thus the specified upper bound is precisely the non-deficit constraint. These statements also hold when \(p=0\).

The task expressly stipulates that unilateral reports leave \(\mu\) fixed. Hence \(p\) and \(r(\mu)\) remain fixed as well.

Each utility comparison has the correct sign:

The argument includes true values outside the support and all reports in \(V\). It establishes weak maximization, exactly as required. No condition connecting rebates across distributions follows from this incentive requirement.

The rule \(r^*(\mu)=R(\mu)\) satisfies all pointwise bounds and is strategyproof by the preceding argument. Its guarantee is one at every distribution.

The additional upper-bound argument is valid: the rational distribution concentrated at a positive \(v_+\in V\) has positive revenue \(\alpha v_+\), so the budget bound excludes guarantees above one.

Any rule guaranteeing one must satisfy \(R(\mu)\le r(\mu)\le R(\mu)\) at every rational distribution. This proves uniqueness throughout the specified domain, including zero-revenue profiles.

The characterization for a prescribed \(\kappa\in[0,1]\) is also correct: the displayed inequalities are necessary and sufficient to provide at least that guarantee. They need not mean that the rule’s largest possible guarantee equals that particular \(\kappa\); the text consistently uses “guarantee” as the required lower bound.

Sorting downward and stopping at the first accumulated mass strictly exceeding \(\alpha\) returns precisely the largest qualifying support value. Equality does not trigger stopping, correctly matching the task’s strict inequality.

The common denominator \(D=\prod_i d_i\) has bit length bounded by the sum of denominator bit lengths. All accumulated integer numerators lie between zero and \(D\). Comparing \(eN\) with \(cD\) correctly implements the strict threshold for \(\alpha=c/e\).

The common-denominator construction, rational sorting, scan, and final multiplication involve polynomially many operations on integers of polynomial bit length. The argument covers both fixed encodings of \(\alpha,V\) and their inclusion in the input. The universal formula supplies the requested construction without optimization search.

Within the promised domain \(\kappa\in[0,1]\), every achievability instance has answer yes. Thus the requested complexity question is resolved by an explicit polynomial-time algorithm.

Section 1 of the cited paper explains that equal redistribution can destroy finite-agent strategyproofness because a bidder can influence the redistributed revenue. The prover’s attribution is supported by the source. [Guo–Conitzer, Section 1](https://cs.adelaide.edu.au/~mingyu/publication/ec174-guo.pdf)

The prover does not apply a finite-agent characterization theorem to this continuum model. Its conclusion rests on the task’s explicit deviation convention and the direct utility comparisons above. No additional theorem or missing lemma is needed.

No additional clarification is required to make the argument verifiable.

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