← back to the atlas

d4-conf-sagt-2023-0001 (d4-conf-sagt-2023-0001)

Answer: —

The anchor (named result in the paper)

Theorem 3.1 — class: algorithmic

The continuous mirror question, as graded

For fixed \(\tau_0\ge2\), given a finite candidate set \(C\subset\mathbb{R}\) with \(|C|\ge2\), and empirical position masses \(\mu_x=k_x/n\) supported on at most \(\tau_0\) positions, determine the infimum limiting worst-case per-capita social-cost approximation ratio over anonymous deterministic mechanism families \(M_n\). Each \(M_n\) must choose distinct sites \((a,b)\in C^2\) and be strategyproof against every single-resident report change, which transfers mass \(1/n\); the ratio is evaluated on profiles with support at most \(\tau_0\) as \(n\to\infty\).

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

Fix an integer \(\tau_0\ge2\). All residents approve both facilities; a resident at \(x\in\mathbb R\) incurs cost \(d_x(a,b)=|x-a|+|x-b|\). The public candidate set \(C\subset\mathbb R\) has \(m\ge2\) distinct sites, and feasible outcomes satisfy \((a,b)\in C^2\), \(a\ne b\).
A society is given by its support: the list of its \(\tau\) positions with positive mass, each mass a binary rational. Here \(\mu_x=k_x/n\), \(k_x\in\mathbb Z_{>0}\), \(\sum_xk_x=n\), and \(n\ge2\) is supplied separately; \(\tau\) is the support size, not the number of possible types.
For finite encoding, candidate and support coordinates are binary rationals; \(L\) is the total input bit length. State any running times in \(m,\tau,L,\log n,\tau_0\); the mechanism class has no efficiency restriction.
An admissible family \((M_n)_{n\ge2}\) consists of anonymous deterministic mechanisms defined on every real position profile and every candidate set, with fixed deterministic tie-breaking. Anonymity means dependence only on the empirical masses, the public \(n\), and \(C\).
Require strategyproofness on all profiles, including those with support exceeding \(\tau_0\): for every occupied \(x\) and report \(y\in\mathbb R\), \(d_x(M_n(\mu,C))\le d_x(M_n(\mu+n^{-1}(\delta_y-\delta_x),C))\), where \(\delta_z\) is unit mass at \(z\).
Define per-capita social cost \(S_\mu(a,b)=\sum_x\mu_xd_x(a,b)\) and \(\operatorname{OPT}(\mu,C)=\min_{a,b\in C,\,a\ne b}S_\mu(a,b)\).
Let \(\mathcal E_n\) contain all finitely encoded pairs \((\mu,C)\) satisfying these conditions, with \(\tau\le\tau_0\), and define \(R_{\tau_0}=\inf_{(M_n)\text{ admissible}}\limsup_{n\to\infty}\sup_{(\mu,C)\in\mathcal E_n}S_\mu(M_n(\mu,C))/\operatorname{OPT}(\mu,C)\).

What is the exact value of \(R_{\tau_0}\) for each fixed \(\tau_0\ge2\)?

