← back to the atlas

Positive Intra-Group Externalities in Facility Location (aamas24-00212)

Answer: $\rho^*=3/2$. A deterministic unanimous, location-strategyproof mechanism attains this ratio on the stated compressed integral-clone domain, so the $\sqrt3$ guarantee can be improved and $3/2$ is optimal.

The anchor (named result in the paper)

Theorem 1 — class: algorithmic

The continuous mirror question, as graded

Given \(N\in\mathbb{N}\), rational public coefficients \(\alpha_g\), and rational finite-support masses \(\mu_{g,x}\) with \(N\mu_{g,x}\in\mathbb{Z}_{\ge 0}\) and \(\sum_{g,x}\mu_{g,x}=1\), compute the RGA-M facility \(F_N(\mu)\) using weighted group medians, weights \(c_g=\mu_g(1+\alpha_g(N\mu_g-1))\), and \(\lambda=2\sqrt{3}-3\), together with \(\max_{z\in[0,1]}SU_N(z;\mu)\) and the achieved ratio, where \(SU_N(y;\mu)=\sum_g[1+\alpha_g(N\mu_g-1)]\sum_x\mu_{g,x}(1-|y-x|)\). Prove uniformly that \(F_N\) is unanimous, no one-clone location report \(\mu\mapsto\mu+N^{-1}(e_{g,x'}-e_{g,x})\) improves the true type's utility, and the ratio is at most \(\sqrt{3}\); the design variant asks for the smallest achievable \(\rho\).

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

A society is given by its support: the list of the \(\tau\) types \((g,x)\) with positive mass, each mass a binary rational; \(\tau\) is the support size, not the number of possible types. Locations are rational \(x\in[0,1]\), groups \(g\in\{1,\ldots,m\}\) are public and nonempty, and public coefficients satisfy \(\alpha_g\in[0,1]\cap\mathbb Q\).
The input includes a binary integer \(N\ge1\), with \(N\mu_{g,x}\in\mathbb Z_{\ge0}\) and \(\sum_{g,x}\mu_{g,x}=1\); put \(\mu_g=\sum_x\mu_{g,x}\). State algorithmic running times in \(m,\tau,L,\log N\), where \(L\) is the total input bit length.
The true utility of one clone of type \((g,x)\) at facility \(y\in[0,1]\) is \(U_{g,x}(y;\mu)=(1-\alpha_g)(1-|y-x|)+\alpha_gN\sum_t\mu_{g,t}(1-|y-t|)\).
A deterministic mechanism family \(f_{N,\alpha}\) is unanimous if it outputs \(x\) whenever all mass is at \(x\), and location-strategyproof if \(U_{g,x}(f_{N,\alpha}(\mu);\mu)\ge U_{g,x}(f_{N,\alpha}(\mu');\mu)\) for every occupied type and rational report \(x'\in[0,1]\), where \(\mu'=\mu+N^{-1}(e_{g,x'}-e_{g,x})\) and \(e_{g,t}\) denotes unit mass at \((g,t)\).
Define \(SU_N(y;\mu)=\sum_g[1+\alpha_g(N\mu_g-1)]\sum_x\mu_{g,x}(1-|y-x|)\), and \(\rho(f)=\sup_{N,m,\alpha,\mu}\max_{z\in[0,1]}SU_N(z;\mu)/SU_N(f_{N,\alpha}(\mu);\mu)\), taking a zero denominator as infinite.
For comparison, RGA-M uses lower group medians \(q_g=\min\{t:\sum_{x\le t}\mu_{g,x}\ge\mu_g/2\}\), weights \(c_g=\mu_g[1+\alpha_g(N\mu_g-1)]\), and \(\lambda=2\sqrt3-3\).
Write \(C=\sum_gc_g\), \(B=\sum_{q_g\le1/2}c_g\), and \(Q(a)=\min\{t:\sum_{q_g\le t}c_g\ge a\}\). Its output is \(Q((1+\lambda)C/2)\) if \(B>(1+\lambda)C/2\), \(1/2\) if \((1-\lambda)C/2\le B\le(1+\lambda)C/2\), and \(Q((1-\lambda)C/2)\) otherwise.

What is \(\rho^*=\inf_f\rho(f)\) over deterministic unanimous, location-strategyproof mechanism families on this domain: can the \(\sqrt3\) guarantee be improved, or is it optimal?

For finite societies, RGA-M is unanimous and location-strategyproof with approximation ratio at most \(\sqrt3\); every deterministic unanimous, location-strategyproof mechanism has worst-case ratio at least \(3/2\). [Source](https://ifmas.csc.liv.ac.uk/Proceedings/aamas2024/pdfs/p1883.pdf)
These bounds also cover the stated integral-clone mass domain; the optimal ratio between them remains unresolved in the verified sources. The expanded treatment retains the same bounds. [Source](https://lbms03.cityu.edu.hk/theses/c_ftt/phd-cs-194502506.pdf)

Modeling choices made when packaging the task

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

Result

The optimal ratio on the stated domain is
$$ \boxed{\rho^*=\frac32}. $$

Thus the $\sqrt3$ guarantee can be improved. The construction below replaces RGA-M’s two fixed quantile thresholds by a continuously varying threshold. It closes the gap between the bounds stated in the [AAMAS paper](https://ifmas.csc.liv.ac.uk/Proceedings/aamas2024/pdfs/p1883.pdf) and its [expanded treatment](https://lbms03.cityu.edu.hk/theses/c_ftt/phd-cs-194502506.pdf).

The proof is self-contained: it establishes unanimity, individual location-strategyproofness, the $3/2$ welfare guarantee, and the matching universal lower bound.

1. Counts, weights, and group medians

Write
$$ n_{g,x}=N\mu_{g,x}, \qquad n_g=\sum_xn_{g,x}, \qquad \beta_g=1+\alpha_g(n_g-1). $$

Every $n_g$ is a positive integer, so $\beta_g\ge1$. Define
$$ c_g=\mu_g\beta_g, \qquad C=\sum_gc_g, \qquad w_g=\frac{c_g}{C}. $$
These weights are positive and sum to one. Crucially, they remain unchanged by a location report, because such a report preserves all group sizes.

Let $P_g$ be the conditional location distribution within group $g$:
$$ P_g(\{x\})=\frac{n_{g,x}}{n_g}. $$
Then normalized social utility is
$$ W(y)=\frac{SU_N(y;\mu)}{C} =\sum_gw_g\int(1-|y-t|)\,dP_g(t). $$
Normalization preserves approximation ratios.

The lower group median $q_g$ satisfies
$$ P_g([0,q_g])\ge\frac12, \qquad P_g([q_g,1])\ge\frac12. $$
Indeed, the mass strictly below the first support point reaching half the group mass is less than half.

For later use, put
$$ S_g(y)=\sum_tn_{g,t}(1-|y-t|). $$
The individual utility in the question is exactly
$$ U_{g,x}(y;\mu) =(1-\alpha_g)(1-|y-x|)+\alpha_gS_g(y). $$

The median inequalities imply that $S_g$ is nondecreasing on $[0,q_g]$ and nonincreasing on $[q_g,1]$. For example, if $q_g\le u\le v$, every clone at or below $q_g$ loses exactly $v-u$ when the facility moves from $u$ to $v$, while every remaining clone gains at most $v-u$. Since at least half the clones are at or below $q_g$,
$$ S_g(v)-S_g(u)\le0. $$
The argument on the left of $q_g$ is symmetric.

2. The mechanism

Define, for $p\in[0,1]$,
$$ R(p)=1+2p-2p^2, \qquad F(p)=\frac{1-p^2}{1+2p-2p^2}. $$

The denominator is positive, and
$$ 1\le R(p)\le\frac32. $$
Moreover,
$$ F(0)=1, \qquad F(1)=0, \qquad F'(p)= -\frac{2(p^2-p+1)}{(1+2p-2p^2)^2}<0. $$
Thus $F$ is a continuous, strictly decreasing bijection from $[0,1]$ onto $[0,1]$. Write $H=F^{-1}$.

Sort the group medians, retaining their weights:
$$ q_{(1)}\le\cdots\le q_{(m)}, \qquad p_i=\sum_{j=1}^iw_{(j)}. $$

Define the mechanism by
$$ \boxed{ f_{N,\alpha}^{\star}(\mu) = \min_{1\le i\le m} \max\{q_{(i)},F(p_i)\}. } $$

Equal medians may be ordered arbitrarily. Within a block of equal medians, $p_i$ increases and $F(p_i)$ decreases, so only the last index of the block can improve the displayed minimum.

Although $H$ is useful for the proof, the mechanism evaluates only $F$ at rational numbers. Its output is therefore rational.

The threshold characterization

For any $y\in[0,1]$, define
$$ A_<(y)=\sum_{q_g<y}w_g, \qquad A_\le(y)=\sum_{q_g\le y}w_g. $$

The mechanism’s output is the unique $y$ satisfying
$$ \boxed{ A_<(y)\le H(y)\le A_\le(y). } $$

To prove existence, let $y$ be the output in the explicit formula. If there are medians strictly below $y$, let $k$ be their last index. Since every candidate in the minimum is at least $y$,
$$ \max\{q_{(k)},F(p_k)\}\ge y. $$
Because $q_{(k)}<y$, this implies $F(p_k)\ge y$, hence
$$ A_<(y)=p_k\le H(y). $$
If there are no such medians, the inequality is immediate.

Next, take an index $i$ attaining the minimum. Then
$$ q_{(i)}\le y, \qquad F(p_i)\le y. $$
Consequently,
$$ A_\le(y)\ge p_i\ge H(y). $$

For uniqueness, suppose $y_1<y_2$ both satisfied the characterization. Then
$$ H(y_1) \le A_\le(y_1) \le A_<(y_2) \le H(y_2), $$
contradicting strict decrease of $H$.

This characterization includes atoms at the output and outputs at either endpoint or at the midpoint.

Unanimity

If all mass is at $x$, every group median equals $x$. Every candidate is at least $x$, and the last candidate is
$$ \max\{x,F(1)\}=x. $$
Therefore the mechanism outputs $x$.

3. Individual location-strategyproofness

We first establish two properties of the aggregation rule.

Changing one group median

Fix the weights and all other group medians. Suppose one median increases from $q$ to $q'$, with $q'>q$. Let the corresponding outputs be $y$ and $y'$.

At every location $t$, increasing that median weakly decreases cumulative median weight:
$$ A'_\le(t)\le A_\le(t). $$
If $y'<y$, the threshold characterizations would give
$$ H(y') \le A'_\le(y') \le A_\le(y') \le A_<(y) \le H(y), $$
contradicting $H(y')>H(y)$. Hence
$$ y'\ge y. $$

Furthermore, if $y<q$, both the old and new median lie strictly above $y$. Thus $A_<(y)$ and $A_\le(y)$ are unchanged. The old output still satisfies the new threshold characterization, so uniqueness implies $y'=y$.

It follows that
$$ q'>q,\quad y'>y \quad\Longrightarrow\quad y\ge q. $$

Reversing the comparison proves the corresponding statement for a decrease:
$$ q'<q,\quad y'<y \quad\Longrightarrow\quad y\le q. $$

Which clone can change its group median?

Suppose a clone at true location $x$ reports $x'$, changing its group’s lower median from $q$ to $q'$.

If $q'>q$, then necessarily $x\le q$. Otherwise, the report removes no clone at or below $q$, so the reported profile still has at least half its clones at or below $q$, forcing $q'\le q$.

If $q'<q$, then necessarily $x\ge q$. Otherwise, the report removes one clone strictly below $q$ and adds at most one there. The number strictly below $q$ cannot increase, so it remains less than half, forcing $q'\ge q$.

Comparing true utilities

A report changes only the reporting group’s median; all aggregation weights remain fixed.

If the group median is unchanged, the output is unchanged. Suppose it increases. The output weakly increases. If it increases strictly, the preceding facts give
$$ x\le q\le y\le y'. $$
Both the clone’s own proximity utility and its true group proximity sum are nonincreasing on $[q,1]$. Their coefficients $1-\alpha_g$ and $\alpha_g$ are nonnegative. Therefore
$$ U_{g,x}(y;\mu)\ge U_{g,x}(y';\mu). $$

If the group median decreases and the output changes, then
$$ y'\le y\le q\le x. $$
Both components of true utility are nondecreasing on $[0,q]$, again giving
$$ U_{g,x}(y;\mu)\ge U_{g,x}(y';\mu). $$

These cases cover every permitted report. Hence $f^\star$ is location-strategyproof.

4. The $3/2$ welfare guarantee

Fix a profile and let
$$ y=f^\star_{N,\alpha}(\mu), \qquad p=H(y), \qquad r=R(p). $$
Thus $y=F(p)$ and $1\le r\le3/2$.

We prove, for every $z\in[0,1]$,
$$ W(z)\le rW(y). $$

Splitting the median weight at the output

The threshold characterization gives
$$ A_<(y)\le p\le A_\le(y). $$

Assign all groups with median below $y$ to a left part and all groups with median above $y$ to a right part. Split the weights of groups whose median equals $y$, if necessary, so that the left part has total weight exactly $p$.

Every distribution assigned to the left part has at least half its mass in $[0,y]$. Every distribution assigned to the right part has at least half its mass in $[y,1]$. Splitting a group’s weight does not change its conditional distribution or the resulting normalized welfare distribution.

A comparison lemma

Define
$$ \phi(t)=(1-|z-t|)-r(1-|y-t|), \qquad M=\max\{\phi(0),\phi(1)\}. $$

The function $\phi$ is nonincreasing on $[0,y]$. Indeed, for $0\le s\le t\le y$, proximity to $y$ increases by exactly $t-s$, while proximity to $z$ increases by at most $t-s$. Hence
$$ \phi(t)-\phi(s)\le(1-r)(t-s)\le0. $$

Similarly, $\phi$ is nondecreasing on $[y,1]$: proximity to $y$ decreases by exactly $t-s$, and proximity to $z$ decreases by at most $t-s$, so
$$ \phi(t)-\phi(s)\ge(r-1)(t-s)\ge0. $$

Consequently, $\phi(t)\le M$ everywhere. If a probability distribution $P$ has mass $a\ge1/2$ in $[0,y]$, then
$$ \int\phi\,dP \le a\phi(0)+(1-a)M \le\frac{\phi(0)+M}{2}. $$
The last inequality uses $\phi(0)\le M$.

Likewise, if $P([y,1])\ge1/2$, then
$$ \int\phi\,dP\le\frac{\phi(1)+M}{2}. $$

Applying these bounds to the left and right parts yields
$$ W(z)-rW(y) \le \frac p2\phi(0)+\frac{1-p}{2}\phi(1)+\frac12M. $$

Set
$$ t_-=\frac p2, \qquad t_+=\frac{1+p}{2}. $$
The right-hand side is exactly
$$ \max\left\{ t_-\phi(0)+(1-t_-)\phi(1), \; t_+\phi(0)+(1-t_+)\phi(1) \right\}. $$

Thus it remains to check two endpoint distributions.

The two endpoint distributions

For a distribution with mass $t$ at $0$ and $1-t$ at $1$, its normalized welfare is
$$ W_t(v)=t(1-v)+(1-t)v. $$

Because $t_-\le1/2$ and $t_+\ge1/2$,
$$ \max_vW_{t_-}(v)=1-t_-=\frac{2-p}{2}, $$
and
$$ \max_vW_{t_+}(v)=t_+=\frac{1+p}{2}. $$

Our choice of $F$ gives the identities
$$ p+2(1-p)F(p)=\frac{2-p}{R(p)}, $$
and
$$ 1+p-2pF(p)=\frac{1+p}{R(p)}. $$
For verification, multiplying the first identity by $R(p)$ gives
$$ p(1+2p-2p^2)+2(1-p)(1-p^2)=2-p, $$
and multiplying the second gives
$$ (1+p)(1+2p-2p^2)-2p(1-p^2)=1+p. $$

Since $y=F(p)$ and $r=R(p)$, these identities imply
$$ rW_{t_-}(y)=\max_vW_{t_-}(v), \qquad rW_{t_+}(y)=\max_vW_{t_+}(v). $$

Therefore, for either $t=t_-$ or $t=t_+$,
$$ t\phi(0)+(1-t)\phi(1) = W_t(z)-rW_t(y) \le0. $$
The comparison lemma now gives
$$ W(z)\le rW(y)\le\frac32W(y). $$

There is no zero-denominator exception: every location has proximity at least $1/2$ to the midpoint, so $W(1/2)\ge1/2$. The proved inequality consequently implies
$$ W(y)\ge\frac13. $$

We have established
$$ \rho(f^\star)\le\frac32. $$

The ratio is attained by a small admissible example: take $N=4$, two groups of size two, and $\alpha_1=\alpha_2=0$. Put group $1$’s clones at $0$ and $1$, and both group $2$ clones at $1$. The medians are $0$ and $1$ with equal weights, so the mechanism outputs $F(1/2)=1/2$. Optimal social utility is $3/4$, while the output gives $1/2$, producing ratio $3/2$.

5. Universal lower bound

For completeness, we prove that every location-strategyproof mechanism family has ratio at least $3/2$. Unanimity is unnecessary for this argument.

Choose
$$ n=2^s\ge4, \qquad N=2n, \qquad k=\frac n2-1. $$
There are two groups, each containing $n$ clones, with
$$ \alpha_1=\alpha_2=1. $$

Initially, group $1$ is entirely at $0$ and group $2$ entirely at $1$. Let the mechanism output $y_0$.

Case 1: $y_0\ge1/2$

For $j=0,\ldots,k$, move $j$ group-$2$ clones from $1$ to $0$, and denote the resulting output by $y_j$.

At profile $j$, every group-$2$ clone has true utility
$$ U_2(y)=j(1-y)+(n-j)y=j+(n-2j)y. $$

For each $j\ge1$, an occupied group-$2$ clone at $0$ can report $1$, recovering profile $j-1$. Strategyproofness gives
$$ j+(n-2j)y_j \ge j+(n-2j)y_{j-1}. $$
Since $n-2j>0$ throughout the chain,
$$ y_j\ge y_{j-1}. $$
In particular, $y_k\ge1/2$.

The groups have equal welfare weights. At the final profile, the normalized welfare distribution places mass
$$ t=\frac{n+k}{2n}>\frac12 $$
at $0$, and the remainder at $1$. Therefore
$$ W(y)=t+(1-2t)y. $$
Its optimum is $W(0)=t$, while $y_k\ge1/2$ implies $W(y_k)\le1/2$. The approximation ratio is at least
$$ 2t=1+\frac kn=\frac32-\frac1n. $$

Case 2: $y_0<1/2$

Instead move $j$ group-$1$ clones from $0$ to $1$. At profile $j$, their common true utility is
$$ U_1(y)=n-j-(n-2j)y. $$
A clone at $1$ can report $0$ to recover profile $j-1$. Strategyproofness gives $y_j\le y_{j-1}$, hence $y_k<1/2$.

The final normalized welfare distribution now places mass $t=(n+k)/(2n)$ at $1$. Its optimum is $1$, and its welfare at the mechanism output is at most $1/2$. The same lower bound follows.

Every profile has dyadic masses and at most three occupied types; every report uses a rational endpoint. Taking arbitrarily large powers of two proves
$$ \rho(f)\ge\frac32 $$
for every admissible family.

Together with the construction,
$$ \boxed{\rho^*=\rho(f^\star)=\frac32}. $$

6. Computation from the compressed support

The mechanism requires no expansion into clones.

Put
$$ K=L+\left\lceil\log_2(N+1)\right\rceil. $$
Using elementary integer arithmetic, its output can be computed in
$$ O\!\left( \bigl[ \tau\log(\tau+1)+m\log(m+1)+\tau+m \bigr]K^2 \right) $$
bit operations.

Here is an exact implementation.

$$ h_g=D\,n_g[1+\alpha_g(n_g-1)]. $$
These are a common positive scaling of the mechanism weights $c_g$.

$$ T=\sum_gh_g, \qquad S_i=\sum_{j=1}^ih_{(j)}. $$
Compute each candidate using
$$ F(S_i/T) = \frac{T^2-S_i^2}{T^2+2TS_i-2S_i^2}. $$
Its denominator is
$$ T^2+2S_i(T-S_i)\ge T^2>0. $$
Compare these rational values exactly with the corresponding medians, then take the minimum of the resulting maxima.

The bit length of $D$ is $O(L)$. The counts, scaled weights, cumulative weights, and candidate numerators and denominators have $O(K)$ bits; here $m\le N$ because groups are nonempty. Rational comparisons and arithmetic therefore cost $O(K^2)$ each. The sorting and arithmetic counts give the stated bound.

⟨structured verdict parsed — rendered above⟩

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

The claimed result is proved with a minor wording correction. The construction establishes
$$ \rho^*=\rho(f^\star)=\frac32 $$
on the stated integral-clone domain. I found no substantive gap in the mechanism, strategyproofness proof, welfare bound, universal lower bound, or running-time analysis.

1. Domain, normalization, and medians

All definitions are valid on the prescribed domain. Nonempty groups and integral clone counts imply $n_g\ge1$, so
$$ \beta_g=1+\alpha_g(n_g-1)\ge1. $$
Consequently, $c_g>0$, $C>0$, and the normalized weights are well-defined.

The expression for $W(y)=SU_N(y;\mu)/C$ follows directly from the conditional distributions $P_g$. A location report preserves $n_g$, hence preserves every aggregation weight. This invariance is essential to the strategyproofness argument and is correctly established.

Both lower-median inequalities hold, including when exactly half the group lies at or below its lower median. The argument establishing the monotonicity of $S_g$ on either side of $q_g$ is valid even when the group utility has a plateau.

2. Mechanism and threshold characterization

The stated derivative is correct:
$$ F'(p)=-\frac{2(p^2-p+1)}{(1+2p-2p^2)^2}<0. $$
The denominator is positive throughout $[0,1]$, and
$$ R(p)=1+2p(1-p)\in[1,3/2]. $$
Thus $H$ exists and is strictly decreasing.

The explicit mechanism is well-defined, returns a rational location, and is independent of the ordering within blocks of equal medians. Within such a block, the final candidate is no larger than any preceding candidate.

The threshold characterization is proved correctly:

The inequalities remain valid at the endpoints and when the output coincides with one or more medians.

The unanimity proof is complete: the last candidate equals the common location, and every candidate is at least that location.

3. Individual location-strategyproofness

The aggregation monotonicity argument correctly shows that increasing one group median cannot decrease the output.

The additional invariance argument is also valid: if the old output lies strictly below the old median, increasing that median leaves both cumulative weights at the old output unchanged. Uniqueness of the threshold characterization then forces the output to remain unchanged. Reversing this comparison gives the corresponding property for a decrease.

The restrictions on which clone can change its group median are correct:

These statements correctly use the strict inequality for mass below a lower median; they do not assume an odd group size.

For a strict output increase, the established order is
$$ x\le q\le y\le y'. $$
Both components of true utility are nonincreasing along this movement. For a strict decrease, the order is
$$ y'\le y\le q\le x, $$
and both components are nondecreasing as functions of facility location on the relevant interval. Their coefficients are nonnegative.

The proof evaluates group utility at the true profile, as required by the task. It covers unchanged medians, unchanged outputs, and arbitrary permitted rational reports. No strategyproofness gap remains.

4. Welfare guarantee

The weight splitting is legitimate. Groups with median at the output may have their aggregation weights split without changing their conditional distributions or total welfare contribution. The threshold inequalities permit a left part of total weight exactly $p$.

The comparison lemma is correct. For $r\ge1$, the stated proximity bounds show that $\phi$ is nonincreasing to the left of $y$ and nondecreasing to its right. Therefore its maximum occurs at an endpoint.

For a distribution with at least half its mass in $[0,y]$, the displayed expectation bound follows because $\phi(0)\le M$. The corresponding right-side bound follows in the same way. These statements also cover endpoint outputs and mass at $y$.

The resulting expression is exactly the maximum of the two endpoint-distribution comparisons with
$$ t_-=\frac p2,\qquad t_+=\frac{1+p}{2}. $$

Both critical algebraic identities check out. Multiplying them by $R(p)$ gives the stated numerators $2-p$ and $1+p$, respectively. They therefore establish
$$ rW_{t_-}(y)=\max_vW_{t_-}(v), \qquad rW_{t_+}(y)=\max_vW_{t_+}(v). $$
The conclusion
$$ W(z)\le rW(y)\le\frac32W(y) $$
follows for every real $z\in[0,1]$.

The zero-denominator issue is correctly handled: $W(1/2)\ge1/2$, so the proved comparison implies $W(y)\ge1/3$.

The claimed attaining example is admissible and correctly computed. Its mechanism output is $1/2$, optimal social utility is $3/4$, and achieved social utility is $1/2$.

5. Universal lower bound

The lower-bound profiles satisfy all domain requirements. Their groups remain nonempty, their masses are dyadic, and the chain uses only rational endpoint reports. There are at most three occupied types.

In Case 1, the displayed strategyproofness inequality correctly uses an occupied clone at the current profile reporting back to the preceding profile. Since $n-2j>0$, it forces $y_j\ge y_{j-1}$. The final welfare calculation yields the claimed lower bound
$$ \frac32-\frac1n. $$

Case 2 correctly reverses the utility slope and forces $y_j\le y_{j-1}$. The resulting ratio calculation is valid, subject to the following wording correction.

Minor issue — Section 5, Case 2: “Its optimum is $1$” is ambiguous and false if it denotes the optimal normalized welfare value. Here $1$ is the optimal facility location; the optimal welfare value is $t$. The preceding Case 1 explicitly distinguishes these quantities.

Minimum clarification: Specify that the optimum occurs at facility location $1$, with normalized welfare value $t$. This is an expositional correction; the subsequent bound already uses the correct value.

Taking arbitrarily large powers of two establishes the supremum lower bound $3/2$. The argument does not require unanimity or any consistency between mechanisms at different population sizes.

6. Computation and running time

The implementation uses the compressed support and does not enumerate clones.

The integer weights satisfy
$$ h_g=DNc_g, $$
so they preserve the normalized cumulative weights. The exact rational formula for $F(S_i/T)$ is correct, and its denominator is strictly positive.

The asserted bit-length bounds are sound. The product $D$ has $O(L)$ bits; counts, scaled weights, cumulative weights, and candidate numerators and denominators have $O(K)$ bits. The condition $m\le N$ follows from nonempty integral groups.

Elementary arithmetic and exact rational comparisons therefore fit the stated $O(K^2)$ cost per operation. The sorting and arithmetic operation counts support the displayed polynomial running time in $m,\tau,L,\log N$.

No unverified external theorem is needed for the claimed improvement or matching lower bound.

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