Answer: The rule satisfies group IR, \(\mathrm{GFT}=\mathrm{FB}\), dominant-strategy IC, and SBB for every admissible exact-mass population.
Theorem 4.3 — class: algorithmic
Given finite rational mass distributions \(\mu^B\) over buyer values and \(\mu^S\) over seller costs in \([0,1]\), does the rule that trades when \(\bar v>\bar c\) and sets the shared per-member payment and receipt to \((\bar v+\bar c)/2\) achieve group IR and first-best gains from trade in the exact-mass population, while remaining IC and SBB?
Two nonatomic societies, buyers and sellers, each have total mass \(1\) and trade one indivisible item non-excludably. Their publicly known exact type distributions \(\mu^B,\mu^S\) have nonempty finite supports of rational values and costs in \([0,1]\).
A society is given by its support: the list of types with positive mass, each mass a binary rational. Let \(\tau\) be the combined support size, not the number of possible types, and \(L\) the total input bit length; state any running times in \(m,\tau,L\), with \(m=1\) item.
Each member privately knows its type and may report any number in \([0,1]\); the public distributions are fixed independently of reports. Write \(\bar v=\int v\,d\mu^B\) and \(\bar c=\int c\,d\mu^S\).
The rule ignores reports and uses shared allocation \(x=\mathbf 1\{\bar v>\bar c\}\) and shared payment and receipt \(p=r=x(\bar v+\bar c)/2\). Buyer and seller utilities are respectively \(xv-p\) and \(r-xc\); utility ties favor trade.
Group IR means each society's integrated utility is nonnegative, with strictly positive utilities required when trade occurs. IC means dominant-strategy truthfulness for individual members; SBB means equality of total payments and receipts. GFT is \(x(\bar v-\bar c)\), and FB is its maximum over the two possible shared allocations.
Does this rule achieve group IR and GFT equal to FB for every such exact-mass population, while satisfying IC and SBB, or can any of these guarantees fail?
For equal finite groups with independent draws from known bounded priors, the corresponding report-independent rule is IC and SBB; under a strictly positive mean gap, group IR holds with probability \(1-e^{-\Omega(n)}\) and its expected GFT/FB ratio is \(1-e^{-\Omega(n)}\). [Xu, Zhang, and Conitzer](https://arxiv.org/html/2312.11800v1)
No result settling precisely this exact-mass formulation was identified in the literature search.
All four guarantees hold for every population in the question. Strict positivity when trade occurs holds for each society’s integrated utility, as required by the stated definition of group IR.
Write the buyer distribution as \(\mu^B=\sum_{i=1}^{b}\alpha_i\delta_{v_i}\) and the seller distribution as \(\mu^S=\sum_{j=1}^{s}\beta_j\delta_{c_j}\), where all masses are positive and \(\sum_i\alpha_i=\sum_j\beta_j=1\). Thus \(\tau=b+s\),
\(\bar v=\sum_i\alpha_i v_i,\qquad \bar c=\sum_j\beta_j c_j.\)
Define \(\Delta=\bar v-\bar c\). The rule sets \(x=\mathbf 1\{\Delta>0\}\) and \(p=r=x(\bar v+\bar c)/2\).
Since every buyer pays the same amount and the buyer society has total mass \(1\), its integrated utility is
\(U^B=\int(xv-p)\,d\mu^B=x\bar v-p=x\Delta/2.\)
Similarly, the seller society’s integrated utility is
\(U^S=\int(r-xc)\,d\mu^S=r-x\bar c=x\Delta/2.\)
There are two cases:
These cases exhaust all populations and establish precisely the required group IR.
Individual members can have negative utility. For example, if buyers have types \(0\) and \(1\), each with mass \(1/2\), and every seller has cost \(0\), then \(p=1/4\). Buyers of type \(0\) obtain utility \(-1/4\), while each society’s integrated utility is \(1/4\). This does not violate the specified group IR.
For either possible shared allocation \(y\in\{0,1\}\), aggregate gains from trade are
\(\mathrm{GFT}(y)=\int yv\,d\mu^B-\int yc\,d\mu^S=y\Delta.\)
Consequently,
\(\mathrm{FB}=\max_{y\in\{0,1\}}y\Delta=\max\{0,\Delta\}.\)
The rule obtains
\(\mathrm{GFT}=x\Delta=\mathbf 1\{\Delta>0\}\Delta=\max\{0,\Delta\}=\mathrm{FB}.\)
This equality also covers \(\Delta=0\): both allocations yield zero gains, and the stated rule chooses no trade. No approximation ratio is needed when \(\mathrm{FB}=0\).
Fix any buyer’s true type \(v\), every other member’s reports, and any alternative report \(a\in[0,1]\). The public distributions are fixed independently of reports, so reporting either \(v\) or \(a\) produces exactly the same allocation and payment. Hence
\(u^B(v;\text{report }v)=xv-p=u^B(v;\text{report }a).\)
Truthful reporting therefore weakly dominates every alternative report. The same argument gives, for every seller’s true cost \(c\) and alternative report \(a\),
\(u^S(c;\text{report }c)=r-xc=u^S(c;\text{report }a).\)
Thus the rule is dominant-strategy IC. The convention that utility ties favor trade cannot distinguish these reports: they produce the same trade decision as well as the same monetary utility.
Finally, total payments and receipts are
\(P=\int p\,d\mu^B=p,\qquad R=\int r\,d\mu^S=r.\)
Because \(p=r\), strong budget balance holds for every report profile.
At \(\bar v=\bar c\), the explicit allocation formula prescribes no trade. If one instead changed the formula to require trade at equality, SBB would imply \(U^B+U^S=\bar v-\bar c=0\), preventing both integrated utilities from being strictly positive. The strict inequality in the given rule therefore handles this boundary consistently with strict group IR.
The finite-sample setting in [Xu, Zhang, and Conitzer](https://arxiv.org/html/2312.11800v1) involves independent draws from priors. Here, the public distributions specify the actual population masses exactly, so the integrated utilities above are deterministic; no concentration argument is required.
For \(m=1\), the rule can be evaluated using \(O(\tau)\) rational arithmetic operations. Computing the means with unreduced common denominators keeps intermediate integers at \(O(L)\) bits: each denominator is a product of input denominators whose total bit length is \(O(L)\). Ordinary integer arithmetic therefore gives a conservative running time of \(O(\tau L^2)\) bit operations.
⟨structured verdict parsed — rendered above⟩
The prover resolves the task correctly. All four guarantees hold under the stated definitions. The proof covers every sign of the mean gap, establishes dominant-strategy IC for all allowed reports, and gives a valid polynomial bit-complexity bound. No major or minor mathematical issues were found.
The finite-support representations correctly encode both societies. Positive masses and normalization to total mass \(1\) are hypotheses of the task. The definitions of \(\bar v\), \(\bar c\), \(\Delta\), \(x\), \(p\), and \(r\) match the specified rule.
Nonatomic membership is compatible with a finite-support type distribution: positive mass at a type does not mean that a single member has positive mass. The argument does not confuse these notions.
The buyer utility calculation is valid:
\(U^B=x\bar v-p=x\Delta/2\).
Pulling the shared allocation and payment outside the integral is justified because they are constant across members. The payment term integrates to \(p\) because buyer mass is \(1\).
The seller calculation,
\(U^S=r-x\bar c=x\Delta/2\),
is valid for the same reasons.
The two cases are exhaustive:
This establishes precisely the required group IR, including strict positivity whenever trade occurs.
The example distinguishing group IR from individual IR is also correct: \(\bar v=1/2\), \(\bar c=0\), and \(p=r=1/4\). Type-zero buyers receive utility \(-1/4\), while both societies have integrated utility \(1/4\). This is permitted by the task.
For either admissible shared allocation \(y\in\{0,1\}\), the stated expression \(\mathrm{GFT}(y)=y\Delta\) follows directly from the definitions. Consequently, \(\mathrm{FB}=\max\{0,\Delta\}\).
The identity
\(\mathbf 1\{\Delta>0\}\Delta=\max\{0,\Delta\}\)
holds for positive, zero, and negative \(\Delta\). Thus the rule achieves \(\mathrm{GFT}=\mathrm{FB}\) on every admissible population.
The proof correctly avoids an undefined approximation ratio when \(\mathrm{FB}=0\).
The proof fixes an arbitrary member’s true type, arbitrary reports by all other members, and an arbitrary alternative report in \([0,1]\). These are the required quantifiers.
Because the public distributions are fixed independently of reports and the rule ignores reports, every alternative report produces exactly the same allocation and transfer. The displayed buyer and seller utility equalities therefore hold. Truthfulness weakly dominates every alternative report, establishing dominant-strategy IC.
No restriction to reports inside the finite support is imposed. The argument covers the entire permitted report domain.
The identities \(P=p\) and \(R=r\) correctly use the unit mass of each society. Since \(p=r\), total payments equal total receipts for every report profile. This establishes SBB as defined.
At \(\bar v=\bar c\), the explicit allocation formula requires no trade. The prover correctly follows that formula.
The task’s utility-tie convention does not provide a reporting deviation that changes this outcome: all reports induce the same allocation and transfers. The prover also correctly observes that trading at equality under SBB would make the sum of integrated utilities zero, so both societies could not receive strictly positive integrated utility.
There is no unresolved boundary case.
The contextual statement about independent draws from priors agrees with the model described in [Xu, Zhang, and Conitzer](https://arxiv.org/html/2312.11800v1). The prover does not invoke that paper’s theorem to establish the exact-mass result, so no external theorem application requires additional hypotheses.
The \(O(\tau)\) rational-arithmetic count is valid for computing the two weighted means and then evaluating the rule.
The intermediate-size justification is sound. Unreduced denominators can be products of input denominators, whose combined bit length is \(O(L)\). Weighted sums and the final comparison also have \(O(L)\)-bit representations. Ordinary integer addition, multiplication, and cross-multiplication therefore support the conservative \(O(\tau L^2)\) bit-operation bound.
The running time is stated for \(m=1\) and uses actual support size \(\tau\), as requested.
None. The write-up needs no additional mathematical clarification or repair.
⟨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.