← back to the atlas

d4-conf-wine-2022-0037 (d4-conf-wine-2022-0037)

Answer: Yes. For every pair of distributions specified in the question, \(\mathsf{FB}_\mu\le 3.15\,\mathsf{RandOff}_\mu\).

The anchor (named result in the paper)

Theorem 1.1 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateFor any pair of distributions $F$ and $G$, the inequality $\mathsf{FB}\leq 3.15\cdot\mathsf{RandOff}$ holds.

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

The continuous mirror question, as graded

Given finite rational type distributions \(\mu_B\) over buyer values \(v\) and \(\mu_S\) over seller costs \(c\), with unit mass on each side and independent matching so pair \((v,c)\) has mass \(\mu_B(v)\mu_S(c)\), apply the paper’s random-offerer mechanism to each pair using the marginal distributions. Is aggregate first-best \(\mathsf{FB}_\mu=\sum_{v,c}\mu_B(v)\mu_S(c)(v-c)_+\) always at most \(3.15\) times aggregate random-offerer gains from trade?

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

There is one item, initially held by a seller. Buyer values and seller costs lie in \(\mathbb{Q}\), with independent distributions \(\mu_B\) and \(\mu_S\), each of total mass \(1\).
A society is given by its support: the list of types with positive mass, each with its mass as a binary rational. Let \(\tau\) be the combined support size, not the number of possible types, and \(L\) the total input bit length; here \(m=1\) item. State any running times in \(m,\tau,L\).
For each cost \(c\), choose the smallest maximizer \(p_c\in\arg\max_{p\in\mathbb{R},\,p\ge c}(p-c)\sum_{v\ge p}\mu_B(v)\). For each value \(v\), choose the largest maximizer \(q_v\in\arg\max_{q\in\mathbb{R},\,q\le v}(v-q)\sum_{c\le q}\mu_S(c)\).
The random-offerer mechanism flips a fair coin: the seller offers \(p_c\), accepted iff \(v\ge p_c\), or the buyer offers \(q_v\), accepted iff \(c\le q_v\); the buyer pays the seller the offered price upon trade.
Define \(\mathsf{RandOff}_\mu=\frac12\sum_{v,c}\mu_B(v)\mu_S(c)(v-c)(\mathbf{1}\{v\ge p_c\}+\mathbf{1}\{c\le q_v\})\) and \(\mathsf{FB}_\mu=\sum_{v,c}\mu_B(v)\mu_S(c)\max\{v-c,0\}\).

Does \(\mathsf{FB}_\mu\le 3.15\,\mathsf{RandOff}_\mu\) hold for every such pair of distributions?

