← back to the atlas

d4-journals-geb-2021-0118 (d4-journals-geb-2021-0118)

Answer: Attainable: an exact seller-information-only lottery with at most \(\tau_s\) prices guarantees \((1-1/e)W^*\) for every buyer distribution and can be constructed in \(O(\tau_s\log(\tau_s+1)L^2)\) bit operations.

The anchor (named result in the paper)

Theorem 4.1 — class: algorithmic

The continuous mirror question, as graded

Given unit-mass seller and buyer populations with value distributions \(\mu_s\) and \(\mu_b\), paired according to \(\mu_s \otimes \mu_b\), find a price lottery \(\pi\) that depends only on \(\mu_s\) and satisfies \(\mathbb{E}_{p \sim \pi}[W(p;\mu_s,\mu_b)] \geq (1-1/e)W^*(\mu_s,\mu_b)\) for every \(\mu_b\). Here \(W\) is aggregate welfare when a pair trades exactly when \(s \leq p \leq b\), and \(W^*\) is aggregate first-best welfare.

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

Seller and buyer populations each have mass \(1\), with nonnegative rational values and independent pairing measure \(\mu_s\otimes\mu_b\). A society is given by its support: the list of its \(\tau\) types with positive mass, each mass a binary rational; \(\tau\) denotes support size, not the number of possible types. Each population's masses sum to \(1\).
Each seller initially owns one indivisible item. A posted price \(p\geq0\) induces trade exactly when \(s\leq p\leq b\); the buyer pays the seller \(p\), and otherwise the seller keeps the item with no payment.
Define \(W(p;\mu_s,\mu_b)=\int[s+(b-s)\mathbf{1}_{\{s\leq p\leq b\}}]\,d(\mu_s\otimes\mu_b)\) and \(W^*(\mu_s,\mu_b)=\int\max\{s,b\}\,d(\mu_s\otimes\mu_b)\).
A price lottery is chosen using only \(\mu_s\), independently of realized values; its probabilities may be real and specified exactly by finite mathematical expressions. State running times in the seller support size \(\tau_s\) and its input bit length \(L\); here the number of goods is \(m=1\).

Can one construct, for every \(\mu_s\), a price lottery \(\pi(\mu_s)\) satisfying \(\mathbb{E}_{p\sim\pi(\mu_s)}[W(p;\mu_s,\mu_b)]\geq(1-1/e)W^*(\mu_s,\mu_b)\) for every \(\mu_b\), or is this approximation unattainable?

