← back to the atlas

Explicit Payments for Obviously Strategyproof Mechanisms (aamas23-00249)

Answer: —

The anchor (named result in the paper)

Theorem 5.1 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateAlgorithm 1 needs subsidies of at most 𝑛· 𝑣2 −(𝑛− 1) · 𝑣ℓ−𝑣ℓ−1.

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

The continuous mirror question, as graded

Given a finite item set \(U\), complete bidder-type support \(\Theta\) with \(\theta=(R_\theta,D_\theta,v_\theta)\), rational mass vector \(\mu\in\Delta_\Theta\), rational capacity vector \(q\), and canonical tie-breaking, form admissible \(N\)-replica markets with \(N\mu_\theta\) copies of each type and \(Nq_j\) copies of item \(j\). Using Algorithm 1 and the paper's OSP payment constraints, compute or decide whether there exists a per-type, per-history transfer table \(p_{\theta,h}\) whose normalized worst-profile external subsidy \(S_\infty(\mu)=\limsup_{N\to\infty}N^{-1}\max_b\sum_{i=1}^N s_i^N(b)\) is at most \(B\), where \(s_i^N(b)\) is the subsidy required to make truthful utility nonnegative.

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

A society is given by its support: the list of the \(\tau\) types with positive mass, each mass a binary rational; \(\tau\) is the support size, not the number of possible types. Let \(U\) contain \(m\geq1\) items. Each type \(\theta=(R_\theta,D_\theta,v_\theta)\) has a publicly known nonempty bundle \(R_\theta\subseteq U\), a publicly known finite nonempty domain \(D_\theta\subseteq\mathbb Q_{\geq0}\), and a private value \(v_\theta\in D_\theta\). Masses sum to \(1\); capacities \(q_j\) and threshold \(B\) are nonnegative binary rationals.
For every positive integer \(N\) making all \(N\mu_\theta\) and \(Nq_j\) integral, create \(N\mu_\theta\) bidders of each type and \(Nq_j\) units of item \(j\). A winning bidder consumes one unit of every item in her bundle and receives value equal to her private value; a loser receives value \(0\).
Use this querying mechanism: initially each bidder's remaining domain is her full domain; repeatedly select an active bidder maximizing \(\max D_i/\sqrt{|R_i|}\), breaking ties lexicographically by support index and copy index. Remove her as a loser if her bundle exceeds remaining capacities; otherwise ask whether her value equals \(\max D_i\). A yes allocates her bundle and removes her; a no deletes that domain maximum. A singleton domain is answered affirmatively without a query.
A transfer family consists of real tables \(p^N_{\theta,h}\) for all admissible \(N\), where \(h\) is the terminal public transcript with the recipient identified. Transfers may depend on public bundles, domains, and history, but not on an unrevealed private value. Write \(p_i^N(b)\) for the resulting transfer and \(x_i^N(b)\in\{0,1\}\) for winning; utility at true value \(t\) is \(t x_i^N(b)+p_i^N(b)\).
Require baseline budget balance \(\sum_i p_i^N(b)\leq0\) at every profile and OSP: whenever compatible profiles \((t,b_{-i})\) and \((r,c_{-i})\) first take different answers at a query to bidder \(i\), require \(t x_i^N(t,b_{-i})+p_i^N(t,b_{-i})\geq t x_i^N(r,c_{-i})+p_i^N(r,c_{-i})\). Profiles range over the full product of bidders' domains, without a histogram restriction.
Define the truthful-utility deficit \(s_i^N(b)=\max\{0,-b_i x_i^N(b)-p_i^N(b)\}\) and \(S_\infty(\mu,q;p)=\limsup_{N\to\infty,\ N\text{ admissible}}N^{-1}\max_{b\in\prod_iD_i}\sum_i s_i^N(b)\). This counts gross external top-ups; the top-ups are an accounting measure, with OSP imposed on the baseline transfers.
Is deciding whether such a transfer family exists with \(S_\infty(\mu,q;p)\leq B\) solvable in polynomial time, or is it NP-hard? State running times in \(m\), \(\tau\), total input bit length \(L\), and \(d=\max_\theta|D_\theta|\).
For discrete markets with one unit per item and a common domain \(\{v_1>\cdots>v_\ell\}\), \(\ell\geq2\), explicit greedy OSP payments have the tight worst-instance subsidy bound \(n v_2-(n-1)v_\ell-v_{\ell-1}\); some instances need no subsidy. This is a quantitative bound, not a complexity classification of payment optimization. [Ferraioli–Ventre (2023)](https://www.ifaamas.org/Proceedings/aamas2023/pdfs/p2125.pdf)
No result settling this exact replica-limit decision problem was located.

Modeling choices made when packaging the task

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

Partial solution: exact optimization for a common bundle and domain

The general polynomial-time versus NP-hard classification remains unresolved here. However, the subclass in which all bidders have the same public bundle and the same domain admits an exact polynomial-time solution, for domains of arbitrary size.

In particular, a strictly positive replica-limit deficit can occur already with $m=\tau=1$ and $d=4$.

1. A payment rigidity lemma

Fix a replica and a reachable query to bidder $i$, whose current domain maximum is $a$. An affirmative answer immediately allocates her bundle.

Lemma. Suppose some compatible negative continuation also allocates to bidder $i$. Then her transfer is identical across every affirmative continuation and every winning negative continuation at this query.

Proof. Let $y$ be any affirmative continuation, and let $w$ be a winning negative continuation with bidder $i$ reporting some $t<a$. The profiles producing these continuations share the history preceding this query.

OSP, evaluated first at true value $a$, gives
$$ a+p_i(y)\geq a+p_i(w). $$
OSP, evaluated at true value $t$, gives
$$ t+p_i(w)\geq t+p_i(y). $$
Consequently,
$$ p_i(y)=p_i(w). $$
Because either continuation was arbitrary, the claimed equality holds throughout both collections. $\square$

If their common transfer is $P$, a losing negative continuation compatible with true value $t<a$ must additionally satisfy
$$ t+P\leq p_i(\text{losing continuation})\leq a+P. $$
The lower inequality is OSP at true value $t$; the upper inequality is OSP at true value $a$.

These conclusions allow transfers to depend on the entire terminal transcript. No restriction to outcome-dependent transfers has been assumed.

2. Exact finite optimization for a common bundle and domain

Assume every bidder has the same nonempty bundle $R$ and the same domain $D$. Consider a finite replica with $n$ bidders, and let
$$ k=\min\left\{n,\min_{j\in R}Nq_j\right\}. $$
Thus $k$ is the number of complete bundles available, capped by the bidder count.

Let $F(n,k,D)$ denote the infimum, over all baseline-budget-balanced OSP transfers, of the maximum total truthful-utility deficit.

If $k=0$ or $k=n$, allocation is independent of all reports. Zero transfers therefore give
$$ F(n,k,D)=0. $$

For the remaining case, suppose $0<k<n$ and $|D|\geq3$. Define
$$ H=\max D,\qquad A=\text{second-largest element of }D, $$
$$ C=\text{second-smallest element of }D,\qquad \ell=\min D,\qquad \delta=A-C. $$
Here $\delta\geq0$; when $|D|=3$, we have $A=C$.

Theorem. For $0<k<n$ and $|D|\geq3$,
$$ F(n,k,D)=\max\{0,(n-k)\delta-k\ell\}. $$
The infimum is attained.

2.1 Allocation facts

Index the bidders in the prescribed lexicographic order as $1,\ldots,n$.

Because all bundle sizes are equal, the mechanism compares remaining domain maxima directly. Until $k$ bidders have won, every active bidder’s bundle is feasible. Every active bidder eventually answers affirmatively, possibly upon reaching a singleton domain. Hence exactly $k$ bidders win.

Let
$$ E=\{1,\ldots,k\},\qquad O=\{k+1,\ldots,n\}. $$

No bidder in $O$ can win at value $\ell$. To see this, suppose that immediately before the $\ell$ stage, $a$ bidders in $E$ and $s$ bidders in $O$ have already won. The residual capacity is
$$ k-a-s. $$
There are $k-a$ remaining bidders in $E$, and they precede every remaining bidder in $O$ at the common value $\ell$. They therefore exhaust the residual capacity before anyone in $O$ can win at $\ell$.

Consequently, every winning bidder in $O$ has value at least $C$.

2.2 Matching lower bound

Let $a^0$ be the profile assigning value $\ell$ to every bidder.

For each bidder $i$, consider her initial query at $H$ following negative answers to all preceding initial queries. Call this history $Q_i$. It is reachable: those preceding rejections allocate nothing, so the capacity is still $k>0$.

There is a winning negative continuation at $Q_i$: assign bidder $i$ value $C$ and every other bidder value $\ell$. Bidder $i$ rejects $H$ and subsequently wins at $C$.

The rigidity lemma therefore supplies a number $P_i$ such that every affirmative continuation at $Q_i$, and every winning negative continuation there, gives bidder $i$ transfer $P_i$.

At $a^0$, bidders $1,\ldots,k$ win at $\ell$, so
$$ p_i(a^0)=P_i\qquad (i\leq k). $$

For $i>k$, compare $a^0$ with the profile assigning bidder $i$ value $C$ and everyone else value $\ell$. They share the history preceding bidder $i$’s query at $C$. In the latter profile she wins and receives transfer $P_i$; at $a^0$ she loses. OSP at true value $C$ gives
$$ p_i(a^0)\leq C+P_i. $$

Now consider the profile $z$ assigning value $A$ to bidders $1,\ldots,n-1$, and value $H$ to bidder $n$.

Every bidder except the last rejects her initial $H$ query. Bidder $n$ then wins at $H$. At the $A$ stage, bidders $1,\ldots,k-1$ win, exhausting the capacity. The other $n-k$ bidders lose before being queried at $A$.

Every winner at $z$ receives transfer $P_i$ by the rigidity lemma. For each loser $i$, truthful rejection at $Q_i$, evaluated at true value $A$, must dominate an affirmative answer there. Thus
$$ p_i(z)\geq A+P_i. $$

Baseline budget balance at $z$ implies
$$ 0\geq\sum_i p_i(z) \geq\sum_i P_i+(n-k)A. $$
Therefore,
$$ \sum_i P_i\leq-(n-k)A. $$

The sum of truthful utilities at $a^0$ is consequently bounded by
$$ \begin{aligned} \sum_i\bigl(\ell x_i(a^0)+p_i(a^0)\bigr) &\leq k\ell+\sum_iP_i+(n-k)C\\ &\leq k\ell-(n-k)(A-C). \end{aligned} $$

For any real utilities $u_i$, each $\max\{0,-u_i\}$ is at least $-u_i$. Hence
$$ \sum_i s_i(a^0) \geq \max\{0,(n-k)\delta-k\ell\}. $$

This lower bound applies to every allowed transfer table. All profiles used above belong to the full product of domains; no histogram restriction has been imposed.

2.3 Matching transfer construction

For a losing bidder $i$, let $\lambda_i$ be the maximum of her remaining domain when she is removed. This is public transcript information.

First define the following base transfers:

| Bidder group | Winning transfer | Losing transfer |
|---|---:|---:|
| $E$ | $-\ell$ | $\min\{A,\lambda_i\}-\ell$ |
| $O$ | $-A$ | $\min\{A,\max\{C,\lambda_i\}\}-A$ |

Then add the constant rebate
$$ r=\min\left\{\delta,\frac{k\ell}{n-k}\right\} $$
to every bidder in $O$, at every transcript.

The resulting transfers use only public information.

OSP verification. It suffices to verify the base transfers, because a fixed rebate to a bidder cancels from each of her OSP comparisons.

For either group, write the winning transfer as $-c$ and the losing transfer as $f(\lambda)-c$, where
$$ (c,f)= \left(\ell,\lambda\mapsto\min\{A,\lambda\}\right) $$
for $E$, and
$$ (c,f)= \left(A,\lambda\mapsto\min\{A,\max\{C,\lambda\}\}\right) $$
for $O$.

Consider an actual query at current maximum $a$.

A losing negative continuation has remaining maximum $\lambda<a$. If it is truthful at value $t<a$, then also $\lambda\geq t$. Moreover, $t\leq A$, since $t<H$.

For group $E$, these observations imply
$$ f(\lambda)\leq a, \qquad f(\lambda)\geq t $$
in the respective continuations.

For group $O$, every actual query has $a\geq C$: there is no domain element between $C$ and $\ell$, and $\ell$ is a singleton remaining domain. Since $C\leq a$, $\lambda<a$, and $t\leq\min\{A,\lambda\}$, the same two inequalities hold.

At true value $a$, answering affirmatively gives utility $a-c$. A negative winning continuation gives the same evaluated utility; a negative losing continuation gives at most $a-c$.

At true value $t<a$, a truthful negative winning continuation gives utility $t-c$, while a truthful negative losing continuation gives at least $t-c$. An affirmative deviation gives exactly $t-c$.

Thus every required OSP comparison holds, including comparisons with different compatible continuations by other bidders.

Budget balance. Let $s$ be the number of winners in $O$. Because there are exactly $k$ winners and $|E|=k$, exactly $s$ bidders in $E$ lose.

Each losing bidder in $E$ receives at most $A-\ell$, while each losing bidder in $O$ has a nonpositive base transfer. Therefore the sum of base transfers is at most
$$ s(A-\ell)-(k-s)\ell-sA=-k\ell. $$
The total rebate is $(n-k)r\leq k\ell$. Baseline budget balance follows.

Deficit bound. Every bidder in $E$ has nonnegative truthful utility: a winner obtains at least $\ell-\ell$, and a loser receives a nonnegative transfer.

Before the rebate, every bidder in $O$ has truthful utility at least $-\delta$. This follows from the minimum winning value $C$ and from the lower bound $C-A$ on her losing transfer.

After the rebate, each such bidder’s deficit is at most $\delta-r$. Hence, at every profile,
$$ \sum_i s_i \leq(n-k)(\delta-r) =\max\{0,(n-k)\delta-k\ell\}. $$

This matches the lower bound and proves the theorem. $\square$

3. Exact replica-limit decision for this subclass

Return to the society input, still assuming a common public bundle $R$ and common domain $D$. Define
$$ \rho=\min\left\{1,\min_{j\in R}q_j\right\}. $$
Every admissible replica contains exactly $N$ bidders and has
$$ k=N\rho. $$

If $\rho=0$, everyone loses, so zero transfers suffice. If $\rho=1$, everyone wins, and zero transfers again suffice.

For $0<\rho<1$ and $|D|\geq3$, the finite theorem gives, at every admissible $N$,
$$ \frac{F(N,N\rho,D)}{N} = \max\{0,(1-\rho)(A-C)-\rho\ell\}. $$

The lower bound holds separately for every transfer table. The matching construction supplies a table for every admissible $N$. Thus the minimum possible replica-limit deficit is attained and equals
$$ S_*= \begin{cases} 0, & \rho=0\text{ or }|D|\leq2,\\[2mm] \max\{0,(1-\rho)(A-C)-\rho\ell\}, & \rho>0\text{ and }|D|\geq3. \end{cases} $$
The second expression also gives zero when $\rho=1$.

For this subclass, the answer to the decision question is therefore YES exactly when
$$ S_*\leq B. $$

Recognizing the common bundle and domain, finding the required extrema, and evaluating this rational expression takes, conservatively,
$$ O\bigl((m\tau+\tau d)L^3\bigr) $$
bit operations. No replica enumeration is required.

In particular, every instance with $\tau=1$ is covered, for arbitrary $m$ and $d$.

A positive deficit with one item and one support type

Take
$$ U=\{1\},\qquad R=\{1\},\qquad D=\{3,2,1,0\}, $$
with one support type of mass $1$, recorded value $0$, and capacity
$$ q_1=\frac12. $$
Then
$$ \rho=\frac12,\qquad A=2,\qquad C=1,\qquad\ell=0, $$
so
$$ S_*=\frac12. $$

Every admissible replica has $N$ even and optimal worst-profile gross deficit exactly $N/2$. Consequently, this instance is YES precisely when
$$ B\geq\frac12. $$

4. A general polynomial-time sufficient condition

For completeness, the following bound applies without any common-bundle or common-domain assumption.

For each support type $\theta$, define
$$ \ell_\theta=\min D_\theta, $$
and let $c_\theta$ be its second-largest domain value, setting $c_\theta=\ell_\theta$ for a singleton domain. Put
$$ G=\sum_\theta\mu_\theta(c_\theta-\ell_\theta). $$

Proposition. Every input admits a baseline-budget-balanced OSP transfer family with
$$ S_\infty\leq G. $$

Proof. For a bidder of support type $\theta$, write $c=c_\theta$. Give a winner transfer $-c$. Give a loser transfer zero if she never answered negatively. Otherwise, if $\lambda$ was her last declined maximum, give her transfer
$$ -\max\{0,c-\lambda\}. $$
These transfers are public-transcript-dependent and nonpositive, so budget balance holds.

At a query with maximum $a$, an affirmative answer gives evaluated utility $t-c$ at true value $t$.

If $t=a$, a negative winning continuation gives the same utility. In a negative losing continuation, the last declined maximum satisfies $\lambda\leq a$. If $a\geq c$, losing utility is at most $0\leq a-c$. If $a<c$, losing utility is $\lambda-c\leq a-c$.

If $t<a$, then $t\leq c$. A truthful negative winning continuation gives utility $t-c$. A truthful negative losing continuation has $\lambda>t$. Its utility is zero when $\lambda\geq c$, and otherwise is $\lambda-c>t-c$. Thus truthful rejection dominates an affirmative deviation.

This proves OSP at every query. Singleton domains create no query comparisons.

A winner’s deficit is at most $c_\theta-\ell_\theta$. A loser’s deficit has the same bound, because every declined maximum belongs to her original domain. Therefore, at every profile,
$$ \sum_i s_i^N \leq N\sum_\theta\mu_\theta(c_\theta-\ell_\theta) =NG. $$
Taking the normalized limsup proves the claim. $\square$

Computing $G$ and comparing it with $B$ takes conservatively
$$ O\bigl((m\tau+\tau d)L^3\bigr) $$
bit operations. Thus $B\geq G$ is a polynomial-time sufficient condition for YES.

When $d\leq2$, every $c_\theta=\ell_\theta$, so $G=0$. All such instances are YES; under this promise, the decision takes $O(L)$ time to read the input.

5. What remains unresolved

The exact formula above resolves arbitrary domain sizes when the public bundle and domain are common. It also shows that positive replica-limit deficits do not require multiple items.

It does not classify the general problem with heterogeneous public bundles or domains. Neither a polynomial-time algorithm for that problem nor a valid NP-hardness reduction is established here.

⟨structured verdict parsed — rendered above⟩

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

Verification report

Overall assessment: partial, with sound substantive results. The output establishes the claimed exact optimization for a common public bundle and domain, and the general sufficient condition for a YES answer. It does not settle the polynomial-time versus NP-hard classification requested in USER_TASK, and explicitly acknowledges this limitation.

There is one minor overstatement in the allocation discussion. It does not invalidate the finite theorem.

1. Payment rigidity lemma

The lemma is valid.

At the specified query, every affirmative continuation allocates to bidder $i$. The chosen negative continuation also allocates to her. Because the two profiles share the preceding history and differ at this query, the stated OSP comparisons apply.

At true value $a$, the allocations agree, so OSP yields
$$ p_i(y)\geq p_i(w). $$
At true value $t<a$, the reverse comparison yields
$$ p_i(w)\geq p_i(y). $$
Thus the transfers agree. The arbitrariness of the affirmative and winning negative continuations establishes the claimed equality across both collections.

For a losing negative continuation compatible with true value $t$, the two OSP comparisons correctly give
$$ t+P\leq p_i(\text{losing continuation})\leq a+P. $$
No restriction to outcome-dependent transfers is introduced.

2. Finite common-bundle optimization

2.1 Boundary cases and allocation facts

The definition
$$ k=\min\left\{n,\min_{j\in R}Nq_j\right\} $$
correctly counts the available complete bundles, capped by the number of bidders. All quantities inside this minimum are integers for an admissible replica.

When $k=0$, everyone loses; when $k=n$, everyone wins regardless of reports. Zero transfers are budget balanced, satisfy OSP, and give zero deficit in both cases.

For $0<k<n$, all active bidders have feasible bundles until the $k$th allocation. The mechanism awards exactly $k$ bundles.

Minor issue — an overstatement in Section 2.1. The sentence “Every active bidder eventually answers affirmatively, possibly upon reaching a singleton domain” is false without a qualification. For example, with $n=2$, $k=1$, and both bidders having value $H$, bidder $1$ wins immediately and bidder $2$ is removed as a loser without answering affirmatively.

The minimum clarification needed is to qualify this sentence by the availability of residual capacity. The subsequent conclusion that exactly $k$ bidders win remains valid.

The argument excluding a minimum-value winner in $O$ is correct. After $a$ winners from $E$ and $s$ winners from $O$, residual capacity is
$$ k-a-s, $$
whereas $k-a$ bidders from $E$ remain. At the minimum-value stage, these remaining bidders from $E$ precede all remaining bidders from $O$ and exhaust the residual capacity. Therefore every winner in $O$ has value at least $C$.

2.2 Lower bound

The histories $Q_i$ are reachable. Negative answers at $H$ allocate nothing, and bidders whose maxima have decreased cannot precede bidders still having maximum $H$. Thus all preceding initial queries can be rejected while capacity remains $k>0$.

The proposed winning negative continuation at $Q_i$ is valid: with bidder $i$ at $C$ and everyone else at $\ell$, she wins before the minimum-value stage. Since $|D|\geq3$, one has $C<H$, so this continuation takes a negative answer at $Q_i$. The rigidity lemma therefore provides each $P_i$ as claimed.

At the all-minimum profile $a^0$:

$$ p_i(a^0)\leq C+P_i. $$

The profile $z$ also has the stated behavior. Bidder $n$ wins at $H$, followed by bidders $1,\ldots,k-1$ at $A$. The remaining $n-k$ bidders lose before receiving a query at $A$. This description also covers $k=1$, when the latter winner list is empty.

Every winner at $z$ receives $P_i$. For every loser, truthful rejection at $Q_i$, evaluated at true value $A$, correctly gives
$$ p_i(z)\geq A+P_i. $$
Budget balance consequently implies
$$ \sum_iP_i\leq-(n-k)A. $$

Combining this with the utility bounds at $a^0$ gives
$$ \sum_i\bigl(\ell x_i(a^0)+p_i(a^0)\bigr) \leq k\ell-(n-k)(A-C). $$
The final conversion from total utility to gross deficit is valid: for arbitrary real utilities,
$$ \sum_i\max\{0,-u_i\} \geq\max\left\{0,-\sum_i u_i\right\}. $$

Thus the claimed lower bound holds for every allowed transfer table, including tables depending on the complete terminal transcript.

2.3 Transfer construction

The construction uses public information only. The remaining maximum $\lambda_i$ at removal is recoverable from the transcript, and the rebate depends only on public parameters.

OSP. The verification correctly covers both directions of every required comparison.

After a negative answer at maximum $a$, a losing continuation has remaining maximum $\lambda<a$. In a truthful such continuation at value $t<a$, the true value remains in the domain, so $\lambda\geq t$. Also, $t\leq A$.

For group $E$, these facts give the required bounds on $f(\lambda)$. For group $O$, every actual query has $a\geq C$: the only smaller domain value is $\ell$, which is processed as a singleton without a query. The clamping at $C$ therefore preserves both required inequalities.

Winning transfers are constant within each group. The fixed rebate cancels from every comparison for its recipient. Consequently, the verification applies even when the compatible continuations of other bidders differ.

Budget balance. If $s$ bidders in $O$ win, exactly $s$ bidders in $E$ lose. The upper bound on total base transfers simplifies correctly:
$$ s(A-\ell)-(k-s)\ell-sA=-k\ell. $$
The total rebate is at most $k\ell$, so baseline budget balance holds at every profile.

Deficit. Every bidder in $E$ has nonnegative truthful utility. Every bidder in $O$ has base utility at least $C-A=-\delta$, whether winning or losing. Since
$$ 0\leq r\leq\delta, $$
the rebate bounds each such deficit by $\delta-r$. The displayed total bound and its simplification are correct.

The construction attains the lower bound. Hence the finite theorem, including attainment of the infimum, is established.

3. Replica-limit conclusion

The passage to replicas is valid.

Because masses sum to $1$, every admissible replica contains exactly $N$ bidders. Moreover,
$$ N\rho=\min\left\{N,\min_{j\in R}Nq_j\right\} $$
is an integer for every admissible $N$.

For $0<\rho<1$ and $|D|\geq3$, the finite lower bound applies separately to every table in any transfer family, while the construction supplies a matching table for every admissible replica. Thus the normalized optimum is the stated constant, and the limsup creates no additional optimization gap.

The cases $\rho=0$ and $\rho=1$ are correctly handled. The assertion for $|D|\leq2$, which is not proved in Section 2, is supported by the later general proposition: it gives $G=0$ for those domains.

The example with
$$ D=\{3,2,1,0\},\qquad q_1=\frac12 $$
is computed correctly. It has
$$ S_*=\frac12, $$
and every admissible replica has even $N$ and optimum total deficit $N/2$. The recorded support value does not constrain the profiles being optimized, consistently with USER_TASK.

4. General sufficient condition

The proposition is valid.

All proposed transfers are public-transcript-dependent and nonpositive, which immediately establishes baseline budget balance.

At any query, a negative losing continuation has a last declined maximum $\lambda\leq a$, because the current rejection itself is a decline and subsequent maxima decrease. The two cases $a\geq c$ and $a<c$ give exactly the asserted upper bound on losing utility when evaluating a deviation from true value $a$.

For true value $t<a$, one has $t\leq c$. In a truthful negative losing continuation, every declined maximum exceeds $t$, so the last one satisfies $\lambda>t$. The displayed comparison with affirmative utility $t-c$ is therefore valid in both payment cases. Winning negative continuations have the same evaluated utility as affirmative continuations.

For singleton domains, there are no query comparisons. A winner receives utility zero, and a loser has transfer zero.

The deficit bound is correct for winners and losers. Summing over the integral copy counts gives the bound $NG$, and taking the normalized limsup establishes
$$ S_\infty\leq G. $$
For domains of size at most $2$, the identity $c_\theta=\ell_\theta$ yields $G=0$. Thus all inputs under that promise are YES, since $B$ is nonnegative.

5. Running times and unresolved assignment

The stated conservative bounds
$$ O\bigl((m\tau+\tau d)L^3\bigr) $$
are sufficient for the input checks, rational extrema, arithmetic, and comparisons described. They do not require enumerating replicas or transfer tables. The linear-time conclusion under the promise $d\leq2$ is also consistent with simply reading the input and returning YES.

Major issue relative to the assignment — the general classification is missing. The output provides neither a polynomial-time decision procedure for arbitrary heterogeneous public inputs nor an NP-hardness reduction. A polynomial-time sufficient condition alone does not decide instances that fail that condition.

This is an acknowledged limitation, rather than an incorrect claim of completeness. To complete the assignment, the prover must supply one of those general complexity results with its required correctness argument and running-time analysis.

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