Known results: the original anchor is an approximation guarantee for independent distributions with finite first moments, rather than a discrete computational theorem. It already establishes this inequality for the exact distributional setting above, including finite rational supports; consequently this target is settled. [Original source](https://arxiv.org/pdf/2205.00140).

Modeling choices made when packaging the task

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

Answer and theorem used

Yes. The inequality follows from Theorem 1.1 of Yumou Fei’s *Improved Approximation to First-Best Gains-from-Trade*: for independent buyer values and seller costs with finite first moments, the random-offerer mechanism satisfies \(\mathsf{FB}\le 3.15\,\mathsf{RandOff}\). The paper defines offers by maximizing the same expected-payoff objectives used here, with acceptance at equality. [Original source, Sections 1.1–1.2](https://arxiv.org/pdf/2205.00140)

We verify that the specified distributions and price selections satisfy these hypotheses.

Existence and validity of the specified offers

Write \(\mathcal V=\operatorname{supp}(\mu_B)\) and \(\mathcal C=\operatorname{supp}(\mu_S)\). Both sets are finite and nonempty.

Fix a seller cost \(c\). If \(\max\mathcal V\le c\), every feasible seller offer earns zero, and the smallest maximizer is \(p_c=c\).

Otherwise, offering \(\max\mathcal V\) earns strictly positive profit. Any maximizing offer therefore has positive demand and exceeds \(c\). For any such offer \(p\), let \(b\) be the smallest buyer support point satisfying \(b\ge p\). Raising the offer from \(p\) to \(b\) preserves demand and increases profit strictly unless \(p=b\). Thus every maximizer belongs to the finite set \(\{b\in\mathcal V:b>c\}\), so a smallest maximizer exists.

The buyer argument is symmetric. If \(\min\mathcal C\ge v\), every feasible buyer offer earns zero, and the largest maximizer is \(q_v=v\). Otherwise the maximum is positive. For an offer \(q\) with positive acceptance probability, lowering it to the largest seller support point at most \(q\) preserves acceptance probability and increases buyer utility unless it already equals that point. Consequently a largest maximizer exists among \(\{s\in\mathcal C:s<v\}\).

These constrained maximizers also maximize the paper’s unrestricted objectives: a seller price below \(c\), or a buyer price above \(v\), yields nonpositive expected payoff, whereas the constrained maximum is nonnegative.

Moreover, the prescribed tie-breaking favors gains from trade. Among optimal feasible seller prices, the smallest accepts the largest set of buyers; every added trade satisfies \(v\ge p_c\ge c\). Among optimal feasible buyer prices, the largest accepts the largest set of sellers; every added trade satisfies \(c\le q_v\le v\). Hence these selections yield at least as much gains from trade as any other feasible maximizing selections.

Application to the finite distributions

Let \(F\) and \(G\) be the cumulative distribution functions of \(\mu_B\) and \(\mu_S\). Their finite first moments follow from

\(\mathbb E|V|=\sum_{v\in\mathcal V}\mu_B(v)|v|<\infty\), and \(\mathbb E|C|=\sum_{c\in\mathcal C}\mu_S(c)|c|<\infty\).

Independence is an explicit premise. Furthermore,

\(1-F(p^-)=\sum_{v\ge p}\mu_B(v)\), and \(G(q)=\sum_{c\le q}\mu_S(c)\).

Thus the paper’s pricing objectives agree exactly with those in the question. Its first-best expectation equals \(\mathsf{FB}_\mu\), since \((v-c)\mathbf 1\{v\ge c\}=\max\{v-c,0\}\). Its equal mixture of seller-pricing and buyer-pricing gains equals the stated \(\mathsf{RandOff}_\mu\).

All hypotheses are therefore satisfied, giving

\(\boxed{\mathsf{FB}_\mu\le 3.15\,\mathsf{RandOff}_\mu}\).

This includes \(\mathsf{FB}_\mu=0\), because every accepted trade has nonnegative gains. No computational assumption concerning the support encoding is needed.

⟨structured verdict parsed — rendered above⟩

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

Verdict

The output proves the requested inequality. The cited theorem applies to the stated finite rational distributions, and the mechanism definitions agree. No major or minor issues were found.

Step-by-step verification

Theorem 1.1 of the [original paper](https://arxiv.org/pdf/2205.00140) establishes \(\mathsf{FB}\le 3.15\,\mathsf{RandOff}\). Its model assumes independent distributions with finite first moments and allows real-valued types. Its mechanism definitions use acceptance at equality and the same expected-payoff maximization objectives. Consequently, negative rational types and atoms do not invalidate this application.

The task specifies finite support lists whose positive masses sum to one. Thus both support extrema used in the argument exist.

If \(\max\mathcal V\le c\), every feasible offer has zero payoff, and \(c\) is the smallest feasible maximizer. Otherwise, the offer \(\max\mathcal V\) has strictly positive payoff because that support point has positive mass.
The price-rounding argument correctly preserves demand: there is no buyer support point between an offer and the smallest support point above it. Raising the offer to that point strictly increases payoff unless the prices already coincide. This reduces optimization to a nonempty finite candidate set and justifies existence of the smallest maximizer.

If \(\min\mathcal C\ge v\), all feasible offers have zero payoff, and \(v\) is the largest feasible maximizer. Otherwise, offering \(\min\mathcal C\) yields positive payoff. Lowering an offer to the largest seller support point below it preserves acceptance probability and increases utility unless the prices coincide. The finite candidate set therefore supplies the largest maximizer. The strict inequalities defining both candidate sets are appropriate when the optimal payoff is positive.

Prices below the seller’s cost and prices above the buyer’s value yield nonpositive expected payoff. Each constrained optimum is nonnegative. Therefore, a constrained maximizer also maximizes the corresponding unrestricted objective. This reasoning remains valid when the optimal payoff is zero.

Smaller feasible seller prices produce nested, larger buyer acceptance sets; larger feasible buyer prices produce nested, larger seller acceptance sets. Every additional accepted trade has nonnegative gains because the offers obey their feasibility constraints. Thus the stated tie-breaking cannot reduce gains from trade relative to another feasible maximizing selection.

Finite supports imply finite absolute first moments. Independence is explicitly assumed. The identities
\[ 1-F(p^-)=\sum_{v\ge p}\mu_B(v),\qquad G(q)=\sum_{c\le q}\mu_S(c) \]
correctly retain probability mass at the offered price. The first-best identity and the equal mixture of the two pricing mechanisms therefore match the task’s finite sums exactly.

Applying the cited theorem gives the requested inequality. If \(\mathsf{FB}_\mu=0\), nonnegative gains on accepted trades also suffice for the inequality. No division by first-best gains occurs.

Scope and feedback

The output settles the universal approximation guarantee. It makes no algorithmic running-time claim, so the task’s requirement to express any running times in \(m,\tau,L\) is not triggered. This establishes an approximation result, rather than a complexity classification.

No additional clarification or repair is needed.

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