← back to the atlas

d4-conf-ecai-2023-0323 (d4-conf-ecai-2023-0323)

Answer: —

The anchor (named result in the paper)

Theorem 3. — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateFor instances with 3 agents, Procedure $\threealgoDB$ returns a budget-feasible EFx allocation with constant efficiency.

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

The continuous mirror question, as graded

Given rational data for three types \(t\), with masses \(\mu_t\) summing to \(1\), additive valuations \(v_t\), budgets \(B_t\), item costs \(c_g\), and per-capita supplies \(q_g\), assign mass \(x_{t,k}\) of each type to integral bundles \(k\in\mathbb{Z}_{\ge 0}^m\). Require \(\sum_k x_{t,k}=\mu_t\), \(\sum_{t,k}x_{t,k}k_g\le q_g\), and budget feasibility for each assigned bundle. Require every positive-mass recipient of bundle \(k\) to satisfy EFx against every bundle \(\ell\) in the allocation’s support, using their type’s valuation and budget. Is there a polynomial-time algorithm, in \(m\) and the rational input bit length, that returns a sparse rational mass allocation with EFx and population NSW at least \(\rho\) times the maximum NSW among budget-feasible allocations with the same mass and supply constraints, for some absolute constant \(\rho>0\)?

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

A society is given by its support: a list of \(\tau=3\) types with positive binary-rational masses \(\mu_t\) summing to \(1\); \(\tau\) is the support size, not the number of possible types.
There are \(m\geq1\) item categories with interchangeable indivisible copies. Input values \(v_{tg}\), budgets \(B_t\), costs \(c_g\), and per-capita supplies \(q_g\) are nonnegative binary rationals; \(L\) is the total input bit length. Write \(v_t(k)=\sum_g v_{tg}k_g\) and \(c(k)=\sum_g c_gk_g\).
A mass allocation assigns nonnegative masses \(x_{t,k}\) to bundles \(k\in\mathbb Z_{\geq0}^m\), with \(\sum_kx_{t,k}=\mu_t\), \(\sum_{t,k}x_{t,k}k_g\leq q_g\), and \(c(k)\leq B_t\) whenever \(x_{t,k}>0\). Unused supply is permitted.
Let \(\mathcal S(x)=\{\ell:\sum_t x_{t,\ell}>0\}\). Budget-relative EFx requires, for every \(x_{t,k}>0\), every \(\ell\in\mathcal S(x)\), every integer subbundle \(0\leq s\leq\ell\) with \(c(s)\leq B_t\), and every \(g\) with \(s_g>0\), that \(v_t(k)\geq v_t(s-e_g)\), where \(e_g\) is the unit vector. This includes comparisons within a type and removal of zero-valued copies.
Population Nash welfare is \(\operatorname{NSW}(x)=\exp(\sum_{t,k:x_{t,k}>0}x_{t,k}\log v_t(k))\), with value zero if any positive mass receives zero utility. Let \(\operatorname{OPT}\) be its supremum over all feasible mass allocations, allowing real masses, without requiring EFx.

Does there exist an absolute constant \(\rho>0\) and an algorithm running in \(\operatorname{poly}(m,\tau,L)\) that always returns a budget-feasible EFx allocation \(x\), represented by polynomially many bundle–mass pairs with binary-rational masses, satisfying \(\operatorname{NSW}(x)\geq\rho\operatorname{OPT}\)?

