← back to the atlas

d4-conf-aaai-2024-1498 (d4-conf-aaai-2024-1498)

Answer: Polynomial-time solvable in \(O(m+\tau+L)\) time including input reading; every valid instance admits such a mechanism.

The anchor (named result in the paper)

Theorem 2 — class: other

The continuous mirror question, as graded

Given a finite graph of trader types with masses \(\mu_t\), where each type specifies role, valuation, initial awareness, and linked cohorts, does there exist a measurable direct mechanism assigning each trader an integral allocation and payment that balances traded mass among qualified traders, is individually rational, and makes truthful valuation reports and full neighbor invitations dominant strategies?

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

A society is given by its support: \(\tau\) types with positive binary-rational masses \(\mu_t\), summing to \(1\); \(\tau\) counts supported types, not possible types. Type \(t\) specifies a buyer/seller role, a nonnegative rational valuation \(v_t\), initial awareness, and neighbors in an undirected cohort graph with \(m\) edges. Let \(L\) be the total input bit length; state running times in \(m,\tau,L\). Initially aware buyers and sellers both have positive mass.
Realize each cohort as an atomless interval \(X_t=[0,\mu_t)\), with Lebesgue measure \(\lambda\). Every seller initially owns one unit of a homogeneous commodity; every buyer initially owns none and demands at most one unit.
Each individual reports a nonnegative real valuation and a subset of her linked cohorts; inviting a cohort invites every individual in it. Reports may vary measurably within cohorts. An individual is qualified precisely when reachable by a finite directed invitation path from an initially aware individual, including paths of length zero; write \(Q\) for this set.
A deterministic direct mechanism assigns measurable final holdings \(\pi(x)\in\{0,1\}\) and integrable payments \(p(x)\in\mathbb R\), positive for payments to the auctioneer. Unqualified sellers retain their units, unqualified buyers receive none, and all unqualified individuals pay zero; qualified outcomes depend only on qualified reports.
At every report profile, feasibility requires \(\int_{Q\cap B}\pi\,d\lambda=\int_{Q\cap S}(1-\pi)\,d\lambda\). Utilities are \(u_x=\pi(x)v_x-p(x)\) for buyers and \(u_x=(\pi(x)-1)v_x-p(x)\) for sellers.
Individual rationality requires nonnegative utility when reporting the true valuation, for every invitation subset and every measurable profile of others' reports. Incentive compatibility requires reporting the true valuation and inviting all linked cohorts to weakly dominate every joint valuation/invitation deviation, for each individual and every measurable profile of others' reports; require these properties for all nonnegative true valuations. Individuals, rather than cohorts, are the strategic players.

Is deciding whether such a feasible, individually rational, incentive-compatible mechanism exists solvable in polynomial time in \(m,\tau,L\), or is this decision problem NP-hard?

