Answer: Unconditional termination fails under \(\epsilon_r=\epsilon 2^{-r}\). Every terminal output satisfies \(W_v(y)\ge\Delta^\star\operatorname{OPT}_v\), and a terminating transcript exists with at most one refinement round. Construction is \(\mathrm{NP}\)-hard even for \(m=2\), \(\tau=2\), and every fixed \(\Delta^\star>0\), while admitting time \(2^{\operatorname{poly}(B)}\operatorname{poly}(m,L)\).
Theorem 6 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateWhen ICE incorporates δ-MRPAR and ǫ-DIAR and when all bidders are straightforward, then the exchange terminates with a trade that is within target approxi- mation error ∆∗, for any ∆∗≥0 as ǫ →0. The use of ǫ-DIAR by itself is sufficient to establish this result. However, it is the use of prices and MRPAR that drives most elicitation in practice, particularly as we fix δ in δ-MRPAR to a tiny constant in actual use. Empirical support for this, along with the quality of the price-based bound and the direct efficiency bounds, is provided in Section 6.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite type set \(T\), rational masses \(\mu_t\), integral per-agent endowments, TBBL trees with valuation bounds, and parameters \(\Delta^\star,\delta,\epsilon>0\), compute a feasible mass allocation \(y\), common item prices \(\pi\), and a synchronized type-level ICE transcript using \(\delta\)-MRPAR and \(\epsilon\)-DIAR; determine whether the process terminates with \(W_v(y)\ge \Delta^\star\operatorname{OPT}_v\), and characterize its complexity in the type/profile encoding as \(\epsilon\to0\).
A society is given by its support: the list of the \(\tau\) types with positive mass, each mass \(\mu_t\) a binary rational, with \(\sum_t\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types. There are \(m\) goods; type \(t\) has an endowment \(e_t\in\mathbb Z_{\ge0}^m\) and a finite tree whose nodes have rational true coefficients \(a_{t\beta}\) and initial bounds \(\ell_{t\beta}\le a_{t\beta}\le u_{t\beta}\). True coefficients are available to the transcript constructor but remain private in the simulated exchange. Let \(B\) be the total number of tree nodes and \(L\) the total binary input length.
A TBBL leaf carries a signed integer quantity of one good, written \(q_{t\beta j}\); internal node \(\beta\) carries integers \(0\le h_\beta\le k_\beta\le |\operatorname{Child}(\beta)|\). A satisfaction vector \(s\in\{0,1\}^{T_t}\) is valid for an integer trade \(\lambda\) when \(h_\beta s_\beta\le\sum_{\gamma\in\operatorname{Child}(\beta)}s_\gamma\le k_\beta s_\beta\) and \(\sum_{\beta\text{ leaf}}q_{t\beta j}s_\beta\le\lambda_j\). For coefficients \(w_t\), define \(v_t^w(\lambda)=\max_{s\text{ valid}}\sum_\beta w_{t\beta}s_\beta\); coefficients may have either sign. Assume every coefficient profile within the initial bounds gives \(v_t^w(0)=0\).
Set \(C_j=\max_t e_{tj}+\sum_{t,\beta\text{ leaf}}|q_{t\beta j}|\), and let \(F_t\) contain the integer trades with \(0\le e_{tj}+\lambda_j\le C_j\) and at least one valid satisfaction vector. A mass allocation is a finitely supported rational array \(y_{t\lambda}\ge0\), with \(\sum_{\lambda\in F_t}y_{t\lambda}=\mu_t\) and \(\sum_{t,\lambda}y_{t\lambda}\lambda_j=0\). Define \(W_w(y)=\sum_{t,\lambda}y_{t\lambda}v_t^w(\lambda)\) and \(\operatorname{OPT}_w=\max_{y\text{ feasible}}W_w(y)\); individual trades and tree satisfactions remain integral, while type masses may split.
Fix rational \(\Delta^\star\in(0,1]\), \(\delta>0\), and \(\epsilon>0\), with round tolerances \(\epsilon_r=\epsilon 2^{-r}\). All members of a type share one bound refinement in each round; refinements increase lower bounds and decrease upper bounds while retaining the true coefficients. At current bounds, choose a lower-bound welfare maximizer \(y^\ell\), and define \(\rho=\inf_{w\text{ within bounds}}W_w(y^\ell)/\operatorname{OPT}_w\), assigning ratio \(1\) when \(\operatorname{OPT}_w=0\). If \(\rho\ge\Delta^\star\), or upper-bound optimal welfare is zero, perform one final round without further refinement and return \(y^\ell\).
Otherwise set \(\alpha=\max\{1/2,\rho\}\), interpolate node coefficients as \(a^\alpha=\alpha\ell+(1-\alpha)u\), and choose a feasible provisional allocation maximizing \(W_{a^\alpha}\). Common prices \(\pi\in\mathbb Q_{\ge0}^m\) lexicographically minimize the decreasingly sorted pricing errors \(\max_{b\in F_t}[v_t^{a^\alpha}(b)-\pi\cdot b-v_t^{a^\alpha}(a)+\pi\cdot a]\) over supported provisional pairs \((t,a)\); ties next minimize sorted absolute provisional payments \(|\pi\cdot a|\), then sorted item-price differences \(|\pi_j-\pi_k|\). The provisional payment rule is zero payments; remaining allocation and price ties are unrestricted.
Write \(\theta_{t,w}(b,a)=v_t^w(b)-\pi\cdot b-v_t^w(a)+\pi\cdot a\). For each supported provisional pair \((t,a)\), the shared updated bounds satisfy \(\delta\)-MRPAR if either \(\theta_{t,w}(a,b)\ge-\delta\) for every consistent \(w\) and every \(b\in F_t\), or there exists \(c\in F_t\) with \(\theta_{t,w}(c,b)\ge0\) for all such \(w,b\) and \(\theta_{t,w}(c,a)>\delta\) for every consistent \(w\).
For each such pair, define \(E^i(b)=\max_{w\text{ within bounds }i}\theta_{t,w}(b,a)\) and \(d^i(b)=\min_{w\text{ within bounds }i}\theta_{t,w}(b,a)\), where \(i=0,1\) denotes bounds before and after the round. Order \(F_t\) by decreasing \(E^0\), breaking ties lexicographically. The shared refinement satisfies \(\epsilon_r\)-DIAR if it reduces \(E^0(b)-E^1(b)\) by at least \(\epsilon_r\) for some trade \(b\) and establishes \(E^0(c)-d^1(c)<\epsilon_r\) for every earlier trade \(c\), or establishes this inequality for every trade. A synchronized transcript records these allocations, prices, and shared refinements; it must satisfy both activity rules for every supported provisional pair.
Does this mass process retain the termination and welfare guarantee \(W_v(y)\ge\Delta^\star\operatorname{OPT}_v\) as \(\epsilon_r\to0\)? Is constructing a terminating transcript with this approximation guarantee polynomial-time or NP-hard, and how does its complexity depend on \(m,\tau,B,L,\Delta^\star,\delta,\epsilon\)?
For finite agents, ICE with both activity rules and truthful bound refinements is proved to attain its target welfare approximation as the DIAR tolerance tends to zero; this is not a polynomial-time guarantee. Discrete winner determination is NP-hard. [Lubin et al.](https://people.bu.edu/blubin/papers/md/ICE2008JAIR.pdf)
No result for exactly this mass allocation and synchronized transcript model was identified in the literature search.
For the stated geometric schedule, unconditional termination is false. However, every terminating execution has the requested welfare guarantee, and a terminating transcript always exists.
Constructing such a transcript is NP-hard, even with \(m=2\), \(\tau=2\), equal masses, and completely known coefficients. Conversely, a transcript can be constructed in time \(2^{\operatorname{poly}(B)}\operatorname{poly}(m,L)\). Thus bounded tree size yields polynomial-time construction; bounded numbers of goods and supported types do not.
I interpret the activity rules as applying to the provisional pairs in refinement rounds—the “otherwise” branch. The stipulated final round returns the lower-bound allocation without another refinement.
Write \(v_t=v_t^{a_t}\) for the true valuation.
Coefficient monotonicity. If \(w_t\le w'_t\) componentwise, then \(v_t^{w_t}(\lambda)\le v_t^{w'_t}(\lambda)\). Indeed, every satisfaction vector has nonnegative coordinates, so \(w_t\cdot s\le w'_t\cdot s\); taking maxima preserves this inequality. This argument permits coefficients of either sign.
Each \(F_t\) is finite because its integer trades lie in a bounded box. The mass-allocation constraints therefore define a bounded rational polytope. It is nonempty: assigning each type its entire mass at trade \(0\) is feasible. By the normalization assumption, this allocation has welfare \(0\) under every consistent profile. Consequently, \(\operatorname{OPT}_w\ge0\).
For every coefficient profile, a welfare maximizer exists at a vertex of this polytope. Although profiles used in the definition of \(\rho\) may be real, the vertices are rational because the allocation constraints are rational.
A vertex has at most \(\tau+m\) positive entries. To see this, the equality-constraint matrix has rank at most \(\tau+m\). If the columns belonging to positive entries were dependent, a sufficiently small perturbation in both directions along that dependence would preserve feasibility, contradicting extremality.
Now consider a terminating round. Since the true coefficients remain within the bounds,
\(W_v(y^\ell)\ge W_\ell(y^\ell)=\operatorname{OPT}_\ell\ge0.\)
If termination occurs because \(\rho\ge\Delta^\star\), then, when \(\operatorname{OPT}_v>0\), the true profile is among those defining the infimum, and hence
\(\displaystyle \frac{W_v(y^\ell)}{\operatorname{OPT}_v}\ge\rho\ge\Delta^\star.\)
If \(\operatorname{OPT}_v=0\), nonnegativity already proves the desired inequality.
Alternatively, if \(\operatorname{OPT}_u=0\), monotonicity gives
\(0\le\operatorname{OPT}_v\le\operatorname{OPT}_u=0.\)
Thus every terminal output satisfies \(W_v(y^\ell)\ge\Delta^\star\operatorname{OPT}_v\). This conclusion does not require either activity rule.
The activity rules do not force termination under the specified schedule.
Take one good and two types, each of mass \(1/2\).
| Type | Endowment | Tree | True coefficient | Initial bounds |
|---|---:|---|---:|---|
| Buyer | \(0\) | One leaf with quantity \(+1\) | \(2\) | \([1/2,3]\) |
| Seller | \(1\) | One leaf with quantity \(-1\) | \(-1\) | \([-1,-1]\) |
Set \(\delta=1\) and \(\epsilon=1/8\). Let \(\Delta^\star\) be any number in the stipulated interval \((0,1]\).
Here \(C=3\), so
\(F_{\mathrm{buyer}}=\{0,1,2,3\},\qquad F_{\mathrm{seller}}=\{-1,0,1,2\}.\)
For a buyer coefficient \(w\in[1/2,3]\),
\(v_{\mathrm{buyer}}^w(0)=0,\qquad v_{\mathrm{buyer}}^w(b)=w\ \text{for }b\ge1.\)
For the seller,
\(v_{\mathrm{seller}}(-1)=-1,\qquad v_{\mathrm{seller}}(b)=0\ \text{for }b\ge0.\)
These valuations satisfy the required normalization throughout the initial bounds.
Number refinement rounds by \(r=1,2,\ldots\). In round \(r\), increase only the buyer’s lower bound by \(\epsilon_r\). If \(l_r\) is that lower bound after round \(r\), then
\(\displaystyle l_r=\frac12+\sum_{k=1}^r\frac18\,2^{-k} =\frac12+\frac18(1-2^{-r})<\frac58<1.\)
The upper bound remains \(3\). All refinements retain the true coefficient \(2\).
At any lower coefficient \(l<1\), the unique lower-bound welfare maximizer is no trade.
Indeed, let \(x\) be the buyer mass receiving a positive trade, and let \(z\) be the seller mass receiving trade \(-1\). Every positive buyer trade consumes at least one unit, so market clearing implies \(z\ge x\). Lower-bound welfare is
\(lx-z\le(l-1)x.\)
It is strictly negative if \(x>0\); if \(x=0\), any selling also gives negative welfare. With neither buying nor selling, clearing forces all trades to be \(0\).
Thus \(y^\ell\) is always the no-trade allocation. Its welfare is zero under every consistent profile. At the true profile, however,
\(\operatorname{OPT}_v=\frac12(2-1)=\frac12.\)
Therefore \(\rho=0\) in every round. Upper-bound optimal welfare is \(\frac12(3-1)=1\), so neither stopping condition applies.
Since \(\rho=0\), interpolation uses \(\alpha=1/2\). The buyer’s interpolated coefficient is
\(A=(l+3)/2>1.\)
The unique provisional optimum gives every buyer trade \(1\) and every seller trade \(-1\). The same calculation above bounds provisional welfare by \((A-1)x\le(A-1)/2\), with equality requiring precisely these trades.
At a nonnegative price \(p\), the pricing errors for these two supported pairs are
\(\operatorname{err}_{\mathrm{buyer}}(p)=\max\{0,p-A\},\qquad \operatorname{err}_{\mathrm{seller}}(p)=\max\{0,1-p\}.\)
Both errors are zero exactly when \(1\le p\le A\). The two absolute provisional payments are both \(p\), so the prescribed next tie-break selects \(p=1\). There are no item-price differences with one good.
For the buyer’s provisional trade \(a=1\), at price \(1\),
\(\theta_w(1,0)=w-1\ge-1/2>-1,\)
and, for \(b\ge1\),
\(\theta_w(1,b)=b-1\ge0.\)
Thus the buyer satisfies the first alternative of \(\delta\)-MRPAR throughout the updated bounds. The seller’s provisional trade is an exact demand maximizer, so the seller satisfies that alternative as well.
For buyer DIAR, before refinement,
\(E^0(0)=1-l,\quad E^0(1)=0,\quad E^0(2)=-1,\quad E^0(3)=-2.\)
Consequently, trade \(0\) is first in the required ordering. Increasing \(l\) by \(\epsilon_r\) gives
\(E^0(0)-E^1(0)=\epsilon_r.\)
There are no earlier trades to check. Buyer DIAR therefore holds.
The seller’s bounds are already exact and remain unchanged. For every seller trade \(b\),
\(E^0(b)-d^1(b)=0<\epsilon_r,\)
so seller DIAR also holds.
This produces an infinite synchronized execution satisfying both activity rules and truthful refinements, while \(\epsilon_r\to0\) and \(\rho\) remains zero. Moreover, its lower-bound allocations always have true welfare zero.
The obstruction is the summability of the required improvements. The finite-agent limiting result quoted in the question does not, by itself, justify termination under this particular schedule. [Lubin et al., Theorem 6](https://people.bu.edu/blubin/papers/md/ICE2008JAIR.pdf)
Claim. Full revelation in the first refinement round satisfies both activity rules simultaneously for every supported provisional pair.
Choose the prescribed provisional allocation and prices, and refine every coefficient interval to its true singleton value. Fix any supported pair \((t,a)\).
For MRPAR, define
\(G_t(b)=v_t(b)-\pi\cdot b,\qquad M_t=\max_{b\in F_t}G_t(b).\)
The maximum exists because \(F_t\) is finite.
If \(M_t-G_t(a)\le\delta\), then for every \(b\),
\(\theta_{t,v}(a,b)=G_t(a)-G_t(b)\ge-\delta.\)
Otherwise choose a maximizer \(c\). Then
\(\theta_{t,v}(c,b)\ge0\ \text{for every }b,\qquad \theta_{t,v}(c,a)>\delta.\)
Because the updated coefficient profile is a singleton, these inequalities hold for every consistent profile, as required.
For DIAR, full revelation gives
\(E^1(b)=d^1(b)=\theta_{t,v}(b,a).\)
Define \(g(b)=E^0(b)-\theta_{t,v}(b,a)\). Since the true profile was consistent before refinement, \(g(b)\ge0\).
If every \(g(b)<\epsilon_r\), DIAR’s last alternative holds. Otherwise choose the first trade in the prescribed ordering for which \(g(b)\ge\epsilon_r\). For this trade,
\(E^0(b)-E^1(b)=g(b)\ge\epsilon_r,\)
while every earlier trade \(c\) satisfies
\(E^0(c)-d^1(c)=g(c)<\epsilon_r.\)
This proves DIAR. The argument applies separately to every supported pair while using the same full revelation for its type.
After full revelation, the next lower-bound optimization is true welfare optimization and \(\rho=1\). The process therefore terminates.
Accordingly, a terminating transcript needs at most one refinement round followed by the final round. This existence result holds for every positive \(\delta,\epsilon\), including \(\Delta^\star=1\).
The prescribed price minimizers also exist rationally. Their pricing errors are finite maxima of rational affine functions of \(\pi\), and subsequent criteria are absolute values of rational linear functions. Sequential minimization of sums of the largest components implements each sorted lexicographic objective through rational linear programs. Each minimization is feasible and bounded below, so it attains a rational optimum.
The hardness persists after allowing masses to split. In fact, computing any feasible positive-factor welfare approximation is already NP-hard.
Reduce from SUBSET SUM: given positive binary integers \(x_1,\ldots,x_n\) and \(P\ge1\), decide whether some subset sums to \(P\). This is a standard NP-hard problem. [Polak, Rohwedder, and Węgrzycki](https://arxiv.org/abs/2105.04035)
Set
\(\displaystyle V=\max\left\{\sum_{i\in S}x_i:\ S\subseteq\{1,\ldots,n\},\ \sum_{i\in S}x_i\le P\right\},\qquad H=P-\frac12.\)
Thus a yes-instance has \(V=P>H\), while a no-instance has \(V\le P-1<H\).
There are two goods and two types of mass \(1/2\). All coefficient bounds are exact.
The buyer has endowment \((0,0)\). Its root is an AND node with three children:
The root also has coefficient \(0\). Activating it requires both mandatory leaves and permits an arbitrary subset of the item leaves.
The seller has endowment \((0,1)\) and a single leaf of quantity \(-1\) of good \(2\), coefficient \(-H\).
The construction has \(m=2\), \(\tau=2\), and \(B=n+5\), and its binary length is polynomial in the SUBSET SUM input length.
At trade \(0\), the buyer cannot activate its root because that would require one unit of good \(2\). Its value is therefore zero. The seller can leave its negative-coefficient leaf unsatisfied, also obtaining value zero. Hence the normalization promise holds.
Every type has zero endowment of good \(1\). Therefore every feasible individual trade has first coordinate nonnegative. Market clearing forces that coordinate to be zero at every supported pair.
For the buyer, at first coordinate zero,
\(v_{\mathrm{buyer}}(0,0)=0,\qquad v_{\mathrm{buyer}}(0,b)=V\ \text{for every feasible integer }b\ge1.\)
Indeed, root activation imposes exactly the constraint \(\sum_{i\in S}x_i\le P\), and its value is that subset sum.
For the seller,
\(v_{\mathrm{seller}}(0,-1)=-H,\qquad v_{\mathrm{seller}}(0,b)=0\ \text{for }b\ge0.\)
Let \(z_b\) be the buyer mass receiving at least one unit of good \(2\), and \(z_s\) the seller mass receiving trade \((0,-1)\). Integrality and clearing imply
\(0\le z_b\le z_s\le1/2.\)
Consequently,
\(W_v(y)=Vz_b-Hz_s\le(V-H)z_b.\)
If the SUBSET SUM instance is a yes-instance, fully trading one unit between the two types gives welfare
\(\operatorname{OPT}_v=\frac12(V-H)=\frac14.\)
The upper bound follows from \(z_b\le1/2\).
If it is a no-instance, every allocation with \(z_b>0\) has strictly negative welfare. An allocation with \(z_b=0\) and \(z_s>0\) also has strictly negative welfare. The no-trade allocation gives zero, so \(\operatorname{OPT}_v=0\).
Suppose an algorithm returns a feasible allocation satisfying the requested guarantee for any fixed \(\Delta^\star>0\).
In a yes-instance, its welfare must be at least \(\Delta^\star/4>0\), so \(z_b>0\). In a no-instance, its welfare must be nonnegative, forcing \(z_b=0\).
Inspecting whether the returned allocation gives positive buyer mass a positive second-coordinate trade therefore decides SUBSET SUM.
This proves NP-hardness of approximation construction, and hence of terminating-transcript construction. It holds for every fixed positive \(\Delta^\star\), with fixed positive \(\delta,\epsilon\). Because all bounds are exact, the transcript must terminate immediately after its required initial welfare optimization.
This is a search-hardness result; it does not assert NP-completeness of transcript verification.
A constructor can run in time \(2^{\operatorname{poly}(B)}\operatorname{poly}(m,L)\). The proof avoids enumeration of every integer in the trade boxes.
Call a good active if some leaf quantity for it is nonzero. Let \(d\) be the number of active goods. Since each leaf refers to one good,
\(d\le\min\{m,B\}.\)
For an inactive good, every satisfaction vector has total quantity zero, so every feasible trade has nonnegative quantity of that good. Clearing therefore forces its quantity to be zero at every supported allocation pair.
For demand calculations at nonnegative prices, setting inactive coordinates to zero preserves feasibility and valuation and weakly improves payoff. Thus welfare and pricing-error optimization can restrict those coordinates to zero.
Enumerate all satisfaction vectors satisfying the tree constraints. There are at most \(2^{B_t}\) for type \(t\). Write
\(Q_{tsj}=\sum_{\beta\text{ leaf}}q_{t\beta j}s_\beta.\)
For each active coordinate, partition its integer trade interval at the thresholds \(Q_{tsj}\). Each coordinate has at most \(2^{B_t}+1\) resulting integer intervals. On every product rectangle, the set of valid satisfaction vectors is constant. Hence its valuation is constant across trades in that rectangle, simultaneously for every coefficient profile.
Discard rectangles with no valid satisfaction vector and retain their integer corners. Call the resulting set \(D_t\). Its size satisfies
\(|D_t|\le2^d(2^{B_t}+1)^d.\)
Every integer trade in a retained rectangle is a rational convex combination of its corners. Replacing its mass by that combination preserves mass, average trade, and welfare under every coefficient profile. Therefore restriction to \(D_t\) preserves all welfare optima.
Likewise, on a rectangle, valuation minus a linear payment is maximized at a corner. Thus pricing errors can be computed using \(D_t\).
The total representative-set size is
\(N=\sum_t|D_t|\le\tau\,2^d(2^B+1)^d=2^{O(B^2)},\)
using \(\tau\le B\).
The allocation LP on these representatives has at most \(\tau+d\le2B\) equality constraints. Its vertices can therefore be enumerated by supports of size at most \(2B\), giving at most
\(N^{O(B)}=2^{O(B^3)}\)
candidates. Their rational coordinates have polynomial binary length by the usual determinant bounds.
It remains to compute \(\rho\) exactly, so that the constructor follows the prescribed stopping and interpolation rules.
Partition the coefficient box using all hyperplanes on which two satisfaction-vector scores are equal. There are at most \(\tau\,2^{2B}\) such hyperplanes. Within each cell, every representative trade’s valuation is affine in the coefficient profile.
Consequently, every allocation vertex’s welfare is affine there. Further partition by equalities between those vertex-welfare functions. On each resulting closed cell \(P\),
\(N_P(w)=W_w(y^\ell),\qquad D_P(w)=\operatorname{OPT}_w\)
are affine. Moreover,
\(0\le N_P(w)\le D_P(w)\)
throughout the cell: the first inequality follows from coefficient monotonicity and lower-bound optimality, and the second from feasibility of \(y^\ell\).
Let the vertices of \(P\) be \(z_i\), and express \(w=\sum_i\eta_i z_i\). If \(D_P(w)>0\), then
\(\displaystyle \frac{N_P(w)}{D_P(w)} = \sum_{i:D_P(z_i)>0} \frac{\eta_iD_P(z_i)}{D_P(w)} \frac{N_P(z_i)}{D_P(z_i)}. \)
Vertices with zero denominator also have zero numerator and contribute nothing. The displayed expression is a convex combination. Therefore the minimum ratio on this cell is attained at a vertex with positive denominator, unless the denominator vanishes throughout, in which case every assigned ratio is \(1\).
Thus \(\rho\) is rational and can be computed by examining these rational vertices.
The number of hyperplanes in the second partition is \(2^{O(B^3)}\). A hyperplane arrangement in dimension at most \(B\) has \(H^{O(B)}\) cells and faces. Enumerating these arrangements and their vertices therefore takes \(2^{\operatorname{poly}(B)}\) operations, each with polynomial-size rational arithmetic.
For finitely many representatives, each pricing error is a maximum of rational affine functions of \(\pi\). For any list \(f_1,\ldots,f_k\), the sum of its largest \(h\) entries has the representation
\(\displaystyle \sum_{\text{largest }h}f_i = \min_z\left(hz+\sum_i\max\{f_i-z,0\}\right). \)
This gives a linear-programming formulation when the \(f_i\) are maxima of affine functions. Sequentially minimizing these partial sums implements sorted lexicographic minimization. Apply the same construction next to absolute payments and then to absolute item-price differences.
These are rational LPs of size polynomial in \(N,m,L\), and rational LPs can be solved in polynomial time. [MIT notes on linear-programming algorithms](https://courses.csail.mit.edu/6.854/21/Notes/n14-LP_algorithms.html)
The constructor now:
Sections 1 and 3 prove correctness. The total running time is \(2^{\operatorname{poly}(B)}\operatorname{poly}(m,L)\).
The established distinctions are:
| Parameter regime | Proven result |
|---|---|
| Arbitrary legal refinements with the stated schedule | Termination can fail |
| Constructor chooses refinements | At most one refinement round is necessary |
| Fixed \(m=2\) and \(\tau=2\) | Construction remains NP-hard |
| Fixed \(B\) | Construction is polynomial-time |
| General \(B\) | Construction admits time \(2^{\operatorname{poly}(B)}\operatorname{poly}(m,L)\) |
| Any fixed \(\Delta^\star>0\) | NP-hardness persists |
| Any positive \(\delta,\epsilon\) | Full revelation works; no inverse-tolerance round bound is needed |
Binary masses are used directly in the LP; no expansion into a finite population is required. Optimal allocations can be chosen with at most \(\tau+d\) supported pairs and polynomial-size rational masses.
For computational statements, binary encodings of rational control parameters can be included in \(L\). The full-revelation constructor requires no arithmetic involving \(\delta\) or \(\epsilon\); its refinement is valid for all their positive values.
⟨structured verdict parsed — rendered above⟩
Verdict: the prover resolves the task correctly. The nontermination counterexample, guarantee at termination, full-revelation construction, hardness reduction, and parameterized upper bound are sound. I found no issue requiring repair.
The interpretation that activity rules apply to refinement rounds is consistent with the task: provisional pairs are defined in the “otherwise” branch, while the final round explicitly requires no further refinement.
The coefficient-monotonicity argument is correct. Satisfaction vectors have nonnegative coordinates, so increasing any coefficient cannot decrease any satisfaction score or its maximum. Negative coefficients do not invalidate this argument.
Each \(F_t\) is finite because its coordinates are integers in bounded intervals. Trade \(0\) belongs to \(F_t\): the all-zero satisfaction vector satisfies both the tree and quantity constraints, and the endowment lies within the specified box. Thus the no-trade allocation is feasible.
The normalization assumption makes its welfare zero under every consistent coefficient profile. Consequently, \(\operatorname{OPT}_w\ge0\).
The vertex arguments are valid. The allocation constraints have rational coefficients, so vertices are rational even when the welfare objective comes from real coefficients. The support bound follows from the rank bound and the stated two-sided perturbation argument.
At termination, monotonicity gives
\(W_v(y^\ell)\ge\operatorname{OPT}_\ell\ge0\).
If termination uses \(\rho\ge\Delta^\star\), the true coefficient profile is included in the defining infimum. This proves the requested inequality when \(\operatorname{OPT}_v>0\); the zero-optimum case follows separately from nonnegativity.
If termination instead uses \(\operatorname{OPT}_u=0\), monotonicity and nonnegativity imply \(\operatorname{OPT}_v=0\). This branch is also handled correctly.
Finding: every terminal output has the stated welfare guarantee, independently of the activity rules.
The proposed society satisfies the input assumptions. Its bound is \(C=3\), and the two feasible trade sets are exactly those listed.
For the buyer, negative trades violate the endowment restriction; at trade \(0\), only the unsatisfied leaf is valid. At positive trades, its positive coefficient makes satisfaction optimal.
For the seller, trade \(-1\) forces leaf satisfaction and therefore value \(-1\). At nonnegative trades, leaving the negative-coefficient leaf unsatisfied gives value zero.
Normalization holds throughout the coefficient bounds.
The geometric sum is correct:
\(l_r=\frac12+\frac18(1-2^{-r})<\frac58<1\).
The refinement retains the true coefficient and respects bound monotonicity.
The lower-bound optimization argument correctly accounts for all feasible trades, including trades larger than one. Clearing implies \(z\ge x\), and welfare satisfies
\(lx-z\le(l-1)x\).
If \(x>0\), welfare is negative. If \(x=0\), any selling is also detrimental. Without buying or selling, all remaining trades are nonnegative, so clearing forces no trade.
Thus the lower-bound optimum is uniquely no trade. Its welfare is zero under every consistent profile, while the true optimum is positive. Therefore \(\rho=0\). The upper-bound optimum is also positive, so neither stopping condition applies.
The interpolation coefficient satisfies \(A=(l+3)/2>1\). The welfare bound establishes that the provisional optimum uses all buyer and seller mass, with trades \(1\) and \(-1\), respectively.
Both pricing-error formulas are correct for every nonnegative price, after checking all trades in the stated feasible sets. Their simultaneous zero-error region is \(1\le p\le A\).
On this region, both absolute provisional payments equal \(p\). The next prescribed tie-break therefore selects \(p=1\). No remaining item-price criterion changes that conclusion.
For buyer MRPAR, the signs of \(\theta_w(1,b)\) are correct. The comparison with trade \(0\) is uniformly greater than \(-\delta\), and comparisons with all positive trades are nonnegative.
The seller’s trade is an exact demand maximizer at price one, so its MRPAR verification is valid.
The buyer’s four \(E^0\) values are correct. Trade \(0\) is strictly first in the ordering, and its error decreases by exactly \(\epsilon_r\). Hence the first DIAR alternative applies without any earlier-trade condition.
For the seller, singleton bounds make \(E^0(b)=d^1(b)\) for every trade. The strict inequality required by the last DIAR alternative holds because \(\epsilon_r>0\).
Finding: this is a legal infinite synchronized execution. It disproves unconditional termination and also disproves convergence of the lower-bound allocations to the requested positive welfare factor under this schedule.
The prover appropriately avoids treating the finite-agent theorem as a theorem about the specified geometric schedule. The cited [ICE Theorem 6](https://people.bu.edu/blubin/papers/md/ICE2008JAIR.pdf) does not supply the missing guarantee for this explicitly verified execution.
The full-revelation argument checks both activity rules separately for every supported provisional pair while using one shared refinement.
For MRPAR, the two cases exhaust all possibilities because the finite demand maximum exists:
After revelation, the consistent profile is a singleton, so the universal quantifiers over consistent coefficients are satisfied.
For DIAR, \(g(b)\ge0\) follows because the true profile was previously consistent. If all gaps are strictly below tolerance, the last alternative holds. Otherwise, selecting the first trade with gap at least tolerance establishes both the required reduction and the strict inequalities for all earlier trades. Equality with the tolerance is correctly included in the reduction branch.
After revelation, the lower-bound optimization is true optimization. The robustness ratio is one, including the zero-optimum convention.
The price-existence claim is also valid: the objectives admit rational LP formulations, and successive optimization retains a nonempty rational polyhedron with attained finite optimum.
Finding: a terminating transcript exists with at most one refinement round and one final round. The proof covers every permitted target and every positive activity-rule tolerance.
The reduction is polynomial in the binary SUBSET SUM input length. It uses two goods, two equal-mass types, exact coefficient bounds, and \(B=n+5\) nodes. The node count is correct.
The starting hardness premise is standard and is supported by the cited [SUBSET SUM reference](https://arxiv.org/abs/2105.04035).
The buyer’s AND root forces both mandatory leaves and the subset-selection node when activated. When the root is inactive, its child constraints force the subtree inactive. Thus item values cannot be obtained without consuming good two.
At zero trade, root activation is infeasible because of that mandatory positive quantity. The seller can leave its negative-coefficient leaf inactive. Both normalization claims hold.
Every individual first-coordinate trade is nonnegative because both types have zero endowment of good one. Positive masses and clearing therefore force this coordinate to be zero at every supported pair.
At first coordinate zero, the buyer’s quantity constraint is precisely the subset capacity constraint. Its stated valuation formulas follow.
For good two, clearing and integral individual trades imply
\(0\le z_b\le z_s\le\frac12\).
The welfare expression and upper bound are correct.
In a yes-instance, \(V=P\), and full unit trading attains welfare \(\frac14\); the established bound proves optimality.
In a no-instance, \(V\le P-1<H\). Every allocation with positive buyer trading mass has negative welfare, and positive seller trading mass alone is also detrimental. Therefore the optimum is zero.
A positive-factor approximation has positive welfare in a yes-instance, forcing \(z_b>0\). In a no-instance, the guarantee requires nonnegative welfare, forcing \(z_b=0\).
The returned explicit allocation therefore decides SUBSET SUM by inspection of its support. This decoding does not require computing the buyer’s valuation.
Finding: the search-hardness conclusion is valid for every fixed positive approximation factor. Allowing masses to split does not defeat the reduction. Exact bounds also make the initial welfare optimization sufficient for immediate termination.
The prover correctly limits the conclusion to NP-hardness; it does not claim NP-completeness or strong NP-hardness.
The inactive-good argument is valid. Such coordinates must be nonnegative in every feasible trade, so clearing forces them to zero in supported allocations. Setting them to zero also weakly improves demand payoff at nonnegative prices.
For active goods, feasibility of a satisfaction vector depends only on whether each trade coordinate exceeds its quantity threshold. Thus the partition has a constant feasible-satisfaction set on each rectangle, independently of coefficients.
Retained integer corners remain feasible. Convex replacement preserves type mass and average trade, and constant rectangle valuations preserve welfare under every profile. Maximization of valuation minus linear payment also reduces to corners.
The bounds on \(d\), \(|D_t|\), and \(N\) follow as stated. Large binary quantity magnitudes do not require enumerating every integer trade.
The reduced allocation LP has at most \(2B\) equality constraints. Support enumeration gives the stated exponential candidate bound. Rational coordinate lengths follow from determinant bounds on its rational constraint matrix.
The coefficient partition makes every representative valuation affine. Further comparison of allocation-vertex welfare functions makes the optimal welfare affine on each resulting closed cell.
The crucial inequalities \(0\le N_P\le D_P\) hold. Consequently, a cell vertex with zero denominator also has zero numerator. For a positive denominator, the displayed ratio identity is a convex combination of positive-denominator vertex ratios.
This handles the potentially troublesome zero-optimum boundary correctly. Cells with identically zero denominator contribute the stipulated ratio one.
The arrangement counts and rational coefficient sizes support the claimed \(2^{\operatorname{poly}(B)}\operatorname{poly}(m,L)\) bound.
The largest-components identity is correct. Sequential minimization of the partial sums implements decreasingly sorted lexicographic minimization. The same representation applies to absolute payments and item-price differences.
The resulting problems are rational LPs, so the cited [polynomial-time LP result](https://courses.csail.mit.edu/6.854/21/Notes/n14-LP_algorithms.html) applies to their explicit encoded size.
Finding: the construction bound follows. Fixed total tree size gives polynomial-time construction; fixing only goods and support size does not remove the established hardness. Full revelation requires no inverse-tolerance round bound.
These are parameter-dependent tractability statements, not an encoding-dependent complexity split.
All principal claims are established. The output distinguishes arbitrary legal executions from constructor-chosen refinements, handles zero optimum consistently, and proves hardness for the mass model itself. No additional clarification is needed to make the argument verifiable.
⟨structured verdict parsed — rendered above⟩
Tier: machine-proved, adversarially reviewed by an independent model. No human has checked this proof. Generated from pipeline artifacts by tools/atlas_build.py.