Answer: \(R(\mu,q)=q\lambda\), with the supremum attained; deciding \(R(\mu,q)\ge b\) is in \(\mathrm P\).
Theorem 1 — class: other
PDF text-layer excerpt — equations and symbol order may be approximateA redistribution mechanism r is undominated if and only if for all i and all θ1, . . . , θn ri(θ−i) ≥0 (3) ri(θ−i) = min θ′ i∈Θi {V CG(θ′ i, θ−i) − X j̸=i rj(θ′ −j)} (4) Here, θ′ −j are the reported types of the agents other than j when θi is replaced by θ′ i. It should be noted that the only difference between Equation 2 and Equation 4 is that “≤” is replaced by “=”. PROOF. We prove the “if” direction first. Any redistribution mechanism r that satisfies Equation 3 and Equation 4 is feasible by Claim 1.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite rational value set \(T\subseteq\mathbb{Q}_{\ge 0}\), a rational distribution \(\mu\) over \(T\), and \(q\in(0,1)\), assume some \(\lambda\in\operatorname{supp}(\mu)\) satisfies \(\mu(>\lambda)<q<\mu(\ge\lambda)\). For finite populations with empirical value distributions converging to \(\mu\) and numbers of indivisible slots \(m_N\) satisfying \(m_N/N\to q\), what is the greatest common limiting per-buyer rebate achievable by anonymous feasible VCG redistribution rules that preserve the VCG allocation and make each buyer’s rebate depend only on other buyers’ reports?
A society is given by its support: the list \(T\subseteq\mathbb Q_{\ge0}\) of its \(\tau\) positive-mass types, with each mass encoded as a binary rational; \(\tau\) is the support size, not the number of possible reports. Masses sum to \(1\). Input also includes rational \(q\in(0,1)\), with \(\mu((\lambda,\infty))<q<\mu([\lambda,\infty))\) for some \(\lambda\in T\).
For each \(N\), there are \(N\) unit-demand buyers and \(1\le m<N\) identical indivisible slots. Values and reports belong to \([0,\infty)\); observed profiles belong to \(T^N\). Use the VCG allocation and payments, breaking allocation ties uniformly among tied buyers.
An anonymous redistribution rule is a permutation-invariant function \(r_{N,m}:[0,\infty)^{N-1}\to\mathbb R_{\ge0}\); buyer \(i\) receives \(r_{N,m}(v_{-i})\) in addition to the VCG outcome. Feasibility requires \(\sum_i r_{N,m}(v_{-i})\le\operatorname{VCG}_{N,m}(v)\) for every report profile \(v\in[0,\infty)^N\), where \(\operatorname{VCG}_{N,m}\) denotes total VCG revenue.
Call \(a\ge0\) achievable if there exists one feasible family \((r_{N,m})\) such that, for every sequence \(v^{(N)}\in T^N\) whose empirical masses converge to \(\mu\), and every sequence \(m_N/N\to q\), \(\max_{1\le i\le N}|r_{N,m_N}(v^{(N)}_{-i})-a|\to0\). Let \(R(\mu,q)\) be the supremum of achievable \(a\).
What is \(R(\mu,q)\), and is deciding \(R(\mu,q)\ge b\), for an input rational \(b\ge0\), in P or NP-hard?
State limiting-problem running times in \(\tau\) and total input bit length \(L\); any finite-population running times must additionally specify dependence on \(N\) and \(m\).
Known finite-population result: feasible redistribution rules are undominated under pointwise comparison of every buyer’s rebate exactly when each rebate saturates the residual-revenue bound obtained by varying that buyer’s report; the original statement uses a minimum. [Guo–Conitzer](https://users.cs.duke.edu/~conitzer/undominatedAAMAS08.pdf).
The later characterization uses an infimum, allowing unrestricted report domains. [Guo–Markakis–Apt–Conitzer](https://www.cs.cmu.edu/~conitzer/undominatedJAIR13.pdf). No result settling the exact limiting problem above was identified in the search.
Under the stated strict cutoff hypothesis,
\[
R(\mu,q)=q\lambda.
\]
The supremum is attained by a single feasible family that works for every society satisfying this hypothesis. Deciding \(R(\mu,q)\ge b\) is in \(\mathrm P\).
For a report profile \(v\in[0,\infty)^N\), write its reports in nonincreasing order as \(v_{(1)},\ldots,v_{(N)}\).
The total VCG revenue is
\[
\operatorname{VCG}_{N,m}(v)=m\,v_{(m+1)}.
\]
Indeed, let \(W=\sum_{j=1}^{m}v_{(j)}\) be the optimal welfare. If buyer \(i\) is allocated a slot, the optimal welfare without that buyer is \(W-v_i+v_{(m+1)}\). The welfare of the other buyers in the chosen allocation is \(W-v_i\), so the buyer’s externality payment is \(v_{(m+1)}\). An unallocated buyer pays zero.
This calculation holds for every realized choice among tied buyers. Consequently, uniform tie breaking gives the same total revenue, also when payments are interpreted in expectation.
For an opponents’ profile \(w\in[0,\infty)^{N-1}\), let \(s_{m+1}(w)\) denote the \((m+1)\)-st largest entry of the length-\(N\) profile obtained by adjoining a zero to \(w\). Define
\[
r_{N,m}(w)=\frac{m}{N}s_{m+1}(w).
\]
For \(m\le N-2\), this is \(m/N\) times the opponents’ \((m+1)\)-st largest report. For \(m=N-1\), it is zero. This is the Bailey–Cavallo rule, whose multi-unit formula appears in [Guo–Markakis–Apt–Conitzer, Section 5.1](https://www.cs.cmu.edu/~conitzer/undominatedJAIR13.pdf#page=21). We verify feasibility directly.
The rule is permutation invariant and nonnegative. Fix any full report profile \(v\). Replacing \(v_i\) by zero cannot increase any order statistic: for every threshold, the number of entries exceeding that threshold cannot increase. Hence
\[
s_{m+1}(v_{-i})\le v_{(m+1)}.
\]
Summing over buyers gives
\[
\sum_{i=1}^{N}r_{N,m}(v_{-i})
\le \sum_{i=1}^{N}\frac{m}{N}v_{(m+1)}
=m\,v_{(m+1)}
=\operatorname{VCG}_{N,m}(v).
\]
Thus this family is feasible for every report profile in \([0,\infty)^N\), including reports outside \(T\). It does not depend on \(\mu\) or \(q\).
Set
\[
h=\mu((\lambda,\infty)),
\qquad
g=\mu([\lambda,\infty)).
\]
The hypothesis is \(h<q<g\).
Consider arbitrary sequences allowed by the definition of achievability. Let \(H_N\) count the reports strictly above \(\lambda\), and let \(G_N\) count the reports at least \(\lambda\). Because \(T\) is finite and its empirical masses converge,
\[
\frac{H_N}{N}\to h,
\qquad
\frac{G_N}{N}\to g.
\]
Together with \(m_N/N\to q\), this implies
\[
\frac{m_N-H_N}{N}\to q-h>0,
\qquad
\frac{G_N-m_N}{N}\to g-q>0.
\]
Therefore, for all sufficiently large \(N\),
\[
H_N\le m_N,
\qquad
G_N\ge m_N+2.
\]
These inequalities show that both the \((m_N+1)\)-st and \((m_N+2)\)-nd largest reports equal \(\lambda\).
More directly, after deleting any buyer, at most \(H_N\le m_N\) remaining reports are strictly above \(\lambda\), and at least \(G_N-1\ge m_N+1\) remaining reports are at least \(\lambda\). Thus the opponents’ \((m_N+1)\)-st largest report is exactly \(\lambda\). Also, \(G_N\le N\) implies \(m_N\le N-2\), so the zero-padding case is irrelevant eventually.
The constructed family consequently satisfies, for every buyer simultaneously,
\[
r_{N,m_N}(v^{(N)}_{-i})=\frac{m_N}{N}\lambda
\]
for all sufficiently large \(N\). Hence
\[
\max_i\left|r_{N,m_N}(v^{(N)}_{-i})-q\lambda\right|
=\lambda\left|\frac{m_N}{N}-q\right|
\to0.
\]
The sequences were arbitrary, so \(q\lambda\) is achievable.
Suppose \(a\) is achievable by any feasible family.
There exists a sequence of observed profiles with empirical masses converging to \(\mu\): enumerate the types, assign \(\lfloor N\mu(t)\rfloor\) buyers to each of the first \(\tau-1\) types, and assign the remaining buyers to the last type. The errors in all empirical masses tend to zero. Choose also integers \(m_N\) with \(1\le m_N<N\) and \(m_N/N\to q\).
By Section 3, the VCG cutoff on these profiles eventually equals \(\lambda\). Write
\[
\varepsilon_N
=\max_i\left|r_{N,m_N}(v^{(N)}_{-i})-a\right|.
\]
Achievability gives \(\varepsilon_N\to0\). Feasibility then implies
\[
a-\varepsilon_N
\le \frac1N\sum_{i=1}^{N}r_{N,m_N}(v^{(N)}_{-i})
\le \frac{\operatorname{VCG}_{N,m_N}(v^{(N)})}{N}
=\frac{m_N}{N}\lambda.
\]
Taking limits yields \(a\le q\lambda\).
Together with the achievable construction, this proves \(R(\mu,q)=q\lambda\), with the supremum attained. The case \(\lambda=0\) is included: its exact answer is zero.
Sort the support as \(t_1>\cdots>t_\tau\), and define cumulative masses \(S_0=0\) and
\[
S_j=\sum_{\ell=1}^{j}\mu(t_\ell).
\]
Find the index \(j\) satisfying \(S_{j-1}<q<S_j\). The promised hypothesis ensures that it exists and is unique, and \(\lambda=t_j\). Return \(qt_j\); for the decision problem, compare \(qt_j\) with \(b\) exactly.
This takes \(O(\tau\log(\tau+1))\) rational comparisons and \(O(\tau)\) rational arithmetic operations.
For an explicit bit bound, let \(L\) be the total input bit length, including \(b\) for the decision problem. Use the product of the mass denominators as a common denominator. Its bit length is \(O(L)\), and the cumulative-mass numerators also have \(O(L)\) bits because the masses sum to one. All required rational comparisons and products involve integers of \(O(L)\) bits.
Using schoolbook integer arithmetic therefore gives a conservative bound of
\[
O\!\left(\tau\log(\tau+1)L^2\right)
\]
bit operations. This establishes membership in \(\mathrm P\). The limiting algorithm has no dependence on \(N\) or \(m\).
For completeness, the witnessing rule also has an efficient implementation:
For the second bound, sort the full profile. When \(m\le N-2\), deleting a buyer of rank at most \(m+1\) makes the opponents’ \((m+1)\)-st report equal to \(v_{(m+2)}\); deleting any later-ranked buyer makes it equal to \(v_{(m+1)}\). Arbitrarily assigning ranks within ties preserves this formula. When \(m=N-1\), every rebate is zero.
These bounds hold uniformly over \(1\le m<N\). For rational reports whose numerators and denominators have at most \(B\) bits, all rebates can, conservatively, be evaluated in
\[
O\!\left(N\log(N+1)(B+\log N)^2\right)
\]
bit operations. The factor \(m/N\) contributes at most \(O(\log N)\) bits.
⟨structured verdict parsed — rendered above⟩
The prover resolves the task correctly. The construction is feasible on the entire report domain, attains \(q\lambda\) under the required universal sequence quantifiers, and matches the feasibility upper bound. The polynomial-time claim and stated running times are valid. No major or minor mathematical issues were found.
The rule is anonymous, independent of the recipient’s own report, and nonnegative. Replacing one coordinate by zero cannot increase an order statistic, so the individual inequality and its sum are valid for every real report profile, including profiles outside the observed support. No restriction to rational reports is used in the feasibility proof.
The attribution of the multi-unit formula to Bailey–Cavallo agrees with the cited paper. Its bounded-domain presentation introduces no gap here because the prover establishes unrestricted-domain feasibility directly. [Guo–Markakis–Apt–Conitzer, Section 5.1](https://www.cs.cmu.edu/~conitzer/undominatedJAIR13.pdf#page=21)
\(H_N\le m_N\) and \(G_N\ge m_N+2\).
These bounds locate both relevant full-profile order statistics at \(\lambda\). After any deletion, the remaining counts still place the opponents’ \((m_N+1)\)-st report at \(\lambda\). The same bounds ensure \(m_N\le N-2\), so the rule’s exceptional zero-padding branch is correctly excluded eventually.
The resulting rebate identity holds simultaneously for every buyer. Consequently, the maximum-error calculation proves exactly the required convergence. The sequences were arbitrary, and the family was fixed beforehand; there is no quantifier interchange or sequence-dependent construction.
Achievability bounds every rebate below by \(a-\varepsilon_N\). Averaging and applying feasibility gives the stated upper bound. The eventual cutoff calculation applies independently of the chosen redistribution family. Taking limits therefore yields \(a\le q\lambda\). Together with the witness, this establishes both the supremum’s value and its attainment.
The product of mass denominators has \(O(L)\) bits. Cumulative numerators remain bounded by that common denominator because the masses are nonnegative and sum to one. Cross-products for comparisons and the final rational product also have \(O(L)\) bits. The stated schoolbook bound
\(O(\tau\log(\tau+1)L^2)\)
is conservative and valid. It establishes polynomial-time decision complexity without dependence on \(N\) or \(m\).
Rational comparisons and multiplication by \(m/N\) involve \(O(B+\log N)\)-bit integers, supporting the stated conservative bit bound
\(O(N\log(N+1)(B+\log N)^2)\).
Its uniformity over \(1\le m<N\) explicitly accounts for dependence on \(m\).
No additional lemma, clarification, or repair is needed. The finite-population undominance characterizations are not required by this argument.
⟨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.