For three discrete agents, a procedure guarantees budget-feasible EFx and at least \(1/171\) of unrestricted optimal budget-feasible Nash welfare; it uses maximum-Nash-welfare allocations as subroutines and supplies no polynomial-time guarantee. [Source](https://arxiv.org/html/2305.02280).
No result settling this precise distribution-over-types problem was located in the literature search.

Modeling choices made when packaging the task

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

Partial result: a polynomial-time algorithm for proportional values and zero costs

The general question remains unresolved. I prove a constant-factor algorithm for a subclass with arbitrarily many categories and binary-encoded supplies.

Proven result. Suppose all item costs are zero and the three value vectors are positive scalar multiples of one common nonnegative vector:
$$ c_g=0,\qquad v_{tg}=\alpha_t w_g,\qquad \alpha_t>0. $$
Then a polynomial-time algorithm returns a budget-feasible EFx allocation with at most $m+3$ bundle–mass pairs, all of polynomial binary encoding length, satisfying
$$ \operatorname{NSW}(x)\geq e^{-1}\operatorname{OPT}. $$

The proportionality and zero-cost conditions are additional hypotheses. They are not assumed in the general task.

1. Normalization and the zero-welfare case

Choose $w=v_1$, so $\alpha_1=1$. Proportionality can be checked using exact rational arithmetic. If every value is zero, return the empty allocation.

Discard categories with $w_g=0$, leaving their supplies unused. Write
$$ u(k)=\sum_g w_gk_g,\qquad A=\sum_g w_gq_g,\qquad Q=\sum_{g:w_g>0}q_g. $$
Every retained category has strictly positive normalized value.

For any allocation, define its normalized welfare by
$$ W(x)=\exp\left(\sum_{t,k:x_{t,k}>0}x_{t,k}\log u(k)\right), $$
with value zero when some positive mass receives normalized utility zero. Since each type has total mass $\mu_t$,
$$ \operatorname{NSW}(x) = \left(\prod_{t=1}^3\alpha_t^{\mu_t}\right)W(x). $$
Consequently, approximation ratios are unchanged by normalization.

Because costs are zero, all bundles and all comparison subbundles are affordable. Proportionality makes EFx equivalent to
$$ u(k)\geq u(\ell-e_g) $$
for every positively assigned pair $(t,k)$, every supported bundle $\ell$, and every occupied category $g$ in $\ell$. Indeed, these full-bundle inequalities imply the required subbundle inequalities because
$$ u(s-e_g)\leq u(\ell-e_g) \qquad\text{whenever }s\leq\ell. $$

If $Q<1$, positive welfare is impossible: every positive-utility recipient needs at least one retained copy, whereas the population has total mass one. Thus $\operatorname{OPT}=0$, and the empty allocation satisfies the requested inequality.

Henceforth assume $Q\geq1$.

2. Greedy allocation preserves EFx

Process retained categories in nonincreasing order of $w_g$. Start with the empty bundle assigned to every type.

An elementary greedy move selects a positively assigned bundle of minimum normalized utility and gives one copy of the current category to some positive mass receiving that bundle.

Lemma 1. Every elementary greedy move preserves EFx.

Proof. Let the selected bundle be $k$, let
$$ b=u(k)=\min\{u(j):j\text{ is supported}\}, $$
and let the current category have value $w$.

Every copy already allocated has value at least $w$, by the processing order. Therefore every copy in the new bundle $k+e_g$ has value at least $w$. Removing any copy from that bundle leaves utility at most
$$ u(k)+w-w=b. $$
Every recipient after the move has utility at least $b$. Thus all comparisons against the new bundle satisfy EFx.

Comparisons against previously supported bundles remain valid: unchanged recipients retain their inequalities, and recipients receiving the new bundle increase their utility. Splitting the selected mass between its old and new bundles causes no additional difficulty, since both sets of comparisons have just been checked. $\square$

The next section implements potentially enormous sequences of these moves without processing copies individually.

3. A polynomial implementation for binary-encoded supplies

3.1 Allocating one category in bulk

Suppose the current allocation has $r$ positive pairs, indexed by $i$, with masses $\beta_i$, bundles $k_i$, and utilities
$$ u_i=u(k_i). $$
Let the next category have value $w>0$ and supply $q$.

Choose a common positive integer denominator $D$ for all retained values $w_g$. Since every $u_i$ is an integer combination of those values, write
$$ U_i=Du_i\in\mathbb Z_{\geq0}, \qquad W=Dw\in\mathbb Z_{>0}. $$
For an integer $H\geq0$, define
$$ n_i(H)= \max\left\{0,\left\lceil\frac{H-U_i}{W}\right\rceil\right\}, \qquad C(H)=\sum_i\beta_i n_i(H). $$
Here $n_i(H)$ counts the successive copies whose utility immediately before receipt would be strictly below $H/D$.

Find the largest integer $H$ satisfying
$$ C(H)\leq q. $$
Equivalently,
$$ C(H)\leq q<C(H+1). $$
Such an integer exists because $C(0)=0$ and $C(H)$ tends to infinity.

Set $n_i=n_i(H)$ and
$$ R=q-C(H). $$
The difference between consecutive values of $C$ is
$$ C(H+1)-C(H) = \sum_{i:U_i+n_iW=H}\beta_i. $$
Thus $R$ can be distributed among exactly the indices satisfying $U_i+n_iW=H$: choose rational numbers $r_i$ with
$$ 0\leq r_i\leq\beta_i,\qquad \sum_i r_i=R, $$
and set $r_i=0$ for all other indices.

Replace pair $i$ by
$$ \begin{array}{c|c} \text{bundle}&\text{mass}\\ \hline k_i+n_ie_g&\beta_i-r_i\\ k_i+(n_i+1)e_g&r_i \end{array} $$
and omit zero masses.

This preserves type totals and consumes exactly $q$ copies of the current category.

It also preserves EFx. To verify this, consider the finite collection of increments with levels
$$ U_i+aW<H, \qquad 0\leq a<n_i. $$
Perform these increments in increasing order of their levels, assigning the full mass $\beta_i$ at each increment. Every increment’s predecessors have lower levels, so this order gives copies only to minimum-utility recipients. Afterward, perform the indicated partial increments at level $H$. This is a finite sequence of the elementary moves in Lemma 1, with exactly the bulk allocation as its endpoint.

The sequence may be exponentially long, but the formulas compute its endpoint directly.

3.2 Compressing the support

After the bulk operation there are at most $2r$ pairs. Compress them while preserving every type’s mass and every category’s consumption.

For each pair $(t_i,k_i)$, use the integer column
$$ a_i=(e_{t_i},k_i)\in\mathbb Z^{3+m}, $$
where $e_{t_i}$ is the corresponding type indicator.

If the positive columns are linearly dependent, find a nonzero integer vector $z$ with
$$ \sum_i z_i a_i=0. $$
The type rows imply $\sum_i z_i=0$, so $z$ has both positive and negative entries. Set
$$ \theta=\min_{i:z_i>0}\frac{\beta_i}{z_i}, \qquad \beta_i'=\beta_i-\theta z_i. $$
All new masses are nonnegative, at least one becomes zero, and all recorded totals remain unchanged.

Repeat until the remaining columns are independent. There are then at most $m+3$ positive pairs.

Compression preserves EFx: it retains only bundles from the previous support, and all inequalities between those bundles already held.

3.3 Polynomial encoding length and running time

The following bound prevents successive operations from producing bundles of increasing encoding length.

Lemma 2. In every intermediate EFx allocation,
$$ u(\ell)\leq A+\max_g w_g $$
for every supported bundle $\ell$.

Proof. For nonempty $\ell$, choose an occupied category $g$. EFx gives
$$ u(k)\geq u(\ell)-w_g $$
for every recipient. Averaging over the population, whose total mass is one, gives
$$ A_{\mathrm{used}}\geq u(\ell)-w_g. $$
Since $A_{\mathrm{used}}\leq A$, the stated bound follows. The empty bundle also satisfies it. $\square$

Consequently, each retained coordinate satisfies
$$ k_g\leq\frac{A+\max_h w_h}{w_g}. $$
Every positive input rational is between $2^{-L}$ and $2^L$, so
$$ A\leq m2^{2L}, \qquad k_g\leq m2^{3L}+2^{2L}. $$
Thus every bundle coordinate has $O(L+\log m)$ bits.

After compression, the independent positive columns determine their masses uniquely. Select a nonsingular square subsystem of their rows. Its coefficients are bounded bundle counts and type indicators; its right-hand side consists of input type masses, processed supplies, and zeros. Clearing right-hand-side denominators and applying Cramer’s rule shows that every resulting mass has polynomial encoding length. Indeed, for a matrix of order $s\leq m+3$ with integer entries bounded by $M$, its determinant has absolute value at most
$$ s!M^s. $$

Compression itself is polynomial-time. Gaussian elimination finds the dependence vector $z$ with polynomially many bits. If the current masses have common denominator $T$, an elimination step can use common denominator $T|z_j|$, where $j$ attains the minimum defining $\theta$. There are at most $2r$ elimination steps, so intermediate rational arithmetic also has polynomial bit length.

The cutoff search is polynomial-time as well. With
$$ \beta_{\min}=\min_i\beta_i,\qquad U_{\max}=\max_iU_i, $$
the integer
$$ H_{\mathrm{hi}} = U_{\max} + \left(\left\lfloor\frac q{\beta_{\min}}\right\rfloor+2\right)W+1 $$
satisfies $C(H_{\mathrm{hi}})>q$. Its binary length is polynomial by the mass and bundle bounds above. Binary search therefore uses polynomially many evaluations of $C$, each involving polynomial-time rational arithmetic.

There are at most $m$ bulk operations. After each compression the support has at most $m+3$ pairs. The entire algorithm runs in polynomial time and uses only rational arithmetic.

4. Every complete EFx allocation in this subclass has a constant welfare guarantee

The algorithm consumes every retained category’s supply. Its final allocation has positive welfare.

To see positivity, suppose an empty bundle received positive mass. Its normalized utility is zero. EFx would then prohibit every supported bundle containing at least two retained copies, since removing one such copy leaves positive utility. All nonempty supported bundles would therefore be singletons, giving total consumption strictly below one. This contradicts complete consumption of $Q\geq1$ copies.

We now prove the welfare guarantee for any finite-support, positive-welfare EFx allocation that consumes all retained supply.

Let
$$ a=\min\{u(k):k\text{ is supported}\}>0. $$
Define the large categories and their total supply by
$$ G_{\mathrm{large}}=\{g:w_g>a\}, \qquad h=\sum_{g\in G_{\mathrm{large}}}q_g. $$

4.1 Large copies must be singletons

If a supported bundle contained a large copy and another copy, removing the other copy would leave utility greater than $a$, violating EFx for a minimum-utility recipient.

Thus every large copy is assigned as a singleton. Because supply is completely consumed, these singleton recipients have total mass $h$.

Every remaining recipient receives only categories with $w_g\leq a$. For any such bundle $\ell$, EFx gives
$$ u(\ell)\leq a+w_g\leq2a $$
for every occupied category $g$. Hence, writing
$$ A_{\mathrm{small}}=\sum_{g\notin G_{\mathrm{large}}}w_gq_g, $$
we obtain
$$ A_{\mathrm{small}}\leq2a(1-h). $$

Put
$$ J=\sum_{g\in G_{\mathrm{large}}}q_g\log\frac{w_g}{a}. $$
Large singleton recipients contribute their exact utilities, and all other recipients have utility at least $a$. Therefore
$$ \log W(x)\geq\log a+J. $$

4.2 An upper bound on unrestricted welfare

Define nonnegative coefficients
$$ p_g= \begin{cases} w_g/a,&w_g\leq a,\\ 1+\log(w_g/a),&w_g>a. \end{cases} $$

For every positive-utility bundle $k$, I claim that
$$ \log\frac{u(k)}a\leq\sum_g p_gk_g-1. $$

To prove this, let $z$ be its small-copy utility divided by $a$, and list its large-copy value ratios as $r_1,\ldots,r_n$, each strictly greater than one.

If $n=0$, then $z>0$, and the claim is the standard inequality
$$ \log z\leq z-1. $$
If $n\geq1$, put $R=\sum_{j=1}^n r_j$. Since each $r_j\geq1$,
$$ R\leq n\prod_{j=1}^n r_j, \qquad \log R\leq n-1+\sum_{j=1}^n\log r_j. $$
Also $R\geq1$, so
$$ \log(R+z) = \log R+\log\left(1+\frac zR\right) \leq n-1+\sum_{j=1}^n\log r_j+z. $$
This is the claimed inequality.

Now let $y$ be any unrestricted feasible allocation with positive welfare. Summing the pointwise inequality and using the supply constraints gives
$$ \begin{aligned} \log W(y) &\leq \log a-1+\sum_g p_gq_g\\ &=\log a-1+\frac{A_{\mathrm{small}}}{a}+h+J\\ &\leq\log a+J+1-h\\ &\leq\log W(x)+1. \end{aligned} $$
This argument also covers countable supports. Positive normalized utility is bounded below by the smallest retained value, while the nonnegative price expression has finite expectation by the supply constraints. Thus the sums used above are well-defined.

Zero-welfare allocations satisfy the resulting bound automatically. Taking the supremum over all feasible allocations yields
$$ W(x)\geq e^{-1}\sup_y W(y). $$
Restoring the common multiplicative normalization factor proves
$$ \operatorname{NSW}(x)\geq e^{-1}\operatorname{OPT}. $$

5. What remains open

This settles a subclass with arbitrarily many categories, arbitrarily large binary-encoded supplies, and three distinct types—for example, three different positive scaling factors $\alpha_t$.

The proof uses both additional hypotheses essentially. Proportionality provides a common ordering of recipient utilities and copy values; zero costs make every greedy addition budget-feasible. Neither step has been established for the general instance in the task.

⟨structured verdict parsed — rendered above⟩

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

Verification report

The output establishes a sound constant-factor result for the stated subclass, subject to two minor implementation clarifications. It does not resolve the general task, and it explicitly acknowledges this limitation. No central mathematical step in the subclass proof is false.

The overall classification is partial: the general question allows nonproportional valuations and nonzero costs, whereas the proved algorithm requires proportional valuations and zero costs.

1. Scope of the claim

The additional assumptions are explicitly stated:
$$ c_g=0,\qquad v_{tg}=\alpha_t w_g,\qquad \alpha_t>0. $$

Under these assumptions, the output claims a polynomial-time algorithm with at most $m+3$ positive bundle–mass pairs and approximation factor $e^{-1}$.

These assumptions substantially restrict the task. Neither the existence of a constant-factor EFx allocation nor a polynomial-time construction is established for general inputs.

Severity: major relative to completing the assigned task. This is an acknowledged scope limitation, not a hidden flaw in the subclass proof.

Required further work: Resolve the general instance class. Clarifying the present write-up alone cannot remove this limitation.

2. Normalization and degenerate cases

Normalization

For a nonzero common vector, taking $w=v_1$ and $\alpha_1=1$ is valid. Positive proportionality ensures that every other type has a positive scaling factor.

The identity
$$ \operatorname{NSW}(x) = \left(\prod_{t=1}^{3}\alpha_t^{\mu_t}\right)W(x) $$
follows because each type receives total mass $\mu_t$. It also holds under the stated zero-welfare convention. Thus normalized and original approximation ratios coincide.

Discarding zero-valued categories

Leaving categories with $w_g=0$ unused is permitted. Under proportionality they have zero value for every type, so removing them does not reduce any attainable utility. The constructed allocation consequently contains no zero-valued copies.

EFx equivalence

With zero costs, every subbundle is affordable. Positive scaling factors cancel from the comparisons. Necessity follows by choosing $s=\ell$; sufficiency follows from nonnegativity:
$$ u(s-e_g)\leq u(\ell-e_g). $$

This equivalence is correct, including the task’s convention about removing zero-valued copies.

The case $Q<1$

If welfare is positive, every positive-mass recipient must receive at least one retained copy. Total retained-copy consumption would therefore be at least the total population mass, which is one. Hence $Q<1$ implies $\operatorname{OPT}=0$.

Minor issue: “Return the empty allocation” is ambiguous. Literally returning no bundle–mass pairs violates the type-total constraints.

Minimum clarification: State that each type receives its empty bundle with mass $\mu_t$. Apply this interpretation both when all values vanish and when $Q<1$.

3. Greedy preservation of EFx

Lemma 1 is correct.

At a move of value $w$, every previously allocated copy has value at least $w$. Thus removing any copy from the new bundle leaves utility at most the selected minimum utility $b$. Every recipient after the move has utility at least $b$.

Comparisons against old supported bundles remain valid because unchanged recipients retain their utilities and changed recipients gain utility. Splitting a selected mass leaves both groups covered by these comparisons.

The processing order is essential and is explicitly supplied.

4. Bulk implementation

Threshold formulas

For integer $H$, the formula
$$ n_i(H)=\max\left\{0,\left\lceil\frac{H-U_i}{W}\right\rceil\right\} $$
correctly counts increments whose utility immediately before receipt is strictly below $H/D$.

The function $C(H)$ is nondecreasing and unbounded because the masses are positive and $W>0$. Consequently, the largest feasible integer $H$ exists.

The jump formula
$$ C(H+1)-C(H) = \sum_{i:U_i+n_iW=H}\beta_i $$
is correct: an increment enters the count precisely when its integer starting level equals $H$.

Maximality gives
$$ 0\leq R<C(H+1)-C(H), $$
so the stated residual distribution is possible.

Endpoint feasibility and EFx

The replacement preserves each pair’s total mass and uses
$$ \sum_i\beta_i n_i+\sum_i r_i=q $$
copies.

The conceptual ordering of increments is valid. Every predecessor of a listed increment has a strictly smaller level. At each listed level, no recipient remains below that level; otherwise that recipient’s next increment would have appeared earlier. The residual increments occur at the minimum level $H$.

Thus the bulk endpoint is obtainable by the elementary EFx-preserving moves. The conceptual sequence may be very long, but it is finite and need not be executed.

Minor issue: The instruction to “choose rational numbers $r_i$” does not specify how to make that choice with polynomial encoding length. An arbitrary rational choice could introduce unnecessarily large denominators.

Minimum clarification: Specify a residual-distribution routine and state its encoding-length bound. This is an implementation omission, not a missing mathematical existence argument.

5. Support compression

The compression argument is correct.

The type rows imply
$$ \sum_i z_i=0. $$
A nonzero dependence vector therefore has both positive and negative entries. The prescribed value of $\theta$ keeps all masses nonnegative and removes at least one positive pair.

All type totals and category consumptions are preserved. Termination leaves linearly independent columns in dimension $m+3$, giving the claimed support bound.

EFx is preserved because compression only removes supported pairs; every remaining comparison already held. Zero costs ensure budget feasibility throughout.

Compression need not preserve welfare. The proof correctly avoids relying on such preservation: its final welfare guarantee applies to every complete, positive-welfare EFx allocation in the subclass.

6. Encoding length and running time

Lemma 2 is valid. Averaging the EFx comparison against a supported bundle $\ell$ yields
$$ A_{\mathrm{used}}\geq u(\ell)-w_g, $$
and feasibility gives $A_{\mathrm{used}}\leq A$.

The numerical bounds
$$ A\leq m2^{2L}, \qquad k_g\leq m2^{3L}+2^{2L} $$
follow from the stated input bounds. Thus bundle coordinates have polynomial encoding length.

After compression, independence makes the masses uniquely determined by a nonsingular subsystem. Its right-hand side consists of input type masses and category consumptions, which are processed supplies or zero. The determinant bound
$$ |\det M|\leq s!M_{\max}^{s} $$
provides the required polynomial bit bound through Cramer’s rule.

The dependence-vector and intermediate-denominator arguments are also adequate: dependence vectors depend on the bounded integer columns, and only polynomially many elimination steps occur between compressions.

A common denominator $D$ for the retained input values has polynomial bit length. The proposed search upper bound satisfies $C(H_{\mathrm{hi}})>q$, and its encoding length is polynomial. Binary search therefore takes polynomially many evaluations.

Subject to specifying the residual-distribution routine noted above, the polynomial-time claim is justified.

7. Positivity of the final welfare

The positivity argument is correct for the constructed allocation, which contains only retained categories.

If an empty bundle had positive mass, EFx would forbid every supported bundle containing at least two retained copies. All nonempty bundles would be singletons. Their total mass, and hence total copy consumption, would then be strictly below one, contradicting complete consumption when $Q\geq1$.

This also covers the boundary case $Q=1$.

8. Welfare guarantee

Structure of large copies

If $w_g>a$, any bundle containing that copy and another copy violates EFx for a recipient with utility $a$: removing the other copy leaves utility strictly greater than $a$.

Thus large copies must be singletons. Complete consumption makes their recipient mass exactly $h$.

Every remaining bundle uses copies of value at most $a$. EFx bounds its utility by $2a$, yielding
$$ A_{\mathrm{small}}\leq2a(1-h). $$
The lower bound
$$ \log W(x)\geq\log a+J $$
correctly accounts for the large singleton utilities and the lower bound $a$ for all other recipients.

Pointwise upper bound

For bundles with no large copies, the stated inequality is exactly
$$ \log z\leq z-1. $$

For bundles with large-copy ratios $r_1,\ldots,r_n>1$, the bounds
$$ R\leq n\prod_{j=1}^{n}r_j, \qquad \log n\leq n-1 $$
justify the claimed estimate for $\log R$. Since $R\geq1$, the subsequent estimate using $\log(1+z/R)\leq z/R\leq z$ is valid.

Therefore the pointwise price inequality is correct.

Summation and supremum

The coefficients $p_g$ are nonnegative, so supply constraints give the stated upper bound for every unrestricted allocation with positive welfare. Substituting the bound on $A_{\mathrm{small}}$ yields
$$ \log W(y)\leq\log W(x)+1. $$

The countable-support justification is sufficient: positive utility is bounded below by the smallest retained value, and the nonnegative price expression has finite expectation. The logarithmic expectations are consequently well-defined and finite for positive-welfare allocations.

Zero-welfare allocations satisfy the bound automatically. Taking the supremum and restoring normalization establishes the claimed factor $e^{-1}$.

9. Overall assessment

The subclass result is genuine progress. Its mathematical argument stands, with minor clarifications needed for the empty-bundle output and residual-mass implementation.

The general distribution-over-types problem remains unresolved. The output supplies neither a general algorithm nor a counterexample or hardness result.

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