For finite trader networks, dynamic trade reduction is individually rational and makes truthful valuation reports together with full invitations weakly dominant ([Li, Cao and Zhao, 2024](https://ojs.aaai.org/index.php/AAAI/article/download/28845/29607)). This is a mechanism-existence result, rather than a complexity classification. No result settling the exact atomless cohort problem above was located in the literature search.

Modeling choices made when packaging the task

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

Result

The decision problem is polynomial-time solvable: every valid instance admits such a mechanism.

The no-trade mechanism already proves existence literally; to address the substantive trading question, we construct a mechanism that permits positive-mass trade, uses qualification, and even balances payments exactly.

The construction uses a fixed price and a fixed measure-preserving pairing of buyers with sellers. Neither depends on reports.

1. Qualification facts

Regard the population as the disjoint union \(X=\bigsqcup_{t=1}^{\tau}X_t\), with measure \(\lambda\) equal to the sum of the cohort measures. Fix a measurable report profile.

Lemma 1. The qualified set \(Q\) is a union of entire cohorts, and hence is measurable.

Proof. An initially aware cohort is entirely qualified. If an individual in a cohort is reached by a positive-length invitation path, the last invitation on that path invites her entire cohort. Thus every individual in that cohort is qualified. There are only finitely many cohorts. \(\square\)

The following facts concern individual deviations, including deviations by individuals of measure zero.

Lemma 2. Fix an individual \(x\) and all other individuals’ reports.

Proof. Valuation reports do not affect reachability. If a finite invitation path reaches \(x\), truncate it at its first occurrence of \(x\). This path uses no outgoing invitation of \(x\), so it remains valid after any change to \(x\)’s invitations. Applying this argument in both directions proves the first assertion.

For the second assertion, enlarging the invitation subset adds directed edges and removes none. Every previously valid path remains valid. \(\square\)

Lemma 3. Changing reports outside \(Q\), while keeping all reports on \(Q\) fixed, leaves \(Q\) unchanged.

Proof. Every original qualification path consists entirely of individuals in \(Q\), so it remains valid.

Conversely, suppose a modified profile has a qualification path reaching outside the original \(Q\). Consider its first individual outside \(Q\). Its predecessor belongs to \(Q\), whose invitation report was unchanged. That invitation would already have qualified the individual under the original profile, a contradiction. \(\square\)

2. A fixed-price, fixed-pairing mechanism

Fix a finite rational price \(c\), with \(c\geq 0\). For universal existence, take \(c=1\).

Let \(B\) and \(S\) denote the buyer and seller populations, and write \(\beta=\lambda(B)\), \(\sigma=\lambda(S)\), and \(h=\min\{\beta,\sigma\}\). The awareness assumptions imply \(\beta>0\) and \(\sigma>0\).

Choose fixed orders of buyer cohorts and seller cohorts. Concatenating their intervals gives bijections

\(b:[0,\beta)\longrightarrow B,\qquad s:[0,\sigma)\longrightarrow S.\)

For example, if buyer cohort \(t\) begins at cumulative coordinate \(a_t\), then \(b(u)=(t,u-a_t)\) on its coordinate interval. Thus both maps are finite unions of translations. They and their inverses are measurable and preserve Lebesgue measure.

For every \(u\in[0,h)\), permanently pair buyer \(b(u)\) with seller \(s(u)\). Individuals outside the images of this interval are unpaired.

At a report profile, let \(r(x)\) denote the reported valuation and \(Q\) the qualified set. Define the trading coordinates by

\(D=\{u\in[0,h): b(u)\in Q,\ s(u)\in Q,\ r(b(u))\geq c,\ r(s(u))\leq c\}.\)

For each \(u\in D\), assign

\(\pi(b(u))=1,\quad p(b(u))=c,\qquad \pi(s(u))=0,\quad p(s(u))=-c.\)

Every other buyer receives nothing and pays zero. Every other seller retains her unit and pays zero.

This specifies a deterministic mechanism at every measurable report profile.

3. Measurability, feasibility, and dependence on qualified reports

Measurability. By Lemma 1, \(Q\) is measurable. The reported valuations are measurable, and the coordinate maps are piecewise translations. Consequently \(D\), \(b(D)\), and \(s(D)\) are measurable. The allocation and payment functions are therefore measurable.

Payments are integrable because

\(\int_X |p(x)|\,d\lambda(x)=2c\,\lambda(D)\leq 2ch<\infty.\)

This bound holds even for unbounded valuation reports.

Feasibility. Only buyers in \(b(D)\) receive units, and only sellers in \(s(D)\) relinquish units. Both sets consist of qualified individuals. Measure preservation gives

\(\int_{Q\cap B}\pi\,d\lambda=\lambda(b(D))=\lambda(D)=\lambda(s(D))=\int_{Q\cap S}(1-\pi)\,d\lambda.\)

Unqualified buyers receive nothing, unqualified sellers retain their units, and all unqualified individuals pay zero.

The mechanism also balances payments exactly:

\(\int_X p\,d\lambda=c\,\lambda(D)-c\,\lambda(D)=0.\)

Dependence on qualified reports. The price and pairing are fixed beforehand. At a profile, a pair trades only when both individuals are qualified, so its trading decision uses only their qualified valuation reports. Lemma 3 shows that changing unqualified reports leaves qualification unchanged. Therefore qualified outcomes depend only on qualified reports.

4. Individual rationality and incentive compatibility

These arguments hold for every individual, every nonnegative true valuation, and every measurable profile of others’ reports.

Individual rationality

Fix an arbitrary invitation subset for individual \(x\), and suppose she reports her true valuation \(v\).

If she does not trade, her utility is zero. If she trades:

Thus individual rationality holds for every invitation subset.

Dominance against joint deviations

Fix \(x\), her true valuation \(v\), and all other reports. Compare truthful reporting with full invitations against an arbitrary joint valuation/invitation deviation.

If \(x\) is unpaired, her utility is always zero. If she is unqualified under either action, Lemma 2 shows she is unqualified under both, and again her utility is always zero.

Otherwise, \(x\) is paired and qualified under both actions. Let \(y\) be her fixed partner. Define \(A(I)\in\{0,1\}\) to indicate that, under \(x\)’s invitation subset \(I\):

Qualification of \(x\) is already assured. Lemma 2 gives

\(A(I)\leq A(I_{\mathrm{full}}).\)

In particular, inviting more people cannot introduce competition for \(x\)’s partner, because the pairing never changes.

Let \(w\) be \(x\)’s true utility from trading: \(w=v-c\) for a buyer, and \(w=c-v\) for a seller.

There are two cases.

Case \(w\geq 0\). Truthful reporting satisfies \(x\)’s acceptance condition. Her utility with full invitations is

\(u_{\mathrm{truth,full}}=wA(I_{\mathrm{full}}).\)

Under a deviation, let \(e\in\{0,1\}\) indicate whether her reported valuation satisfies her acceptance condition. Her utility is

\(u_{\mathrm{dev}}=weA(I)\leq wA(I_{\mathrm{full}})=u_{\mathrm{truth,full}}.\)

Case \(w<0\). Truthful reporting rejects trade, giving utility zero. Any deviation either causes no trade, giving zero, or causes trade, giving \(w<0\). Hence it cannot improve utility.

Therefore truthful valuation reporting together with full invitations weakly dominates every joint deviation.

Nothing in this proof treats a singleton invitation as negligible: an individual can qualify an entire cohort, and Lemma 2 handles that change pointwise.

5. Positive-mass trade

The mechanism need not be a no-trade mechanism.

First, take \(c=1\) and order initially aware cohorts first on each side. Let \(\beta_0>0\) and \(\sigma_0>0\) be the initially aware buyer and seller masses. At the truthful profile where every buyer has valuation \(2\) and every seller has valuation \(0\), every coordinate in \([0,\min\{\beta_0,\sigma_0\})\) trades, regardless of invitations. Thus traded mass is at least \(\min\{\beta_0,\sigma_0\}>0\).

There is also a stronger statement for the given truthful profile. Suppose full invitations qualify a buyer cohort \(i\) and a seller cohort \(j\) with \(v_i>v_j\). Fix the price \(c=(v_i+v_j)/2\), and put these cohorts first in their respective orders. Then their paired individuals trade over \([0,\min\{\mu_i,\mu_j\})\), yielding positive traded mass.

These choices are fixed before reports. With those constants held fixed, the preceding proof still establishes individual rationality and incentive compatibility for all nonnegative true valuations.

6. Complexity classification

On the promised domain of valid instances, the decision algorithm always returns yes. Its decision step takes constant time; including reading the input, a bound is \(O(m+\tau+L)\).

A finite description of the construction can also be produced in polynomial time. It consists of the fixed price, cohort orders, and cumulative interval endpoints. Using ordinary exact rational arithmetic, a conservative preprocessing bound is \(O(m+\tau L^2+L)\): there are \(O(\tau)\) cumulative additions, and their intermediate integer bit lengths are \(O(L)\).

These are bounds for the finite input and mechanism description. They do not assume an algorithmic encoding of arbitrary measurable report functions.

The [finite-network DTR theorem of Li, Cao and Zhao](https://ojs.aaai.org/index.php/AAAI/article/download/28845/29607) is not needed for this conclusion: the construction and proof above apply directly to the stated atomless model.

⟨structured verdict parsed — rendered above⟩

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

The prover resolves the stated decision problem. The fixed-price mechanism satisfies the required measurability, feasibility, individual rationality, and incentive compatibility conditions. I found no major or minor mathematical issues.

The task requires the existence of a feasible, individually rational, incentive-compatible mechanism. It imposes no minimum trade volume, efficiency requirement, or revenue requirement. Consequently, the observation that a no-trade mechanism satisfies the literal requirements is valid.

The prover also verifies a mechanism capable of positive-mass trade. Its correctness therefore does not rest solely on the no-trade observation.

The argument is correct. Initial awareness is specified by type, so each initially aware cohort is entirely qualified. Every invitation targets an entire cohort. Thus, if a positive-length path reaches one member of a cohort, the last invitation on that path reaches every member.

Since there are finitely many cohorts, their qualified union is measurable. This conclusion holds even when invitation reports vary within cohorts.

Both assertions are justified.

A path reaching an individual can be truncated at its first occurrence of that individual. The truncated path uses none of that individual’s outgoing invitations. Applying this reasoning in both directions establishes that changing her invitations cannot change her own qualification. Valuation reports do not enter the reachability definition.

Enlarging an invitation subset only adds directed edges, so it preserves every existing qualification path. This argument applies pointwise, including when a single individual’s invitation qualifies an entire cohort. No measure-zero exception is being assumed.

The proof correctly establishes that qualification remains unchanged.

Every original qualification path uses only originally qualified individuals, whose reports remain fixed. Conversely, any modified path leaving the original qualified set would have a first individual outside it. The predecessor’s unchanged invitation would already have qualified that individual originally, contradicting the definition of the original set.

Initial individuals cannot supply an exception to the first-exit argument, since they belong to the original qualified set.

The buyer and seller concatenations are well-defined measurable bijections. Their finite translation pieces preserve Lebesgue measure in both directions. The half-open intervals avoid ambiguous assignments at cohort boundaries.

The fixed pairing assigns each paired individual exactly one partner. Individuals outside the paired intervals have explicitly specified outcomes.

The conditions defining the trading set \(D\) are measurable: qualification is measurable, and composition of the measurable valuation reports with the translation maps preserves measurability. The images \(b(D)\) and \(s(D)\) are measurable because the maps and their inverses consist of finitely many translations.

The payment calculation is correct:
\[ \int_X |p(x)|\,d\lambda(x)=2c\,\lambda(D)\leq 2ch<\infty. \]
Thus arbitrary unbounded valuation reports do not cause a payment-integrability problem.

The feasibility calculation is exact. The only buyers receiving units are those in \(b(D)\), and the only sellers relinquishing units are those in \(s(D)\). Both populations have measure \(\lambda(D)\), and both consist entirely of qualified individuals.

The mechanism explicitly gives the required default holdings and zero payments to unqualified individuals. Its claimed payment balance also follows from equal trading masses and opposite payments of magnitude \(c\).

Dependence on qualified reports is verified correctly. The price and pairing are fixed parameters; a trading pair’s valuation conditions involve only qualified individuals. Lemma 3 establishes invariance under changes to reports outside the qualified set.

The utility calculations agree with the task’s formulas. A nontrading buyer receives zero utility, and a nontrading seller retains her initial unit and receives zero utility.

A truthfully reporting trading buyer satisfies \(v\geq c\) and receives utility \(v-c\). A truthfully reporting trading seller satisfies \(v\leq c\) and receives utility \(c-v\). Both are nonnegative.

The argument does not restrict the individual’s invitation subset or others’ reports, so it establishes the required universal individual rationality.

The proof covers every individual.

Unpaired individuals always receive zero utility. Lemma 2 ensures that an individual cannot change her own qualification, so unqualified individuals also always receive zero utility.

For a paired, qualified individual, the partner’s valuation report remains fixed. Increasing invitations can only increase the partner’s qualification. Hence the claimed inequality
\[ A(I)\leq A(I_{\mathrm{full}}) \]
is justified. Fixed pairing prevents changes in the qualified population from displacing either partner.

When \(w\geq 0\), truthful reporting accepts trade, including the boundary \(w=0\), and
\[ weA(I)\leq wA(I_{\mathrm{full}}) \]
follows from \(e\in\{0,1\}\) and the preceding monotonicity.

When \(w<0\), truthful reporting rejects trade. A deviation gives either zero utility or the negative utility \(w\). Thus it cannot improve utility.

These cases establish the stated weak dominance against every joint valuation and invitation deviation, for every nonnegative true valuation.

The first claim is correct as a demonstration of possible trade under the universally quantified valuation domain. Placing initially aware cohorts first makes both partners initially qualified throughout the interval of length \(\min\{\beta_0,\sigma_0\}\). Buyer valuation \(2\), seller valuation \(0\), and price \(1\) satisfy both acceptance conditions.

The conditional claim concerning the given valuations is also correct. If the specified cohorts qualify under full invitations and \(v_i>v_j\), their midpoint price lies strictly between their valuations. Placing those cohorts first pairs a mass \(\min\{\mu_i,\mu_j\}>0\) that trades at that profile.

These claims do not assert positive trade for every instance or every profile. Their stated scope is appropriate. Fixing these parameters before reports also preserves the universal incentive argument.

On the promised domain, universal existence makes the constant-answer decision algorithm valid. Including input reading, the stated \(O(m+\tau+L)\) bound is polynomial.

The optional mechanism-description bound is also justified. There are \(O(\tau)\) cumulative rational additions. Intermediate fractions have \(O(L)\) bit length: their denominators can be represented using products of input denominators, whose total bit length is bounded by the input length. Ordinary exact rational arithmetic therefore supports the conservative \(O(m+\tau L^2+L)\) preprocessing bound.

The prover appropriately distinguishes producing a finite mechanism description from evaluating arbitrary measurable report functions. The latter is not required by the existence decision problem.

No repair or additional clarification is needed. The finite-network theorem is explicitly unused, so the conclusion requires no unverified external theorem application.

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