← back to the atlas

d4-conf-wine-2024-0001 (d4-conf-wine-2024-0001)

Answer: —

The anchor (named result in the paper)

Theorem 1.2 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateThe $k$-BE problem admits an efficient truthful mechanism with approximation ratio $k - 1 + \epsilon$ for every length bound $k \geq 3$ and constant $\epsilon > 0$.\footnote{ The readers familiar with the work of Ashlagi and Roth \cite{ashlagi2014free} may wonder whether our \Thm{}~\ref{theorem:uniform-upper-bound} is implied by \cite[Theorem~1]{ashlagi2014free}, stating that any solution to the $k$-BE problem, which is maximal in terms of the set of partaking agents, is guaranteed to be a $(k - 1)$-approximation.

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

The continuous mirror question, as graded

For fixed \(k\), given finitely many complete compatibility types \(T\) with rational masses \(\mu_t\), and allowed cycle patterns \(C\) of lengths \(2,\ldots,k\), choose feasible cycle masses \(x_C\ge 0\) satisfying \(\sum_C a_t(C)x_C\le \mu_t\) for every type \(t\), where \(a_t(C)\) counts its positions in \(C\). What is the maximum total participating mass \(\sum_C |C|x_C\)? Repeated appearances of a type in a pattern use distinct agents.

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

Fix an integer \(k\geq3\). A society is given by its support: a list \(T\) of \(\tau\) types with positive binary rational masses \(\mu_t\), normalized by \(\sum_t\mu_t=1\); \(\tau\) is the support size, not the number of possible types.
Each type owns one item per agent and has a reported wish set \(W_t\subseteq T\): every agent of type \(t\) accepts every other agent's item of type \(s\) exactly when \(s\in W_t\). Acceptance of another agent's item of the same type is permitted.
The allowed patterns \(\mathcal C(W)\) are all cyclic sequences \(C=(t_1,\ldots,t_\ell)\), modulo rotation, with \(2\leq\ell\leq k\) and \(t_{j+1}\in W_{t_j}\), using cyclic indices. Repeated types represent distinct agents.
An outcome assigns real masses \(x_C\geq0\) satisfying \(p_t(x):=\sum_{C\in\mathcal C(W)}a_t(C)x_C\leq\mu_t\), where \(a_t(C)\) counts occurrences of \(t\). Unused mass keeps its items; participating agents have unit utility. Write \(V(x)=\sum_C|C|x_C\) and \(\operatorname{OPT}(W,\mu)=\max_x V(x)\).
A deterministic mechanism returns such a feasible outcome. Each type reports collectively, may only delete entries from its wish set, and cannot change its mass; truthfulness means \(p_t(f(W_{-t},W'_t;\mu))\leq p_t(f(W;\mu))\) whenever \(W'_t\subseteq W_t\).
Let \(L\) be the total input bit length. There is no independent item-count parameter \(m\): item compatibility is specified directly over \(T\).

For every fixed \(k\geq3\) and constant \(\epsilon>0\), does a truthful deterministic mechanism running in \(\operatorname{poly}(\tau,L)\) guarantee \(V(f(W;\mu))\geq\operatorname{OPT}(W,\mu)/(k-1+\epsilon)\), or is this approximation guarantee impossible in polynomial time?

For finite individual agents restricted to hiding wished items, a deterministic truthful mechanism achieves ratio \(k-1+\epsilon\) in time \(n^{O(k^2/\epsilon)}\). [Source](https://arxiv.org/html/2410.06683v1)
The literature search did not identify a result settling this normalized mass formulation with collective type reports.

Modeling choices made when packaging the task

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

Partial result: an unconditional lower bound for collective truthfulness

The requested approximation guarantee remains unresolved. I prove a new obstruction that applies to every fixed $k\geq3$:

Theorem. Any truthful mechanism with approximation ratio $\rho$ in the normalized mass model must satisfy
$$ \rho\geq R_k:=\frac{k^2+2k-4}{k^2+k-2} =1+\frac{k-2}{k^2+k-2}. $$

This holds without any running-time restriction. In particular, no truthful mechanism always maximizes welfare. The construction uses only $\tau=2k$ types.

For example, $R_3=11/10$ and $R_4=10/9$. These bounds are below $k-1+\epsilon$, so they do not settle the target question.

1. Reducing repeated-type patterns to simple cycles

Represent the wish sets by a directed graph on types, with an arc $t\to s$ exactly when $s\in W_t$.

We will use graphs without self-arcs. In such a graph, every allowed pattern is a directed closed walk and can be decomposed into simple directed cycles of lengths between $2$ and $k$.

To justify the decomposition, if a closed walk repeats a vertex, split it at two occurrences of that vertex into two shorter closed walks. Continue until every component is simple. The process terminates because each split reduces the lengths of the components being split.

The decomposition preserves the multiset of directed edges. For each type $t$, its occurrence count in a closed walk equals the number of edges leaving $t$ in that walk. Consequently, decomposition preserves every type’s total occurrence count.

Thus, replacing mass $x_C$ on a pattern $C$ by mass $x_C$ on each component cycle preserves both participation and welfare. Conversely, every simple cycle of length between $2$ and $k$ is an allowed pattern.

It follows that, for our construction, the feasible participation vectors and welfare values are represented exactly by allocations to its simple cycles of length at most $k$. This argument applies to real allocation masses; no rationality assumption on the mechanism’s output is needed.

2. A construction for every $k\geq3$

Start with six types
$$ \{0,1,2,4,5,6\}. $$

Add two disjoint sets of auxiliary types
$$ U=\{u_1,\ldots,u_{k-3}\}, \qquad Q=\{q_1,\ldots,q_{k-3}\}. $$

Both sets are empty when $k=3$. There are therefore
$$ \tau=6+2(k-3)=2k $$
types.

Include the directed paths
$$ 0\to u_1\to\cdots\to u_{k-3}\to4, $$
$$ 1\to q_1\to\cdots\to q_{k-3}\to6. $$

Each path has $k-2$ edges. When $k=3$, these are simply $0\to4$ and $1\to6$.

Include precisely these additional arcs:
$$ 2\to0,\qquad 4\to2,\quad4\to5,\quad4\to6, $$
$$ 5\to0,\quad5\to1,\qquad 6\to4,\quad6\to5. $$

These arcs and paths specify all wish sets.

Let
$$ M=2k+1. $$

Give type $4$ mass $2/M$ and every other type mass $1/M$. These masses are positive binary-encoded rationals, and they sum to one.

The deviation considered below is
$$ W'_4=W_4\setminus\{2\}. $$

Thus type $4$ deletes just the arc $4\to2$.

Enumerating the simple cycles

Write $U$ and $Q$ inside a cyclic sequence for their auxiliary vertices in path order. The simple cycles are exactly:

| Cycle | Sequence | Length |
|---|---|---|
| $B$ | $(4,6)$ | $2$ |
| $C$ | $(0,U,4,2)$ | $k$ |
| $D$ | $(0,U,4,5)$ | $k$ |
| $F$ | $(1,Q,6,5)$ | $k$ |
| $G$ | $(0,U,4,6,5)$ | $k+1$ |
| $H$ | $(1,Q,6,4,5)$ | $k+1$ |

Here is a direct verification that the list is exhaustive. Contract the two auxiliary paths to obtain arcs $0\to4$ and $1\to6$. Simple cycles before and after contraction correspond bijectively, because every auxiliary vertex has exactly one incoming and one outgoing arc.

In the contracted graph:

Therefore only $B,C,D,F$ have length at most $k$. Deleting $4\to2$ removes exactly $C$ from this list.

3. The feasible allocations and their exact optima

Multiply all masses and allocation variables by $M$. The capacities are now $2$ at type $4$ and $1$ everywhere else.

Let $b,c,d,f$ denote the scaled allocation masses on $B,C,D,F$. The scaled participation amounts at the six original types are
$$ p_0=c+d,\qquad p_1=f,\qquad p_2=c, $$
$$ p_4=b+c+d,\qquad p_5=d+f,\qquad p_6=b+f. $$

Every auxiliary type in $U$ has participation $c+d$, and every auxiliary type in $Q$ has participation $f$.

Consequently, feasibility is equivalent to
$$ b,c,d,f\geq0, $$
$$ c+d\leq1,\qquad d+f\leq1,\qquad b+f\leq1. $$

Indeed, these inequalities imply $c\leq1$, $f\leq1$, and
$$ b+c+d\leq1+1=2, $$
so all remaining capacity constraints follow.

The scaled welfare and type $4$’s scaled participation are
$$ v=2b+k(c+d+f), \qquad P=b+c+d. $$

Under the deletion report, the same description holds with $c=0$.

Full report

For every feasible allocation,
$$ v \leq2(1-f)+k+kf =k+2+(k-2)f \leq2k. $$

The first inequality uses $b+f\leq1$ and $c+d\leq1$; the second uses $f\leq1$.

The allocation
$$ (b,c,d,f)=(0,1,0,1) $$
attains $2k$. Hence
$$ \operatorname{OPT}(W,\mu)=\frac{2k}{M}. $$

Moreover, equality forces $f=1$ because $k-2>0$. Feasibility then forces $b=d=0$, and attaining welfare $2k$ forces $c=1$.

Thus every welfare-optimal outcome has type $4$ participation
$$ \frac{P}{M}=\frac1M. $$

Deletion report

Now $c=0$, and
$$ v'=2b'+k(d'+f')\leq2+k. $$

The allocation
$$ (b',d',f')=(1,1,0) $$
attains this bound, so
$$ \operatorname{OPT}(W_{-4},W'_4;\mu)=\frac{k+2}{M}. $$

Equality requires $b'=1$ and $d'+f'=1$. The constraint $b'+f'\leq1$ then gives $f'=0$, and hence $d'=1$.

Every welfare-optimal outcome at the deletion report therefore gives type $4$ participation
$$ \frac{P'}M=\frac2M. $$

An always-optimal mechanism would consequently increase type $4$’s participation from $1/M$ to $2/M$ after deletion, violating truthfulness. This rules out every choice of tie-breaking.

4. The approximation lower bound

Let a truthful mechanism return arbitrary feasible outcomes at these two reports. Decompose its patterns as in Section 1, and write $v,P$ and $v',P'$ for their scaled welfare and type $4$ participation.

Truthfulness requires
$$ P'\leq P. $$

At the full report,
$$ v+(k-2)P =k(b+f)+(2k-2)(c+d) \leq3k-2. $$

At the deletion report,
$$ v'-P' =(b'+f')+(k-1)(d'+f') \leq k. $$

Combining these inequalities gives
$$ v+(k-2)v' \leq v+(k-2)(P'+k) \leq v+(k-2)P+k(k-2) \leq k^2+k-2. $$

Suppose the mechanism guarantees approximation ratio $\rho$. Since the two scaled optima are $2k$ and $k+2$, respectively,
$$ v\geq\frac{2k}{\rho}, \qquad v'\geq\frac{k+2}{\rho}. $$

Substituting into the preceding bound yields
$$ \frac{2k+(k-2)(k+2)}{\rho} \leq k^2+k-2. $$

The numerator is $k^2+2k-4$. Therefore
$$ \rho\geq \frac{k^2+2k-4}{k^2+k-2} =1+\frac{k-2}{k^2+k-2}. $$

This proves the theorem.

5. The bound is sharp for this report pair

This section concerns only the two reports constructed above. It does not construct a truthful mechanism on the whole domain.

Set
$$ N=k^2+2k-4, \qquad P_*=\frac{k^2+4k-4}{N} =1+\frac{2k}{N}. $$

Because $N>2k$ for $k\geq3$, we have $1<P_*<2$.

At the full report, choose
$$ b=d=P_*-1,\qquad c=f=2-P_*. $$

All three feasibility inequalities hold with equality, and type $4$’s participation is $P_*$. Welfare is
$$ v=3k-2-(k-2)P_*. $$

At the deletion report, choose
$$ b'=d'=\frac{P_*}{2}, \qquad f'=1-\frac{P_*}{2}. $$

This is feasible, gives the same participation $P'=P_*$, and has welfare
$$ v'=k+P_*. $$

Direct substitution gives
$$ \frac{v}{2k} = \frac{v'}{k+2} = \frac{k^2+k-2}{k^2+2k-4}. $$

Thus these outcomes satisfy the truthfulness inequality for the report pair and attain the lower bound exactly. A stronger impossibility result will require additional constraints or a different construction.

6. What this establishes, and what remains open

The construction proves that collective type reports create an incentive obstruction even when optimal participation vectors are unique. This differs substantively from the individual-agent setting: the finite-agent literature discusses an optimal truthful mechanism without an efficiency requirement, with individual agents as the strategic units. [Barter Exchange with Bounded Trading Cycles](https://arxiv.org/html/2410.06683v1)

Welfare optimization itself remains polynomial-time solvable here. For fixed $k$, enumerate the at most
$$ \sum_{\ell=2}^{k}\tau^\ell $$
candidate sequences, test their arcs, and remove rotation duplicates. The outcome constraints then form a rational linear program of polynomial encoding length. It is feasible at zero and bounded because
$$ V(x)=\sum_t p_t(x)\leq1. $$

Polynomial-time rational linear programming therefore computes an exact welfare optimum. The obstruction above concerns implementing welfare guarantees truthfully.

Finally,
$$ R_k<2\leq k-1<k-1+\epsilon. $$

Accordingly, the proved lower bound excludes exact welfare maximization but does not exclude the approximation requested in the task. Constructing that mechanism, or proving its impossibility, remains open in this write-up.

⟨structured verdict parsed — rendered above⟩

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

Verification report

Result: partial. The stated lower bound is correct, including its sharpness for the specified report pair. The polynomial-time welfare optimization claim is also justified. However, neither result settles the requested approximation guarantee under collective truthfulness.

There is no false central step or substantive gap in the lower-bound argument. The major outstanding issue is completion of the assigned task, which the prover explicitly acknowledges.

1. Reduction to simple cycles

The reduction is valid for the graphs used in the construction.

Assigning the original pattern mass to each component is valid even when a component occurs more than once: its contributions are added. The argument works for arbitrary nonnegative real masses.

This reduction concerns representations of outcomes, not changes to the mechanism. Participation is preserved, so using the decomposed outcomes in the truthfulness comparison is legitimate.

2. Construction and cycle enumeration

The instance satisfies the task’s input restrictions:

$$ |T|=6+2(k-3)=2k, $$

and its total mass is

$$ \frac{2+(2k-1)}{2k+1}=1. $$

All masses are positive rational numbers with finite binary encodings. The deviation deletes precisely one permitted wish-set entry.

The cycle enumeration is exhaustive. Auxiliary vertices have unique incoming and outgoing arcs, so contracting the paths preserves simple cycles bijectively. The cases in the contracted graph cover all possibilities:

Restoring the paths gives the stated lengths. In particular, $G$ and $H$ have length $k+1$ and are excluded. Deleting $4\to2$ removes exactly $C$ among the allowed simple cycles.

The boundary case $k=3$ is handled correctly by taking both auxiliary sets empty.

3. Feasibility and exact optima

The participation formulas follow directly from the listed cycles. The reduced feasibility description is equivalent to the full capacity system:

$$ c+d\leq1,\qquad d+f\leq1,\qquad b+f\leq1, $$

together with nonnegativity. These imply the individual bounds on $c$ and $f$, and

$$ b+c+d\leq2. $$

Auxiliary capacities add no further restrictions.

Full report

The upper bound

$$ v\leq k+2+(k-2)f\leq2k $$

uses exactly the stated feasibility inequalities. The exhibited allocation attains it.

Since $k-2>0$, equality forces $f=1$. Feasibility then gives $b=d=0$, and welfare equality gives $c=1$. Thus every optimum has scaled type $4$ participation $P=1$.

Deletion report

With $c=0$, the bound

$$ v'=2b'+k(d'+f')\leq2+k $$

follows from $b'\leq1$ and $d'+f'\leq1$. The exhibited allocation attains it.

Equality forces $b'=1$ and $d'+f'=1$, hence $f'=0$ and $d'=1$. Every optimum therefore has $P'=2$.

After undoing normalization, deletion increases optimal type $4$ participation from $1/M$ to $2/M$. This contradicts the required truthfulness inequality for every always-optimal mechanism, independently of tie-breaking.

4. Approximation lower bound

Both critical identities and inequalities are correct:

$$ v+(k-2)P =k(b+f)+(2k-2)(c+d) \leq3k-2, $$

and

$$ v'-P' =(b'+f')+(k-1)(d'+f') \leq k. $$

Truthfulness gives $P'\leq P$. Since $k-2>0$, combining the inequalities in the stated direction yields

$$ v+(k-2)v'\leq k^2+k-2. $$

For a positive approximation ratio $\rho$, applying its guarantee separately at both reports gives

$$ \frac{2k+(k-2)(k+2)}{\rho}\leq k^2+k-2. $$

The numerator simplifies correctly to $k^2+2k-4$, proving

$$ \rho\geq R_k =\frac{k^2+2k-4}{k^2+k-2}. $$

The examples $R_3=11/10$ and $R_4=10/9$ are correct. No running-time assumption enters this argument.

5. Sharpness for the report pair

The sharpness calculation is correct and appropriately limited to the two reports.

For

$$ N=k^2+2k-4, $$

the assertion $N>2k$ holds for every $k\geq3$, so $1<P_*<2$. Both proposed allocations are nonnegative and feasible.

At the full report, all three reduced constraints hold with equality, participation is $P_*$, and the first lower-bound inequality is tight. At the deletion report, participation is also $P_*$, and the second inequality is tight.

The common normalized welfare fraction is correctly computed as

$$ \frac{v}{2k} =\frac{v'}{k+2} =\frac{k^2+k-2}{k^2+2k-4}. $$

Consequently, the pairwise truthfulness constraint alone cannot strengthen this construction’s bound. The prover correctly avoids claiming that these two outcomes extend to a globally truthful mechanism.

6. Polynomial-time optimization and literature comparison

The welfare optimization claim is justified for fixed $k$. Enumerating at most

$$ \sum_{\ell=2}^{k}\tau^\ell $$

sequences produces polynomially many variables. Rotation removal, arc checks, and occurrence-count computation take polynomial time.

The resulting linear program has rational coefficients and polynomial encoding length. It is feasible at zero, and

$$ V(x)=\sum_t p_t(x)\leq1 $$

bounds its objective. These satisfy the hypotheses of polynomial-time rational linear programming for computing an exact optimum.

This establishes polynomial-time optimization without the truthfulness requirement. It does not supply the mechanism requested in the task.

The cited paper does state the existence of a computationally inefficient optimal truthful mechanism for the finite individual-agent model. The prover’s contextual comparison is accurate; it is not used as a theorem about collective reports. [Barter Exchange with Bounded Trading Cycles](https://arxiv.org/html/2410.06683v1)

7. Outstanding issue and actionable feedback

Major issue — the assigned approximation question remains unresolved. The proved bound satisfies

$$ R_k<2\leq k-1<k-1+\epsilon. $$

It therefore excludes exact truthful optimization but does not exclude the requested approximation ratio. Polynomial-time unconstrained optimization does not establish a truthful approximation mechanism either.

No clarification or expositional repair can close this gap. To complete the assignment, the prover must establish either:

The existing construction and lower-bound proof can be retained as rigorous partial progress.

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