← back to the atlas

d4-conf-atal-2014-0376 (d4-conf-atal-2014-0376)

Answer: —

The anchor (named result in the paper)

Theorem 14 — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximateThere are no randomized mechanisms that are truthful in expectation and have approximation ratio less or equal than 1.09 for CAs with known 2-minded bidders. This holds even for simple instances with n = 2 bidders, and m = 2 goods.

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

The continuous mirror question, as graded

Given goods \(U\), rational per-capita supplies \(q_e\), and a finite set of types \(T\) with rational masses \(\mu_t\) and public menus \(D_t\) of at most two whole bundles, determine the best worst-case welfare approximation ratio achievable in polynomial time by a truthful-in-expectation mechanism with the paper’s verification rule. The mechanism specifies a lottery \(\pi_r(S\mid\mu)\) for each reported type \(r\), with aggregate assignment masses \(x_{t,S}=\mu_t\pi_t(S\mid\mu)\); feasibility requires each type’s mass to be assigned and total use of each good to be at most \(q_e\). Truthfulness requires that, for each true type \(t\) and permissible report \(r\), the expected value under \(\pi_t(\cdot\mid\mu)\) is at least that under \(\pi_r(\cdot\mid\mu)\). Compare welfare with the optimum feasible mass allocation, or prove a lower bound on the achievable ratio.

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

Let \(U\) contain \(m\ge2\) goods, with positive binary-rational per-capita supplies \(q_e\). A society is given by its support: the list of \(\tau\) types with positive binary-rational masses \(\mu_t\), summing to \(1\). Here \(\tau\) is the support size, not the number of possible types; \(L\) is the total input bit length.
Each type \(t=(D_t,v_t)\) has an immutable public menu \(D_t\) of one or two distinct nonempty bundles and private nonnegative rational values. Values respect inclusion within the menu; zero values and ties are allowed, and \(v_t(\varnothing)=0\). The declaration domain contains every such valuation on the same public menu, including declarations outside the society's support.
A mechanism uses no payments and supplies a lottery \(\pi_r(\cdot\mid\mu)\) on \(D_r\cup\{\varnothing\}\) for every report \(r\). Individuals are nonatomic: an individual's deviation leaves \(\mu\) fixed. Lottery probabilities must be computable in time polynomial in \(m,\tau,L\) and the queried report's bit length.
For supported types, set \(x_{t,S}=\mu_t\pi_t(S\mid\mu)\). Feasibility means \(\sum_{S\in D_t\cup\{\varnothing\}}x_{t,S}=\mu_t\) and \(\sum_t\sum_{S\in D_t:e\in S}x_{t,S}\le q_e\); individuals receive whole bundles, while aggregate masses may be split.
Verification checks only the awarded nonempty bundle. A report \(r\) by true type \(t\) is permissible exactly when \(D_r=D_t\) and \(v_r(S)\le v_t(S)\) for every nonempty \(S\) with \(\pi_r(S\mid\mu)>0\); any positive probability of detection carries a prohibitive penalty. Truthfulness in expectation requires \(\sum_S\pi_t(S\mid\mu)v_t(S)\ge\sum_S\pi_r(S\mid\mu)v_t(S)\) for every permissible report, every rational true valuation on a public menu occurring in the society, and every society.
Welfare is \(W=\sum_t\sum_{S\in D_t}x_{t,S}v_t(S)\). Let \(\mathrm{OPT}\) be maximum welfare over feasible mass allocations without incentive constraints; an approximation factor \(\alpha\ge1\) guarantees \(W\ge\mathrm{OPT}/\alpha\) on every instance with \(\mathrm{OPT}>0\).

What is the optimal worst-case welfare approximation ratio achievable by polynomial-time truthful-in-expectation mechanisms in this mass model?