Known results: Blumrosen–Dobzinski establish the seller-information-only \(1-1/e\) guarantee for independent bilateral trade, explicitly allowing arbitrary value distributions, including finite supports. [Original result](https://blumrosen.weebly.com/uploads/4/7/4/7/47472385/partnership.pdf)
The mass formulation above has exactly the same welfare integrals and information restriction, so that result already settles its approximation question.

Modeling choices made when packaging the task

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

Conclusion

The approximation is attainable. For every seller distribution, one can construct a lottery with at most \(\tau_s\) prices, using only seller information, that guarantees \((1-1/e)W^*\) for every buyer distribution.

This is the Random-Quantile mechanism of Blumrosen–Dobzinski, whose Theorem 4.1 establishes the guarantee. Their model explicitly allows arbitrary distributions. Below is an exact finite-support implementation and a direct proof that handles atoms and ties. [Original paper, Sections 2 and 4](https://blumrosen.weebly.com/uploads/4/7/4/7/47472385/partnership.pdf).

Exact construction

Write the seller distribution as \(\mu_s=\sum_{i=1}^{n}a_i\delta_{s_i}\), where \(n=\tau_s\), \(0\leq s_1<\cdots<s_n\), \(a_i>0\), and \(\sum_i a_i=1\). Define cumulative masses \(C_0=0\) and \(C_i=\sum_{j=1}^{i}a_j\).

Post price \(s_i\) with probability

\(\displaystyle w_i=\ln\!\bigl(\max\{1,eC_i\}\bigr)-\ln\!\bigl(\max\{1,eC_{i-1}\}\bigr).\)

These are permitted exact finite mathematical expressions. Each probability is nonnegative because the cumulative masses increase, and telescoping gives

\(\displaystyle \sum_{i=1}^{n}w_i=\ln(e)-\ln(1)=1.\)

Thus they specify a price lottery depending only on \(\mu_s\).

For the proof, an equivalent description is useful. Set \(c=1/e\), draw \(X\) with density \(1/x\) on \([c,1]\), and post

\(\displaystyle q(X),\qquad q(x)=\min\{s_i:C_i\geq x\}.\)

The density integrates to \(\ln(1/c)=1\). Except at endpoints of probability zero, \(q(x)=s_i\) precisely when \(C_{i-1}<x\leq C_i\). Consequently, integrating the density over these intervals gives exactly the probabilities \(w_i\) above.

Proof of the welfare guarantee

Fix any buyer value \(b\geq0\). Let \(S\) have distribution \(\mu_s\), independently of \(X\), and define

\(\displaystyle y=\Pr(S\leq b),\qquad T=\mathbb E[S\mathbf1_{\{S>b\}}].\)

The optimal expected welfare for this fixed buyer value is

\(\displaystyle O_b=\mathbb E[\max\{S,b\}]=by+T.\)

Moreover, because \(S>b\) on the event defining \(T\),

\(\displaystyle T\geq b\Pr(S>b)=b(1-y).\)

Let \(A_b\) denote the expected welfare of the constructed lottery for this buyer value.

For every posted price, sellers with \(S>b\) cannot trade: the conditions \(S\leq p\leq b\) would contradict \(S>b\). They therefore contribute exactly \(T\) to expected welfare. All remaining welfare contributions are nonnegative.

Now consider a quantile \(x\in[c,y]\), if this interval is nonempty. Since \(x\leq\Pr(S\leq b)\), the generalized quantile satisfies \(q(x)\leq b\). Also,

\(\displaystyle \Pr(S\leq q(x))\geq x.\)

Every seller satisfying \(S\leq q(x)\) trades under the specified inclusive trade rule and produces welfare \(b\). This event is disjoint from \(S>b\). Hence expected welfare conditional on \(X=x\) is at least \(T+bx\).

Integrating over \(X\), and retaining the contribution \(T\) for every quantile, yields

\(\displaystyle A_b\geq T+b(y-c)_+,\qquad (z)_+=\max\{z,0\}.\)

Indeed, when \(y\geq c\), the additional contribution is at least \(b\int_c^y x(1/x)\,dx=b(y-c)\); when \(y<c\), the bound is simply \(A_b\geq T\).

Set \(\alpha=1-c=1-1/e\). Combining the preceding inequalities gives

\(\displaystyle A_b-\alpha O_b \geq cT+b(y-c)_+-(1-c)by \geq b\bigl[c(1-y)+(y-c)_+-(1-c)y\bigr] =b\bigl[c-y+(y-c)_+\bigr] =b(c-y)_+ \geq0.\)

Thus \(A_b\geq(1-1/e)O_b\) for every \(b\geq0\). The calculation also covers \(b=0\), and never divides by welfare.

Finally, independence means that conditioning on any buyer value leaves both the seller distribution and the price lottery unchanged. Taking the weighted sum over buyer types therefore gives

\(\displaystyle \mathbb E_{p\sim\pi(\mu_s)}[W(p;\mu_s,\mu_b)] \geq(1-1/e)W^*(\mu_s,\mu_b).\)

This proves the required universal guarantee.

Running time and representation

Let \(L\) be the total binary input length of the seller values and masses.

Sorting takes \(O(\tau_s\log(\tau_s+1))\) rational comparisons. Computing cumulative masses takes \(O(\tau_s)\) rational arithmetic operations, after which the algorithm writes the \(\tau_s\) probability expressions above.

A conservative bound using elementary integer arithmetic is

\(\displaystyle O\!\bigl(\tau_s\log(\tau_s+1)L^2\bigr)\)

bit operations. To justify the arithmetic bound, use the product of the mass denominators as a common denominator. Its bit length is \(O(L)\); every cumulative numerator is at most that denominator because cumulative mass is at most \(1\). Rational value comparisons likewise use integers of \(O(L)\) bits.

Writing each cumulative rational explicitly gives an output length of \(O(\tau_sL)\). Logarithms and maxima remain symbolic, so constructing this exact specification requires no numerical evaluation or comparison with \(1/e\). Zero-probability entries may be retained. The lottery has at most \(\tau_s\) possible prices, and construction requires no buyer input.

⟨structured verdict parsed — rendered above⟩

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

Verification report

Verdict: proved. The output resolves the assigned question: the approximation is attainable, and the stated lottery can be constructed in polynomial time under the permitted exact symbolic representation. No major or minor mathematical issues were found.

1. Scope and cited result

The claimed guarantee has the required quantifiers: for every seller distribution, the construction gives one lottery that works for every buyer distribution. Its construction uses no buyer information.

The citation is accurate. Section 2 explicitly states that the results hold for any pair of distributions, with atomlessness assumed only for presentation. Theorem 4.1 gives the stated Random-Quantile guarantee. Independence, nonnegative values, and the welfare benchmark match the task. Moreover, the output supplies a direct finite-support proof, so its treatment of atoms does not depend on extending the paper’s atomless calculations. [Original paper, Sections 2 and 4](https://blumrosen.weebly.com/uploads/4/7/4/7/47472385/partnership.pdf).

2. Validity of the lottery

The support ordering and cumulative masses are well-defined because the seller distribution has nonempty finite support, positive masses, and total mass \(1\).

The function \(t\mapsto\ln(\max\{1,et\})\) is nondecreasing on the relevant domain. Thus every \(w_i\) is nonnegative. The normalization calculation is correct: \(C_0=0\) and \(C_n=1\) make the sum telescope to \(1\).

Every posted price is a nonnegative seller value. The expressions defining the probabilities are finite and exact, as the task permits.

3. Quantile representation and atoms

The auxiliary density \(1/x\) on \([c,1]\), with \(c=1/e\), integrates to \(1\).

The generalized quantile is defined throughout this interval because \(C_n=1\). Its intervals give exactly the stated lottery weights; boundary points have probability zero.

Crucially, the proof uses \(\Pr(S\leq q(x))\geq x\), rather than equality. This is correct for atomic distributions. Also, \(x\leq y=\Pr(S\leq b)\) implies \(q(x)\leq b\). Both quantile assertions follow directly from the finite cumulative masses.

4. Fixed-buyer welfare bound

The identity \(O_b=by+T\) correctly partitions the seller values into \(S\leq b\) and \(S>b\), including ties in the first event.

The bound \(T\geq b(1-y)\) is valid, including when the event \(S>b\) is empty.

For every price, sellers with \(S>b\) retain the item and contribute exactly \(T\). For \(x\in[c,y]\), sellers with \(S\leq q(x)\) trade and contribute welfare \(b\). These events are disjoint, and the remaining contributions are nonnegative. Independence of \(S\) and \(X\) therefore justifies the conditional lower bound \(T+bx\).

Integration against the density correctly yields \(A_b\geq T+b(y-c)_+\). The cases \(y<c\) and \(y\geq c\) are both explicitly handled.

5. Approximation calculation and universal guarantee

Every inequality and algebraic equality in the displayed chain is correct. Substituting the lower bound on \(T\) preserves the inequality because its coefficient \(c\) is positive. The final identity \(c-y+(y-c)_+=(c-y)_+\) holds in both cases.

The proof covers \(b=0\), \(y=0\), \(y=c\), \(y=1\), singleton seller support, atoms, ties, and zero optimal welfare. No division by welfare occurs.

Independence preserves the seller distribution and lottery when conditioning on a buyer type. Summing the pointwise guarantee over buyer masses gives exactly the requested welfare inequality.

6. Running time and representation

The arithmetic justification is sound. The product of the mass denominators has \(O(L)\) bits, and cumulative numerators are bounded by that denominator. Rational value comparisons likewise involve integers of \(O(L)\) bits.

Consequently, the stated \(O(\tau_s\log(\tau_s+1)L^2)\) bit-operation bound is a valid conservative bound. The \(O(\tau_sL)\) output-size bound also holds.

Leaving logarithms and maxima symbolic avoids numerical evaluation and threshold comparisons. This is sufficient for the exact lottery specification requested by the task.

Repair feedback: none required.

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