For finite societies, choosing the two candidates closest to the leftmost median is strategyproof and has tight worst-case social-cost ratio \(3\); every deterministic strategyproof mechanism has unrestricted worst-case ratio at least \(1+\sqrt2\). [Published source](https://repository.essex.ac.uk/39422/1/1-s2.0-S0304397524005309-main.pdf)
No result settling this precise bounded-support empirical limiting problem was located.

Modeling choices made when packaging the task

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

Status and proved results

The exact value of $R_{\tau_0}$ remains unresolved. I establish the bounds
$$ 1+\sqrt2\le R_{\tau_0}\le3 $$
and a new finite characterization of the optimization over mechanisms.

More precisely, for a fixed population size and a candidate set whose pair sums and pair gaps are all distinct, every anonymous strategyproof mechanism is represented exactly by a finite table of ordinal-type counts. Its optimal bounded-support approximation guarantee is an attained, computable rational number. A limiting argument shows that these candidate sets suffice for the worst-case optimization defining $R_{\tau_0}$.

The finite characterization preserves strategyproofness on profiles of every support size. It does not yet evaluate the resulting limiting optimization.

1. Self-contained bounds

1.1. An admissible family with ratio at most $3$

For a profile of $n$ reports, let $q$ be its $r$th order statistic, where
$$ r=\lceil n/2\rceil. $$
Let $P(t)$ be the unordered pair of candidates closest to $t$, resolving distance ties toward the smaller coordinate. The mechanism outputs $P(q)$, written in increasing order.

This mechanism is anonymous and defined on all real profiles.

To prove strategyproofness, first observe that both sorted coordinates of $P(t)$ are nondecreasing in $t$. Indeed, suppose $s<t$, a candidate $u$ leaves the selected pair, and a candidate $v$ enters it. Selection implies
$$ |s-u|\le |s-v|, \qquad |t-v|\le |t-u|. $$
If $u>v$, these inequalities imply
$$ s\ge\frac{u+v}{2}, \qquad t\le\frac{u+v}{2}, $$
contradicting $s<t$. Thus every departing candidate is smaller than every entering candidate, which proves the assertion.

Write $P(s)=(a_s,b_s)$ and $P(t)=(a_t,b_t)$ in increasing order. The function
$$ \Delta(z)=d_z(P(t))-d_z(P(s)) $$
is nonincreasing: each summand has the form $|z-v|-|z-u|$ with $u\le v$. Since $P(s)$ minimizes individual cost at $s$, $\Delta(s)\ge0$. Therefore every resident at $z\le s$ weakly prefers $P(s)$ to $P(t)$. Similarly, every resident at $z\ge t$ weakly prefers $P(t)$.

Fix the other reports $z_1\le\cdots\le z_{n-1}$ and put $z_0=-\infty$. The selected order statistic as a function of the remaining report is
$$ q(x)=\min\{\max\{x,z_{r-1}\},z_r\}. $$
If a deviation increases $q$, the true position satisfies $x\le q$; if it decreases $q$, the true position satisfies $x\ge q$. The preceding preference implications rule out a profitable deviation in either case. Thus the mechanism is strategyproof on all profiles.

For the approximation bound, define
$$ F(t)=\sum_x\mu_x|x-t|, \qquad D=F(q). $$
At least half the mass lies weakly on each side of $q$. The convex function $F$ consequently has a nonpositive left derivative and a nonnegative right derivative at $q$, so $q$ minimizes $F$.

For an optimal pair $O=(o_1,o_2)$,
$$ 2D\le F(o_1)+F(o_2)=\operatorname{OPT}. $$
The triangle inequality and individual optimality at $q$ give
$$ S_\mu(P(q)) \le2D+d_q(P(q)) \le2D+d_q(O). $$
Also,
$$ d_q(O) \le\sum_x\mu_x\bigl(2|q-x|+d_x(O)\bigr) =2D+\operatorname{OPT}. $$
Combining these inequalities yields
$$ S_\mu(P(q))\le4D+\operatorname{OPT}\le3\operatorname{OPT}. $$
Every denominator is positive, because $d_x(a,b)\ge|a-b|$ and the finite candidate set has positive minimum separation. Hence
$$ R_{\tau_0}\le3. $$

The mechanism can be evaluated from the support in
$$ O\!\left((\tau\log\tau+m)\operatorname{poly}(L+\log n)\right) $$
bit operations, without expanding the population into $n$ reports.

1.2. A two-support lower bound

We first record a consequence of strategyproofness. Suppose reports $u$ and $v$ induce the same strict ordering of outcome classes, with every outcome in one class strictly preferred to every outcome in a lower class. Changing one report from $u$ to $v$ cannot change the outcome class. An improvement would violate strategyproofness at $u$; a deterioration would violate it at $v$ through the reverse deviation.

Take
$$ n=2^s,\quad s\ge2,\qquad \varepsilon=n^{-2},\quad \delta=n^{-1}, $$
and
$$ C=\{-\varepsilon,\varepsilon,2-\varepsilon,2+\varepsilon\}. $$
Classify pairs as $LL$, $LR$, or $RR$ according to their cluster membership. Their costs are:

| Position | $LL$ | $LR$ | $RR$ |
|---|---:|---:|---:|
| $0$ | $2\varepsilon$ | $[2,2+2\varepsilon]$ | $4$ |
| $1-\delta$ | $2-2\delta$ | $[2-2\varepsilon,2+2\varepsilon]$ | $2+2\delta$ |
| $1+\delta$ | $2+2\delta$ | $[2-2\varepsilon,2+2\varepsilon]$ | $2-2\delta$ |
| $2$ | $4$ | $[2,2+2\varepsilon]$ | $2\varepsilon$ |

Since $\varepsilon<\delta$ and $\delta+\varepsilon<1$, the strict class ordering is $LL,LR,RR$ at both $0$ and $1-\delta$, and its reverse at both $2$ and $1+\delta$.

Put
$$ \alpha=\sqrt2-1,\qquad k=\lfloor\alpha n\rfloor,\qquad p=k/n, $$
and start with $k$ residents at $0$ and $n-k$ at $2$. Depending on the initial output, perform the indicated sequence of individual report changes:

| Initial class | Changes | Final output cost, or lower bound | Feasible comparison cost |
|---|---|---:|---:|
| $LL$ | All left residents move to $1-\delta$ | $4-2p-2p\delta$ | $2p(1+\delta)+2\varepsilon(1-p)$ |
| $RR$ | All right residents move to $1+\delta$ | $4p+2(1-p)(1-\delta)$ | $2\varepsilon p+2(1-p)(1+\delta)$ |
| $LR$ | All left residents move to $1-\delta$ | $2-2\varepsilon p$ | $2p(1+\delta)+2\varepsilon(1-p)$ |

Class preservation justifies the final output classes. The comparison pairs are respectively $RR$, $LL$, and $RR$. Their costs upper-bound the optimum, so each row gives a valid lower bound on the actual ratio.

Every final society has exactly two support points. Intermediate societies may have three; the stipulated global strategyproofness applies to them.

As $s$ tends to infinity, the three ratio bounds converge respectively to
$$ \frac2\alpha-1=1+2\sqrt2,\qquad \frac{1+\alpha}{1-\alpha}=1+\sqrt2,\qquad \frac1\alpha=1+\sqrt2. $$
Thus, for every admissible family, the supremum in the definition of $R_{\tau_0}$ has limsup at least $1+\sqrt2$. All constructed coordinates and masses are dyadic rationals, and their total encoding length is $O(\log n)$. Consequently,
$$ R_{\tau_0}\ge1+\sqrt2. $$

These numerical bounds agree with the published unrestricted bounds, but the argument above verifies the bounded-support and empirical limiting requirements directly. [Published paper](https://repository.essex.ac.uk/39422/1/1-s2.0-S0304397524005309-main.pdf)

2. Consecutive optimal pairs and an obstruction to an independent construction

2.1. A consecutive optimal pair always exists

Write the candidates as
$$ c_1<\cdots<c_m. $$
The function $F(t)=\sum_x\mu_x|x-t|$ is convex, and the cost of a pair is $F(a)+F(b)$.

Suppose an optimal pair is $(c_i,c_j)$ with $j-i>1$, and choose $i<k<j$. Convexity gives
$$ F(c_k)\le\max\{F(c_i),F(c_j)\}. $$
Replacing the endpoint with the larger $F$ value by $c_k$ does not increase the pair cost and strictly decreases its index separation. Repeating this operation produces an optimal consecutive pair.

Therefore, if candidates are partitioned alternately into
$$ C_{\mathrm{o}}=\{c_1,c_3,\ldots\}, \qquad C_{\mathrm{e}}=\{c_2,c_4,\ldots\}, $$
then
$$ \operatorname{OPT}(\mu,C) = \min_{a\in C_{\mathrm{o}}}F(a) + \min_{b\in C_{\mathrm{e}}}F(b). $$
Indeed, the right side minimizes over a subset of feasible pairs, and that subset contains a consecutive optimal pair.

2.2. Different quantiles in the two sets can still approach ratio $3$

Selecting the nearest site in each fixed candidate set to a fixed order statistic is individually strategyproof. This follows from the clipping argument in Section 1, applied to a single nearest-candidate map. Summing the two strategyproof cost inequalities proves strategyproofness of their independent combination. The disjoint candidate sets ensure distinct facilities.

Nevertheless, this construction does not automatically improve the approximation bound.

For any fixed $\alpha\in(0,1/2)$, consider selecting the nearest odd-indexed candidate to the lower $\alpha$ order statistic and the nearest even-indexed candidate to the upper $1-\alpha$ order statistic. For sufficiently large even $n$, take
$$ C=\{0,1,2,3\}, \qquad \mu=\tfrac12\delta_{1-\eta}+\tfrac12\delta_{2+\eta}, \qquad 0<\eta<\tfrac12. $$
The selected pair is $(0,3)$, with social cost $3$. The optimal pair $(1,2)$ has cost $1+2\eta$. Hence the ratio is
$$ \frac3{1+2\eta}\longrightarrow3. $$
The reverse assignment of the two quantiles has the same obstruction on
$$ C=\{0,1,2,3,4\}, \qquad \mu=\tfrac12\delta_{2-\eta}+\tfrac12\delta_{3+\eta}, $$
where its output is $(1,4)$ and the optimal pair is $(2,3)$.

Thus preserving the optimum through a fixed partition does not by itself yield a matching mechanism.

3. Pairwise preferences have a single crossing

Let $\mathcal A(C)$ be the set of unordered feasible pairs, and put
$$ K=|\mathcal A(C)|=\binom m2. $$
For $A=(a,b)$ with $a<b$, define
$$ u_A=a+b,\qquad w_A=b-a. $$
A direct calculation gives
$$ d_x(A)=\max\{|2x-u_A|,w_A\}. $$

Call $C$ generic if the $K$ pair sums $u_A$ are all distinct and the $K$ pair gaps $w_A$ are all distinct.

Single-crossing lemma

Suppose $u_A<u_B$ and $w_A\ne w_B$. There is exactly one position $t_{AB}$ at which the costs coincide, with
$$ d_x(A)<d_x(B)\quad\text{for }x<t_{AB}, $$
and
$$ d_x(B)<d_x(A)\quad\text{for }x>t_{AB}. $$
Explicitly,
$$ t_{AB}= \begin{cases} \displaystyle \max\left\{\frac{u_A+u_B}{4},\frac{u_A+w_B}{2}\right\}, & w_B>w_A,\\[6pt] \displaystyle \min\left\{\frac{u_A+u_B}{4},\frac{u_B-w_A}{2}\right\}, & w_A>w_B. \end{cases} $$

Proof. Set
$$ h=\frac{u_B-u_A}{2}, \qquad t_0=\frac{u_A+u_B}{4}. $$
First suppose $w_B>w_A$.

For $x<t_0$,
$$ |2x-u_A|<|2x-u_B|. $$
Together with $w_A<w_B$, this implies $d_x(A)<d_x(B)$.

If $w_B\le h$, then at $t_0$ both costs equal $h$. For $x>t_0$,
$$ |2x-u_A|>|2x-u_B|, \qquad |2x-u_A|>h\ge w_B, $$
so $d_x(A)>d_x(B)$. The unique crossing is $t_0$.

If $w_B>h$, put
$$ t=\frac{u_A+w_B}{2}>t_0. $$
At this point,
$$ |2t-u_A|=w_B, \qquad |2t-u_B|=|w_B-2h|\le w_B, $$
so both costs equal $w_B$. For $t_0<x<t$, both $|2x-u_A|$ and $w_A$ are smaller than $w_B$, giving $d_x(A)<d_x(B)$. For $x>t$, $|2x-u_A|$ exceeds both $w_B$ and $|2x-u_B|$, giving the reverse strict inequality.

This proves the first formula. Reflecting positions through the origin and exchanging $A,B$ gives the second formula. $\square$

In particular, on a generic candidate set every pair of outcomes has exactly one indifference position. For rational candidates, all these positions are rational.

4. Exact finite representation of strategyproof mechanisms

Fix $n$ and a generic encoded candidate set $C$.

Form a breakpoint set consisting of all candidate coordinates and all positions $t_{AB}$. Write its distinct elements as
$$ b_1<\cdots<b_B. $$
Partition the real line into its singleton breakpoints and intervening open intervals:
$$ (-\infty,b_1),\{b_1\},(b_1,b_2),\ldots,\{b_B\},(b_B,\infty). $$
Call these sets $I_1,\ldots,I_T$, where
$$ B\le m+\binom K2, \qquad T=2B+1=O(m^4). $$

Every open type has a constant strict ordering of all outcomes, by the single-crossing lemma. Every singleton type has its fixed weak ordering. Including candidate coordinates also ensures that every individual cost function is affine on each open type.

Choose a rational representative $r_t\in I_t$ for every type. For a profile, let $N_t$ be its number of residents in type $I_t$. The possible count vectors form the finite set
$$ \mathcal N_{n,T} = \left\{N\in\mathbb Z_{\ge0}^T:\sum_{t=1}^T N_t=n\right\}, $$
of size
$$ H=\binom{n+T-1}{T-1}. $$

4.1. Every anonymous strategyproof mechanism induces a count table

We identify an outcome with its unordered pair; sorting the pair changes neither costs nor strategyproofness.

Fix all reports except one, and let $x,y$ belong to the same open type. Their strict outcome rankings coincide. If changing the report from $x$ to $y$ changed the unordered output, one of these two positions would strictly prefer the other output. Either the forward or reverse deviation would then violate strategyproofness.

Thus changing a report within an open type leaves the unordered output unchanged. Singleton types contain only one possible report.

Replace reports, one at a time, by their type representatives. The output remains unchanged throughout. Anonymity then implies that the mechanism is represented by a table
$$ f:\mathcal N_{n,T}\longrightarrow\mathcal A(C). $$

This argument uses strategyproofness on every intermediate profile, without a support restriction.

4.2. The exact finite strategyproofness constraints

A table $f$ defines a strategyproof mechanism on all real profiles if and only if, for every count vector $N$, every $t$ with $N_t>0$, and every type $u$,
$$ d_{r_t}(f(N)) \le d_{r_t}\bigl(f(N-e_t+e_u)\bigr). $$
Here $e_t$ is the $t$th unit vector.

Necessity follows by applying strategyproofness to profiles at the representatives.

For sufficiency, consider a true position $x\in I_t$ and a report $y\in I_u$. Their count vectors differ by $-e_t+e_u$. The weak ordering of outcomes at $x$ is exactly the ordering at $r_t$, so the displayed inequality also holds with $x$ replacing $r_t$. This is the required strategyproofness inequality.

Consequently, full strategyproofness is characterized by a finite collection of constraints over all $H$ count vectors. Restricting these constraints to count vectors with at most $\tau_0$ occupied types would not suffice.

5. Exact computation of a table’s bounded-support guarantee

For a count vector $N$, let
$$ J(N)=\{t:N_t>0\}. $$
Define
$$ W_{\tau_0}(f,C) = \max_{\substack{N\in\mathcal N_{n,T}\\ |J(N)|\le\tau_0}} \ \max_{O\in\mathcal A(C)} \ \sup_{z_t\in I_t,\ t\in J(N)} \frac{\sum_{t\in J(N)}N_t d_{z_t}(f(N))} {\sum_{t\in J(N)}N_t d_{z_t}(O)}. $$
The factor $n^{-1}$ cancels. Taking the maximum over $O$ is equivalent to dividing by the minimum feasible social cost.

5.1. One occupied position per type suffices

Suppose a society has several occupied positions within an open type $I_t$. Let $z_t$ be their multiplicity-weighted average. This average remains in $I_t$. Because every $d_x(A)$ is affine on that interval,
$$ \sum_{x\in I_t}k_xd_x(A)=N_t d_{z_t}(A) $$
for every outcome $A$.

Replacing all these residents by residents at $z_t$ therefore preserves every pair’s social cost and preserves the count vector, hence the mechanism’s output. Singleton types need no replacement.

It follows that every society with support at most $\tau_0$ can be compressed to at most one position per occupied type without changing its ratio. Conversely, every configuration in the definition of $W_{\tau_0}$ has support at most $\tau_0$.

Encoded positions suffice for the same supremum: representatives and finite endpoints are rational, and positions in open intervals can be approximated by encoded rational positions within the same types. Costs are continuous and denominators remain positive.

Thus $W_{\tau_0}(f,C)$ is exactly the worst-case guarantee on the task’s encoded societies for this fixed $n,C$.

5.2. Only endpoint evaluations are required

Fix $N$ and $O$. On the product of the occupied types, numerator and denominator are affine functions of the positions $z_t$. The denominator is positive everywhere, including finite boundary points, since
$$ \sum_tN_t d_{z_t}(O)\ge n\,|o_1-o_2|>0. $$

For a bounded closed box, write any point as a convex combination of vertices. If $U,V$ are the affine numerator and denominator, then
$$ \frac{U(z)}{V(z)} = \sum_v \frac{\lambda_vV(v)}{\sum_{v'}\lambda_{v'}V(v')} \frac{U(v)}{V(v)}. $$
The coefficients are nonnegative and sum to one. Hence the maximum occurs at a vertex.

Using interval closures is legitimate for a supremum: approach each endpoint from within its original type while keeping the table output fixed.

For an unbounded interval, any position tending to infinity makes the ratio tend to $1$. Indeed, for any two outcomes $A,O$,
$$ |d_x(A)-d_x(O)| \le |a_1-o_1|+|a_2-o_2|, $$
so the difference of numerator and denominator is uniformly bounded, whereas the denominator tends to infinity. Truncating the unbounded intervals and applying the bounded-box result therefore reduces the supremum to finite endpoint evaluations and the value $1$.

There are at most $2^{|J(N)|}$ finite endpoint combinations. All associated ratios are rational. Therefore $W_{\tau_0}(f,C)$ is an exactly computable rational number.

5.3. The fixed-candidate optimum is attained

Let $\mathscr S_n(C)$ be the finite set of tables satisfying the constraints of Section 4. It is nonempty because the median mechanism induces such a table.

For generic $C$, the optimal guarantee among all anonymous deterministic strategyproof mechanisms is exactly
$$ \Gamma_{n,\tau_0}(C) = \min_{f\in\mathscr S_n(C)}W_{\tau_0}(f,C). $$
The minimum is attained and rational.

A coarse exhaustive-search bound can be stated entirely in the prescribed input parameters. Put
$$ \ell=\lceil\log_2(n+1)\rceil, \qquad Q=2^{T\ell}. $$
Since $H\le(n+1)^T\le Q$, enumerating all tables, checking strategyproofness, and evaluating their guarantees takes at most
$$ K^Q\,Q\, \bigl(T^2+K\tau_0 2^{\tau_0}\bigr) \operatorname{poly}(L+\ell+m+\tau_0) $$
bit operations, with $K=O(m^2)$ and $T=O(m^4)$.

This bound is deliberately coarse and extremely large. The mechanism class imposes no efficiency restriction.

6. Generic candidate sets suffice for the global optimization

For an arbitrary encoded candidate set $C$, let $\Gamma_{n,\tau_0}(C)$ denote the infimum of the fixed-candidate guarantee over anonymous deterministic mechanisms strategyproof on all real profiles.

Generic rational candidate sets are dense among candidate sets with $m$ distinct ordered sites. The nongeneric conditions are finitely many nontrivial linear equations equating two pair sums or two pair gaps. Their union has empty interior, and rational points are dense in its open complement.

We now prove the inequality
$$ \Gamma_{n,\tau_0}(C) \le \liminf_{j\to\infty}\Gamma_{n,\tau_0}(C_j) $$
whenever generic encoded sets $C_j$ of the same cardinality converge coordinatewise to $C$.

6.1. Constructing a limiting strategyproof mechanism

Pass to a subsequence along which the right-hand guarantees converge to their liminf. For each $C_j$, choose an optimal finite table and its corresponding mechanism $M_j$.

The number of breakpoints is uniformly bounded by $m+\binom K2$. Pass to a subsequence with a constant breakpoint count $B$. Every breakpoint lies in the candidate span: outside that span, two pair costs differ by their distinct pair sums and cannot coincide. Thus the sorted breakpoints are uniformly bounded. Pass to a further subsequence on which each sorted breakpoint converges.

Let $Z$ be the finite set of their limits. At each $z\in Z$, the type index of $z$ has finitely many possibilities. Another subsequence makes all these indices constant. For every $x\notin Z$, its type index is eventually constant because each breakpoint converges to a point different from $x$.

Therefore, along this subsequence, every real position has an eventually constant type index.

Label candidate pairs by their two indices in the ordered candidate set. The population size, type count, and pair-label set are now fixed. There are only finitely many tables, so one further subsequence has a constant table.

For every real profile $P$, the output pair indices of $M_j(P)$ consequently stabilize. Define $M(P)$ to use those indices in $C$. This mechanism is anonymous and deterministic.

Fix any real profile, any resident’s true position $x$, and any real deviation. The relevant two outputs eventually stabilize in pair indices. Taking limits in the strategyproofness inequalities for $M_j$ gives
$$ d_x(M(P))\le d_x(M(P')). $$
Thus $M$ is strategyproof on all real profiles.

For every fixed encoded profile of support at most $\tau_0$, take limits in its approximation inequalities. Pair costs are continuous in candidate coordinates, and the optimum is the minimum of finitely many continuous pair-cost functions, hence is continuous. This proves the claimed inequality for $\Gamma$.

6.2. Removing nongeneric sets from the supremum

For fixed $n$, the preceding inequality gives
$$ \sup_{C\text{ encoded}}\Gamma_{n,\tau_0}(C) = \sup_{C\text{ generic and encoded}}\Gamma_{n,\tau_0}(C). $$
The inequality from right to left is immediate. For the reverse inequality, approximate any nongeneric $C$ by generic encoded sets and apply Section 6.1. This argument applies separately for every candidate-set cardinality.

7. The resulting characterization of $R_{\tau_0}$

Define
$$ \beta_{n,\tau_0} = \inf_{M_n} \sup_{(\mu,C)\in\mathcal E_n} \frac{S_\mu(M_n(\mu,C))} {\operatorname{OPT}(\mu,C)}, $$
where the infimum requires anonymity and strategyproofness on all real profiles and candidate sets.

Because the candidate set is public, mechanisms for different fixed candidate sets can be selected independently. Hence
$$ \beta_{n,\tau_0} = \sup_{C\text{ encoded}}\Gamma_{n,\tau_0}(C). $$
For completeness, every mechanism’s uniform guarantee is at least the right-hand side. Conversely, for any $\epsilon>0$, choose for each encoded $C$ a fixed-candidate mechanism within $\epsilon$ of its infimum. Assemble these into one mechanism; on other candidate sets, use a constant feasible outcome. Strategyproofness is checked separately for each public candidate set, so the assembled mechanism is admissible.

The population sizes can likewise be optimized independently:
$$ R_{\tau_0}=\limsup_{n\to\infty}\beta_{n,\tau_0}. $$
One direction follows because every family has its $n$th guarantee at least $\beta_{n,\tau_0}$. For the other, choose an admissible $M_n$ with guarantee at most $\beta_{n,\tau_0}+1/n$ for each $n$.

Combining Sections 4–6 gives the exact characterization
$$ R_{\tau_0} = \limsup_{n\to\infty} \sup_{\substack{m\ge2\\ C\text{ generic and encoded}}} \min_{f\in\mathscr S_n(C)} W_{\tau_0}(f,C). $$

This formula eliminates the unrestricted search over functions on real profiles in favor of finite strategyproof count tables. It also separates the support restriction in the objective from the unrestricted strategyproofness constraints.

8. What remains open

The finite optimization above has not been evaluated uniformly over candidate sets and population sizes. In particular, it does not establish whether its limiting value is $1+\sqrt2$, $3$, or an intermediate number, nor whether that value depends on $\tau_0$.

A complete solution still requires a matching admissible guarantee and lower bound. The consecutive-pair reduction alone does not supply such a guarantee, as the independent-quantile examples demonstrate.

⟨structured verdict parsed — rendered above⟩

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

Assessment: partial, with substantial valid progress. The write-up establishes
$$ 1+\sqrt2\le R_{\tau_0}\le3 $$
for every fixed $\tau_0\ge2$, and its finite-table characterization is sound. It explicitly leaves the requested exact value unresolved. I found no false central step or additional blocking gap in the supporting arguments.

1. Median mechanism and upper bound — verified.

The mechanism chooses two distinct candidates, is anonymous, and has a specified deterministic tie rule.

The monotonicity argument is valid: for any departing candidate $u$ and entering candidate $v$, the two selection inequalities contradict $s<t$ if $u>v$. Consequently, both coordinates of the sorted selected pair are nondecreasing.

For $u\le v$, the function $|z-v|-|z-u|$ is nonincreasing. Thus the asserted monotonicity of $\Delta$ and its preference implications follow. Individual optimality supplies $\Delta(s)\ge0$ and $\Delta(t)\le0$.

The order-statistic clipping formula is well-defined for every $n\ge2$: with $r=\lceil n/2\rceil$, one has $1\le r\le n-1$. When a deviation increases the selected statistic, the true position lies weakly below its original value; the reverse statement holds when it decreases. These are precisely the hypotheses needed for the preceding preference implications. Strategyproofness therefore holds on all real profiles, without a support restriction.

The weighted median minimizes $F$, including the even-population case. The approximation inequalities are correct:
$$ 2D\le\operatorname{OPT}, \qquad S_\mu(P(q))\le2D+d_q(O), \qquad d_q(O)\le2D+\operatorname{OPT}. $$
They imply the claimed factor $3$. Positive candidate separation ensures that every approximation ratio is defined.

The evaluation time is consistent with sorting the support, finding the weighted median, and scanning the candidates for the two nearest sites. It does not require expanding the population.

2. Two-support lower bound — verified.

The class-preservation observation correctly uses strategyproofness in both directions. If the output moves to a better class, the forward deviation is profitable; if it moves to a worse class, the reverse deviation is profitable. Preferences within a class need not coincide.

All entries in the individual-cost table are correct. In particular, at the two interior positions, mixed pairs have costs in
$$ [2-2\varepsilon,2+2\varepsilon]. $$
The inequalities $\varepsilon<\delta$ and $\delta+\varepsilon<1$ ensure the stated strict class rankings.

The three final output-cost bounds and comparison costs also check out:

The comparison pairs are feasible, so their costs upper-bound the optimum. The resulting ratios are valid lower bounds, even without proving that those comparison pairs are optimal.

The limiting calculations are correct:
$$ \frac2\alpha-1=1+2\sqrt2, \qquad \frac{1+\alpha}{1-\alpha}=1+\sqrt2, \qquad \frac1\alpha=1+\sqrt2. $$
Although the initial output class can vary with $n$, the minimum of the three row bounds converges to $1+\sqrt2$. Hence the subsequence $n=2^s$ suffices for the claimed limsup lower bound for every admissible family.

Both final masses are positive, and every final society has exactly two support points. Intermediate profiles can have three support points; invoking global strategyproofness there is authorized by the task. The coordinates and masses are dyadic rationals with the claimed encoding length.

The numerical comparison with the unrestricted published bounds is also accurate. Those bounds appear in the doubleton social-cost results of the [cited paper](https://repository.essex.ac.uk/39422/1/1-s2.0-S0304397524005309-main.pdf). The write-up’s bounded-support lower bound stands independently of that citation.

3. Consecutive optimal pairs and quantile examples — verified.

Convexity gives
$$ F(c_k)\le\max\{F(c_i),F(c_j)\}. $$
Replacing an endpoint attaining the larger value preserves optimality and strictly decreases index separation. The iteration terminates at a consecutive optimal pair.

Every consecutive pair uses one odd-indexed and one even-indexed candidate. Therefore the alternating-partition identity for $\operatorname{OPT}$ follows: the restricted feasible set contains an optimal pair, and its objective separates into the two displayed minima.

The independent combination is strategyproof because each component satisfies its own individual-distance strategyproofness inequality, and these inequalities add. The fixed partition ensures distinct facilities.

Both obstruction examples have the stated outputs and optimal pairs. In the first, the output cost is $3$ and the optimal cost is $1+2\eta$. The reverse-assignment example has the same costs. These examples refute an automatic improvement for the specified independent-quantile constructions; the write-up does not incorrectly extend them to all mechanisms.

4. Single-crossing lemma — verified.

The identity
$$ d_x(A)=\max\{|2x-u_A|,w_A\} $$
is correct.

For $w_B>w_A$, the proof correctly separates the cases $w_B\le h$ and $w_B>h$. In the latter case, the equality at the proposed crossing follows from
$$ |w_B-2h|\le w_B, $$
which holds because $w_B>h>0$. The strict inequalities on both sides follow from the comparisons stated in the proof.

Reflection and exchange of the two outcomes correctly produce the second formula. The hypotheses of distinct pair sums and distinct pair gaps exclude the degeneracies that could prevent a unique crossing.

For rational candidates, the formulas give rational crossing positions. Several crossings may coincide with each other or with candidate coordinates; taking distinct breakpoints correctly handles this.

5. Finite representation and strategyproofness constraints — verified.

Including all crossings ensures a constant strict outcome ranking on every open type. Including candidate coordinates ensures that each individual-cost function is affine there. Singleton types correctly retain their weak rankings.

Within an open type, changing a report cannot change the unordered output: distinct outputs are strictly ranked identically at both positions, so one direction would violate strategyproofness. Sequential replacement by representatives is therefore valid. Anonymity then gives a table depending only on type counts.

The passage to unordered outcomes is legitimate for this task because facility order does not affect costs, feasibility, or strategyproofness.

The count-vector number
$$ H=\binom{n+T-1}{T-1} $$
is correct. The stated representative inequalities are necessary, and they are sufficient because every true position in a type has exactly the representative’s weak ordering.

Crucially, the constraints range over all count vectors. The write-up preserves strategyproofness on profiles whose support exceeds $\tau_0$.

6. Exact guarantee computation and attainment — verified.

The within-type compression preserves all outcome costs because of affineness, and preserves the mechanism’s output because type counts remain unchanged. Multiplicity-weighted averages remain inside their open intervals. For encoded societies, these averages are rational.

Conversely, each configuration in the definition of $W_{\tau_0}$ has at most $\tau_0$ support points. Rational approximation within the same types preserves the output and approaches the ratio continuously. Thus the encoded-domain supremum is correctly represented.

The maximum over comparison outcomes is valid: for a fixed positive numerator, maximizing its ratio to a feasible outcome’s cost is equivalent to dividing by the minimum feasible cost.

The linear-fractional vertex argument is correct because its denominator is positive throughout each closed box. Endpoint evaluation keeps the original table output fixed and approaches boundaries from the original types, so it does not mistakenly substitute a neighboring type’s output.

For unbounded coordinates, the numerator–denominator difference is uniformly bounded, while the denominator diverges. Hence the limiting ratio is $1$, including when several coordinates diverge. Finite endpoint values together with this limit suffice.

All finite endpoint ratios are rational. Since the strategyproof table set is finite and nonempty, the fixed-generic-candidate optimum is attained and rational.

The exhaustive-search bound is consistent with the number of tables, strategyproofness constraints, comparison outcomes, and endpoint combinations. It establishes computability for fixed encoded generic candidates; it does not establish efficient computation of the global limiting quantity.

7. Passage to nongeneric candidates — verified.

The density argument is valid: the excluded equalities are finitely many nontrivial linear conditions in candidate coordinates.

For the limiting construction, the population size and candidate cardinality remain fixed. Generic crossings lie within the candidate span, so the breakpoint sequences are bounded. A subsequence can fix their number and make every ordered breakpoint converge.

The additional extraction at the finite set $Z$ correctly addresses positions equal to breakpoint limits. Positions outside $Z$ have eventually constant type indices. A further subsequence fixes the finite count table.

Consequently, output pair indices stabilize for every fixed real profile. Taking limits preserves anonymity, feasibility, and every strategyproofness inequality. This does not require a uniform stabilization time over all profiles.

For each fixed encoded society, continuity of candidate-dependent pair costs and of the finite minimum defining the optimum preserves the approximation guarantee. The claimed inequality
$$ \Gamma_{n,\tau_0}(C) \le \liminf_j\Gamma_{n,\tau_0}(C_j) $$
therefore follows. Its direction is sufficient to remove nongeneric sets from the global supremum.

8. Global characterization — verified, but unevaluated.

Mechanisms can be selected independently for each public candidate set because strategyproofness compares reports with that candidate set held fixed. Extending the assembled mechanism by a constant feasible outcome on other candidate sets is admissible.

Likewise, independent selection for each population size justifies
$$ R_{\tau_0}=\limsup_{n\to\infty}\beta_{n,\tau_0}. $$
The near-optimal selections are available because the infima are finite, as ensured by the median upper bound.

Thus the final finite-table characterization is established. It remains a supremum over candidate sets and a limiting optimization over population sizes.

9. Blocking issue and actionable feedback.

Major — the exact-value task remains unresolved. Sections 7–8 do not evaluate the characterized quantity, close the interval between $1+\sqrt2$ and $3$, or determine dependence on $\tau_0$.

This is an acknowledged limitation, rather than a false assertion of completion. No expositional clarification alone repairs it. To resolve USER_TASK, the prover must provide an exact value for each fixed $\tau_0\ge2$ and establish it through matching admissible upper and lower bounds, or rigorously evaluate the displayed limiting optimization to that value.

The existing bounds and characterization are genuine progress and merit retention.

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