For discrete bidders, no truthful-in-expectation mechanism achieves approximation factor at most \(1.09\), even with two bidders, two goods, and public menus of at most two bundles, regardless of computation time. A polynomial-time universally truthful mechanism achieves \(O(\sqrt m)\). [Source](https://research.tees.ac.uk/files/6554847/586887.pdf)
No result settling the precise mass model above was located in the literature search.

Modeling choices made when packaging the task

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

Partial results: a stronger lower bound and a reduction to one common menu

The exact optimal approximation ratio remains unresolved. I prove two new results:

$$ \frac{715}{614}. $$
This strengthens the previous bound $9/8$ and disproves the suggested universal bound $F\ge(8/9)\mathrm{OPT}$ for the dominance LP.

Together with a polynomial-time factor-$2$ mechanism, these results give
$$ \frac{715}{614}\le\alpha_{\mathrm{inf}}\le2. $$

I first prove the necessary characterization and upper bound, so the argument is self-contained.

1. Extending a supported allocation to all declarations

Fix a society. Write $p_t(S)$ for a supported type’s probability of receiving a nonempty bundle $S\in D_t$. The remaining probability awards $\varnothing$.

Suppose this supported table is feasible and satisfies every permissible supported-report comparison: for supported types $t,r$ with the same menu,
$$ v_r(S)\le v_t(S)\quad\text{whenever }p_r(S)>0 $$
implies
$$ \sum_{S\in D_t}v_t(S)p_t(S) \ge \sum_{S\in D_t}v_t(S)p_r(S). $$

Extension lemma. Such a table extends to a truthful-in-expectation mechanism on the entire declaration domain. If the table has polynomial encoding length, its queried lotteries are computable in polynomial time.

Proof. For a declaration $z=(D,v_z)$, make the empty lottery available. Also make a supported lottery $p_s$ available exactly when
$$ D_s=D,\qquad v_s(S)\le v_z(S)\quad\text{whenever }p_s(S)>0. $$
Return an available lottery maximizing declared expected utility. At a supported declaration, prefer its own lottery in a maximizing tie.

A supported type’s own lottery is available. The assumed supported comparisons show that its own lottery maximizes utility over all available supported lotteries. Thus the rule preserves the supported table and hence feasibility.

Now let $v$ be any true valuation, including one outside the support, and let $z$ be a permissible report. If reporting $z$ returns $p_s$, availability and permissibility give
$$ v_s(S)\le v_z(S)\le v(S) \quad\text{whenever }p_s(S)>0. $$
Consequently, $p_s$ is available at the truthful declaration. The truthful declaration selects a lottery giving at least its true expected utility. A deviation returning the empty lottery gives zero utility, which is also no larger than truthful utility.

The rule scans at most $\tau$ supported lotteries, each having at most two nonempty outcomes. Exact rational comparisons therefore take polynomial time in the input, table, and queried declaration lengths. $\square$

This proof uses the nonatomic premise: the society and supported table stay fixed during a deviation.

2. The dominance LP and the approximation infimum

For each society $I$, define $F(I)$ by the following LP. Its variables are the supported nonempty probabilities $p_{t,S}$.

The feasibility constraints are
$$ p_{t,S}\ge0,\qquad \sum_{S\in D_t}p_{t,S}\le1, $$
and
$$ \sum_t\mu_t\sum_{\substack{S\in D_t\\e\in S}}p_{t,S}\le q_e \quad\text{for every }e\in U. $$

For every supported pair with $D_r=D_t$ and
$$ v_r(S)\le v_t(S)\quad\text{for every }S\in D_t, $$
impose
$$ \sum_{S\in D_t}v_t(S)p_{t,S} \ge \sum_{S\in D_t}v_t(S)p_{r,S}. $$
The objective is welfare.

There are at most $2\tau$ variables and $O(m+\tau^2)$ constraints.

Necessity

Coordinatewise understatement is permissible regardless of which outcomes the reported lottery awards. Therefore every truthful mechanism’s supported table satisfies this LP. In particular,
$$ W(I)\le F(I)\le\mathrm{OPT}(I). $$

Polynomial-time sufficiency up to arbitrarily small loss

I use the standard rational linear-programming theorem in its exact form: a nonempty bounded rational polytope, specified by rational linear inequalities, admits an exact rational maximizer of a rational linear objective computable in polynomial time; the returned solution has encoding length polynomial in the specification length.

The dominance LP satisfies these hypotheses. The zero table is feasible, every variable lies in $[0,1]$, and all coefficients have polynomial total encoding length. Let $p^*$ be an exact optimum.

Fix a rational $\varepsilon\in(0,1)$ and put
$$ \delta=\frac14\min\left\{1,\min_{e\in U}q_e\right\}. $$
Define a baseline table $b$ by awarding every nonempty menu bundle with probability $\delta$. Each type’s total nonempty probability is at most $2\delta\le1/2$. Every good’s aggregate consumption is at most
$$ 2\delta\sum_t\mu_t=2\delta\le q_e. $$
Thus $b$ is feasible.

Types with the same menu receive identical baseline lotteries, so every dominance inequality holds for $b$ with equality. Hence
$$ p^\varepsilon=(1-\varepsilon)p^*+\varepsilon b $$
is feasible and satisfies every dominance inequality.

Every menu bundle has positive probability under $p^\varepsilon$. Consequently, a supported report is permissible exactly when it understates every menu coordinate. The dominance inequalities are therefore all supported incentive constraints for this table. The extension lemma makes the mechanism truthful throughout the declaration domain.

Because baseline welfare is nonnegative,
$$ W^\varepsilon(I)\ge(1-\varepsilon)F(I). $$
The exact LP solution, baseline, mixture, and declaration queries all have polynomial bit complexity.

It follows that $F(I)$ is the supremum of truthful welfare on a fixed instance. This does not establish attainment.

Define
$$ \rho=\sup_{I:\,\mathrm{OPT}(I)>0} \frac{\mathrm{OPT}(I)}{F(I)}. $$
Every uniform approximation guarantee is at least $\rho$. Conversely, for each fixed rational $\varepsilon\in(0,1)$, the construction above guarantees factor
$$ \frac{\rho}{1-\varepsilon}. $$
Thus, once finiteness is established below,
$$ \alpha_{\mathrm{inf}}=\rho. $$
This equality holds both with and without the polynomial-time restriction.

3. A polynomial-time factor-$2$ mechanism

Choose a canonical ordering of each two-bundle menu. Write its bundles as $S_1(D),S_2(D)$; for a singleton menu, repeat its sole bundle in both positions.

For each $j\in\{1,2\}$ solve
$$ Z_j=\max_y\sum_t v_t(S_j(D_t))y_t $$
subject to
$$ 0\le y_t\le\mu_t,\qquad \sum_{\substack{t\\e\in S_j(D_t)}}y_t\le q_e. $$
These rational LPs are nonempty and bounded, so the theorem stated above applies.

For a fixed $j$, average allocation probabilities within every group having the same menu and selected-bundle value:
$$ p_t= \frac{\sum_{s\text{ in the group}}y_s} {\sum_{s\text{ in the group}}\mu_s}. $$
This preserves resource consumption and welfare.

For types with the same menu, these probabilities satisfy
$$ v_r(S_j)\le v_t(S_j)\quad\Longrightarrow\quad p_r\le p_t. $$
Equal values are handled by averaging. For strictly ordered values, a contrary inequality $p_r>p_t$ would imply positive allocated mass at $r$ and unused mass capacity at $t$. Moving a sufficiently small positive mass from $r$ to $t$ preserves every resource constraint, since their selected bundle is identical, and strictly increases welfare. This contradicts optimality.

Award only the selected bundle, with probability $p_t$. A supported report with positive allocation probability is permissible only if its selected-bundle value is understated. Monotonicity gives the required utility inequality. Reports returning nothing give zero utility. The extension lemma handles all other declarations.

Choose the index attaining $\max\{Z_1,Z_2\}$. If $x^*$ is an unrestricted optimum, retaining only its $j$th bundle allocations gives a feasible vector for the $j$th LP. Across both vectors, every two-bundle allocation is counted once and every singleton allocation twice. Therefore
$$ Z_1+Z_2\ge\mathrm{OPT}, $$
and the mechanism obtains
$$ W\ge\frac{\mathrm{OPT}}2. $$

Consequently, $\rho\le2$. The same argument proves exact welfare maximization when every public menu is a singleton.

4. A five-type lower bound of $715/614$

Let
$$ U=\{a,b\},\qquad A=\{a\},\qquad B=\{a,b\}, $$
with supplies
$$ q_a=1,\qquad q_b=\frac{15}{32}. $$
All types have the nested menu $\{A,B\}$.

| Type $i$ | Mass $\mu_i$ | Value $a_i=v_i(A)$ | Value $v_i(B)$ |
|---|---:|---:|---:|
| $0$ | $15/32$ | $0$ | $1$ |
| $1$ | $3/32$ | $1/3$ | $1$ |
| $2$ | $4/32$ | $4/9$ | $1$ |
| $3$ | $5/32$ | $5/9$ | $1$ |
| $4$ | $5/32$ | $7/9$ | $1$ |

The masses sum to one, and all valuations respect inclusion.

Write
$$ u_i=\pi_i(A),\qquad w_i=\pi_i(B). $$
Then welfare is
$$ W=\sum_{i=0}^4\mu_i(a_i u_i+w_i). $$

Unrestricted optimum

For every feasible allocation,
$$ W \le \frac{15}{32}+\sum_{i=0}^4\mu_i a_i = \frac{55}{72}. $$
Here the first term bounds total welfare from $B$, whose value is always one, and $u_i\le1$ bounds each $A$ term.

Awarding $B$ to all type-$0$ individuals and $A$ to everyone else attains this bound. It consumes one unit of $a$ and $15/32$ units of $b$. Hence
$$ \mathrm{OPT}=\frac{55}{72}. $$

An exact incentive upper-bound certificate

Define
$$ C=\sum_{i=0}^4\mu_i w_i. $$
Feasibility gives
$$ C\le\frac{15}{32},\qquad u_4+w_4\le1. $$

For $i>j$, type $j$ understates both coordinates relative to type $i$. Its report is always permissible. Thus truthfulness requires
$$ G_{ij}:=a_i(u_j-u_i)+w_j-w_i\le0. $$

Consider the following positive linear combination of necessary inequalities:
$$ \begin{aligned} &2432C+1316(u_4+w_4) +561G_{10}+54G_{20}+684G_{21}\\ &\qquad{}+745G_{32}+157G_{42}+950G_{43} \le 2432\frac{15}{32}+1316 =2456. \end{aligned} $$
Expanding its left side gives the exact identity
$$ \begin{aligned} &2432C+1316(u_4+w_4) +561G_{10}+54G_{20}+684G_{21}\\ &\qquad{}+745G_{32}+157G_{42}+950G_{43} = 3744W+211u_0+4w_4. \end{aligned} $$
For completeness, the coefficients of $(u_i,w_i)$ on both sides are as follows.

| Type $i$ | Coefficient of $u_i$ | Coefficient of $w_i$ |
|---|---:|---:|
| $0$ | $211$ | $1755$ |
| $1$ | $117$ | $351$ |
| $2$ | $208$ | $468$ |
| $3$ | $325$ | $585$ |
| $4$ | $455$ | $589$ |

These equal the coefficients of $3744W$, with the additional terms $211u_0$ and $4w_4$. Since both additional terms are nonnegative,
$$ W\le\frac{2456}{3744}=\frac{307}{468}. $$

The certificate also bounds the dominance-LP optimum, because it uses only feasibility and dominance inequalities.

A truthful table attaining the bound

Use the probabilities

| Type $i$ | Probability $u_i$ of $A$ | Probability $w_i$ of $B$ |
|---|---:|---:|
| $0$ | $0$ | $73/117$ |
| $1$ | $0$ | $73/117$ |
| $2$ | $6/13$ | $49/117$ |
| $3$ | $6/13$ | $49/117$ |
| $4$ | $1$ | $0$ |

The two middle types have total nonempty probability $103/117$, so all lotteries are valid. Resource consumption is
$$ \sum_i\mu_i(u_i+w_i)=\frac{157}{208}\le1, $$
and
$$ \sum_i\mu_iw_i=\frac{15}{32}. $$
Their welfare is
$$ W=\frac{307}{468}. $$

To verify supported truthfulness, the truthful utilities, in type order, are
$$ \frac{73}{117},\quad \frac{73}{117},\quad \frac{73}{117},\quad \frac{79}{117},\quad \frac{91}{117}. $$

Reports $0$ and $1$ return the same pure-$B$ lottery. A report from type $2$ or $3$ awards both bundles, so it is permissible only for supported true types whose $A$ value is at least the reported $A$ value. Both reports return the same lottery. Report $4$ awards $A$ with probability one and is impermissible for every lower supported type.

Consequently:

Thus all supported comparisons hold. The extension lemma gives truthfulness throughout the declaration domain.

Therefore this instance has
$$ F=\frac{307}{468}, $$
and every uniform approximation factor satisfies
$$ \alpha\ge \frac{\mathrm{OPT}}F = \frac{55/72}{307/468} = \frac{715}{614}. $$

In particular,
$$ \frac{F}{\mathrm{OPT}}=\frac{614}{715}<\frac89, $$
so the universal inequality proposed in the earlier notes is false.

5. The extremal gap reduces to two goods and one common menu

Let $\rho_{\mathrm{one}}$ be the supremum of $\mathrm{OPT}/F$ over instances with two goods $a,b$ in which every supported type has the common menu
$$ \bigl\{\{a\},\{b\}\bigr\}. $$
The two bundles are incomparable, so every pair of nonnegative values is valid.

Reduction theorem.
$$ \rho=\rho_{\mathrm{one}}. $$
Moreover, for every fixed $m\ge2$, the extremal gap among instances with exactly $m$ goods also equals $\rho_{\mathrm{one}}$.

Proof. The inequality $\rho_{\mathrm{one}}\le\rho$ follows because these instances belong to the original model. I prove the reverse inequality.

Fix an arbitrary instance and an unrestricted optimum $x^*$. Partition its supported types by their public menus. For each menu $D$ and bundle $S\in D$, define
$$ c_{D,S}=\sum_{t:D_t=D}x^*_{t,S}. $$
Let $V_D$ be the welfare contributed by that group, so
$$ \sum_D V_D=\mathrm{OPT}. $$

I construct a dominance-feasible table within every group. It will consume at most $c_{D,S}$ mass of each bundle and obtain welfare at least $V_D/\rho_{\mathrm{one}}$.

Groups with at most one positively allocated bundle

If all capacities $c_{D,S}$ are zero, then $V_D=0$; award nothing.

Otherwise, suppose only one bundle $S$ has positive capacity. Solve
$$ \max_y\sum_{t:D_t=D}v_t(S)y_t $$
subject to
$$ 0\le y_t\le\mu_t,\qquad \sum_{t:D_t=D}y_t\le c_{D,S}. $$
The original allocation restricted to this group is feasible, so the optimum is at least $V_D$.

Averaging probabilities at equal $S$ values yields monotonicity in that value, by the exchange argument of Section 3. Awarding only $S$ therefore satisfies all supported incentive constraints, and hence all dominance constraints. Its welfare is at least $V_D$, which is at least $V_D/\rho_{\mathrm{one}}$.

This case includes singleton menus and two-bundle menus for which the optimum allocated only one bundle.

Groups with two positive bundle capacities

Let $D=\{S,T\}$ and suppose
$$ c_{D,S}>0,\qquad c_{D,T}>0. $$
Construct an auxiliary two-good instance:

The auxiliary supplies are positive. Its masses sum to one, and all declarations are valid because its bundles are incomparable. Duplicate zero-valued types, if present, may be merged.

The original group allocation, with the added zero-valued mass receiving nothing, is feasible in the auxiliary instance. Therefore its unrestricted optimum satisfies
$$ \mathrm{OPT}_D\ge V_D. $$
By the definition of $\rho_{\mathrm{one}}$, its dominance-LP optimum satisfies
$$ F_D\ge\frac{\mathrm{OPT}_D}{\rho_{\mathrm{one}}} \ge\frac{V_D}{\rho_{\mathrm{one}}}. $$

Take an optimal auxiliary dominance table. Set the lotteries of all zero-valued types to the empty lottery. This preserves welfare and feasibility. It also preserves dominance constraints: constraints whose true type has zero values are identically zero, while replacing a zero-valued reported type’s lottery by the empty lottery only decreases the right-hand side of other constraints.

Discard the added zero-valued mass and map the two bundles back to $S,T$. The resulting group table satisfies its dominance constraints, uses at most its two designated capacities, and obtains welfare at least $V_D/\rho_{\mathrm{one}}$.

Combining the groups

Dominance inequalities compare only types having the same public menu, so the constructed group tables can be combined.

For each original good $e$, total consumption is at most
$$ \sum_D\sum_{\substack{S\in D\\e\in S}}c_{D,S} = \sum_t\sum_{\substack{S\in D_t\\e\in S}}x^*_{t,S} \le q_e. $$
Thus the combined table is feasible for the original dominance LP. Its welfare is at least
$$ \sum_D\frac{V_D}{\rho_{\mathrm{one}}} = \frac{\mathrm{OPT}}{\rho_{\mathrm{one}}}. $$
Consequently,
$$ F\ge\frac{\mathrm{OPT}}{\rho_{\mathrm{one}}}, $$
which proves $\rho\le\rho_{\mathrm{one}}$.

For exactly $m>2$ goods, any auxiliary two-good instance can be embedded by adding $m-2$ unused goods with positive supplies. This changes neither optimum. Hence the same supremum applies for every $m\ge2$. $\square$

6. What remains unresolved

The proved conclusions are
$$ \alpha_{\mathrm{inf}} = \rho = \rho_{\mathrm{one}}, \qquad \frac{715}{614}\le\rho_{\mathrm{one}}\le2. $$

The stronger lower bound already uses a nested menu. The reduction shows that evaluating the infimum requires considering only one common menu of two singleton bundles, with arbitrary support size and arbitrary nonnegative value pairs.

Two substantive questions remain: the exact extremal value $\rho_{\mathrm{one}}$, and whether a mechanism attains that value as a uniform approximation factor. The positive-probability perturbation proves approximation arbitrarily close to the infimum, but does not settle attainment.

⟨structured verdict parsed — rendered above⟩

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

Verification report

The output establishes substantial partial results, but it does not determine the optimal approximation ratio requested in USER_TASK. Its central arguments are sound, subject to two minor clarifications in the reduction.

The verified substantive conclusions are the factor-$2$ polynomial-time mechanism, the lower bound $715/614$, and the characterization of the approximation infimum by a dominance-LP gap. No central false step was found.

1. Extension to the entire declaration domain

Assessment: correct.

The extension lemma addresses the full declaration domain, including unsupported true valuations and unsupported reports.

For a supported type, its own lottery is available. Every other available supported lottery satisfies exactly the premise of the assumed supported incentive comparison. Thus preferring its own lottery in a maximizing tie preserves the supported allocation.

For an arbitrary true valuation $v$, a permissible report $z$ returning a supported lottery $p_s$ gives, on every positively awarded outcome,
$$ v_s(S)\le v_z(S)\le v(S). $$
Therefore that same lottery is available when reporting truthfully. Maximizing truthful expected utility over available lotteries establishes the required incentive inequality. Empty lotteries cause no difficulty because values are nonnegative.

The runtime claim is justified: the mechanism scans at most $\tau$ lotteries, each with at most two nonempty outcomes, using exact rational comparisons. Polynomial encoding length of the supported table is explicitly assumed.

The nonatomic hypothesis is used correctly: deviations leave the society and allocation table fixed.

2. Dominance LP and approximation infimum

Assessment: correct.

Necessity

Coordinatewise understatement makes a supported report permissible regardless of its lottery’s support. Consequently, every truthful mechanism satisfies every stated dominance inequality. The bound
$$ W(I)\le F(I)\le\mathrm{OPT}(I) $$
follows.

Exact polynomial-time optimization

The stated rational linear-programming theorem has the required hypotheses:

Its application is justified.

Positive-probability perturbation

The baseline is feasible. In particular,
$$ 2\delta\le\frac12 $$
bounds each type’s total nonempty probability, and
$$ 2\delta\le q_e $$
bounds consumption of every good. This remains valid when both bundles contain the same good.

Identical baseline lotteries within each menu make all dominance inequalities equalities. Mixing with the optimum therefore preserves feasibility and dominance constraints.

Every menu outcome then has strictly positive probability, so supported permissibility becomes precisely coordinatewise understatement. The extension lemma applies, and nonnegative baseline welfare gives
$$ W^\varepsilon(I)\ge(1-\varepsilon)F(I). $$

The distinction between a supremum and attainment is correctly maintained.

Uniform approximation infimum

Necessity bounds every uniform approximation factor below by $\rho$. For each fixed rational $\varepsilon$, the construction is a uniform polynomial-time mechanism with factor
$$ \frac{\rho}{1-\varepsilon}. $$
Together with the finite upper bound established in Section 3, this justifies equality of the approximation infimum and $\rho$, both with and without the polynomial-time restriction.

3. Factor-$2$ mechanism

Assessment: correct.

Averaging within groups having the same menu and selected-bundle value preserves welfare and consumption: all members have the same selected bundle and the same objective coefficient.

The exchange argument establishes the claimed monotonicity. If
$$ v_r(S_j)<v_t(S_j),\qquad p_r>p_t, $$
then type $r$ has positive allocated mass and type $t$ has unused capacity. Transferring sufficiently small positive mass between their identical selected bundles preserves all resource constraints and strictly increases welfare, contradicting optimality. Averaging handles equal values.

For a supported report receiving the selected bundle with positive probability, permissibility requires understatement of its value. Monotonicity and nonnegative true values yield the incentive inequality. Reports receiving nothing yield zero utility. The extension lemma supplies truthfulness for unsupported declarations.

Restricting an unrestricted optimum to each selected bundle gives feasible allocations for the two LPs. Two-bundle allocations are counted once across them, and singleton allocations twice. Therefore
$$ Z_1+Z_2\ge\mathrm{OPT}, $$
and choosing the better mechanism guarantees
$$ W\ge\frac{\mathrm{OPT}}2. $$

Choosing between the mechanisms based on the society is compatible with nonatomic deviations. The singleton-menu exact-optimality conclusion also follows from the same argument.

4. Five-type lower bound

Assessment: correct; all critical arithmetic checks.

The masses sum to $1$, supplies are positive, and all five valuations satisfy inclusion monotonicity on the nested menu.

Unrestricted optimum

The stated upper bound evaluates to
$$ \frac{15}{32}+\sum_i\mu_i a_i=\frac{55}{72}. $$
Awarding $B$ to type $0$ and $A$ to everyone else attains it and meets both supplies. Hence the claimed unrestricted optimum is exact.

Incentive certificate

For every $i>j$, type $j$ understates both coordinates. Thus each inequality $G_{ij}\le0$ is necessary for truthfulness and is included among the dominance constraints.

All certificate multipliers are positive. Re-expanding the combination gives exactly the reported coefficients:

| Type | Coefficient of $u_i$ | Coefficient of $w_i$ |
|---|---:|---:|
| $0$ | $211$ | $1755$ |
| $1$ | $117$ | $351$ |
| $2$ | $208$ | $468$ |
| $3$ | $325$ | $585$ |
| $4$ | $455$ | $589$ |

These agree with
$$ 3744W+211u_0+4w_4. $$
The right-hand side bound is exactly $2456$. Nonnegativity therefore gives
$$ W\le\frac{2456}{3744}=\frac{307}{468}. $$

Attaining table

Direct calculation confirms
$$ \sum_i\mu_i(u_i+w_i)=\frac{157}{208}, \qquad \sum_i\mu_iw_i=\frac{15}{32}, \qquad W=\frac{307}{468}. $$

The truthful utilities are exactly
$$ \frac{73}{117},\quad \frac{73}{117},\quad \frac{73}{117},\quad \frac{79}{117},\quad \frac{91}{117}. $$
Every permissible supported comparison satisfies the incentive inequality. In particular, verification checks only $B$ for reports $0$ and $1$, both of which return the same lottery; the analysis correctly accommodates this.

Thus the table is truthful after extension and attains the certificate bound. The conclusions
$$ F=\frac{307}{468}, \qquad \frac{\mathrm{OPT}}F=\frac{715}{614}, \qquad \frac{F}{\mathrm{OPT}}=\frac{614}{715}<\frac89 $$
are correct. Numerically, this also exceeds the stated comparison bound $9/8$; the historical assertion about earlier results is not independently documented in the supplied material.

5. Reduction to one common singleton menu

Assessment: sound in substance, with two minor gaps.

Partitioning by public menu is valid because dominance inequalities never compare different menus.

For groups with at most one positively allocated bundle, the single-bundle LP and the previously established exchange argument justify the claimed dominance-feasible allocation.

For groups with two positive capacities, mapping the bundles to incomparable singletons preserves the numerical dominance constraints. Original inclusion restrictions pose no problem: value pairs satisfying them remain valid for an incomparable menu.

Replacing all zero-valued types’ lotteries by empty lotteries preserves welfare, feasibility, and dominance constraints for the reasons stated. This also resolves the handling of merged zero-valued types when the added mass is discarded.

Finally, bounding each bundle’s allocated mass by its designated capacity correctly bounds consumption of every original good, including goods belonging to overlapping bundles. Embedding a two-good instance using unused goods preserves both optima.

Minor issue: rationality of the auxiliary instance

Where: Section 5, “Fix an arbitrary instance and an unrestricted optimum $x^*$.”

The auxiliary supplies are derived from $x^*$. To invoke $\rho_{\mathrm{one}}$, they must satisfy the original input’s rationality requirements. The write-up does not explicitly select a rational optimum.

Minimum clarification: State that $x^*$ is chosen to be a rational optimum using the rational LP theorem already stated, and consequently the capacities and auxiliary masses are rational.

This is routine and requires no new mathematical argument.

Minor issue: auxiliary optimum may be zero

Where: Section 5, “By the definition of $\rho_{\mathrm{one}}$.”

The defining supremum excludes instances with zero unrestricted optimum. Having two positive bundle capacities does not ensure positive welfare: an unrestricted optimum can allocate bundles to a wholly zero-valued menu group. The auxiliary instance then has
$$ \mathrm{OPT}_D=0. $$
The stated appeal to the definition does not cover that case.

Minimum clarification: Explicitly handle the zero-optimum auxiliary case before invoking the ratio definition for positive-optimum auxiliary instances.

This is an easily checked edge case, not a substantive obstacle to the reduction.

6. Resolution of the assigned task

Assessment: partial.

The prover accurately describes its work as partial. The bounds and reduction do not determine the exact value of $\rho_{\mathrm{one}}$, and equality of an infimum does not establish that a mechanism attains it.

Major incompleteness relative to USER_TASK: The optimal worst-case approximation ratio remains undetermined. A complete answer must determine the exact extremal value and address whether it is achievable as a uniform polynomial-time guarantee. This is outstanding mathematics, not an expositional repair.

The direction is promising: the certified lower bound, polynomial-time upper bound, and reduction constitute genuine progress.

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