← back to the atlas

Facility Location with Minimax Envy (d4-conf-ijcai-2016-0474)

Answer: Yes. The proposed \(\alpha\)-LRM rule is anonymous, truthful in every finite lift, has uniform additive error at most \(\varepsilon\), and admits polynomial-time construction and evaluation with polynomial representation size.

The anchor (named result in the paper)

Theorem 3 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateFor any ✏> 0, there exists a mechanism in the class ↵-LRM with additive approximation ✏.

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

The continuous mirror question, as graded

Given a finite rational location-type and report set \(T\subseteq\mathbb{R}\) and rational \(\varepsilon>0\), output a compact anonymous rule \(M\) on distributions \(\mu\) over \(T\) such that every rational finite lift is truthful-in-expectation and \(\sup_{\mu}\bigl(E_{\mu}(M(\mu))-O(\mu)\bigr)\le\varepsilon\); an α-LRM formula with \(\alpha\le\min\{1/4,\varepsilon/2\}\) is an allowed representation.

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

Let \(T\subseteq\mathbb Q\) be a nonempty finite set of true locations and permitted reports, with \(m=|T|\). Facility locations may be anywhere in \(\mathbb R\); agents minimize expected distance, without payments.
A society \(\mu\) is given by its support: the list of its \(\tau\) types with positive mass, each mass a binary rational, summing to \(1\). Here \(\tau\) is the support size, not the number of possible types. Let \(L\) denote total input bit length, including locations, masses, and the positive rational accuracy parameter \(\varepsilon\).
For \(S=\operatorname{supp}\mu\), write \(a=\min S\), \(b=\max S\), and \(d=b-a\). For \(d>0\), define \(g_\mu(y)=\max_{s,t\in S}(|y-s|-|y-t|)/d\), \(O(\mu)=\min_{y\in\mathbb R}g_\mu(y)\), and \(E_\mu(M(\mu))=\mathbb E_{Y\sim M(\mu)}g_\mu(Y)\). For singleton support, set both objectives to \(0\) and require the facility at that type.
An anonymous rule maps rational distributions on \(T\) to facility lotteries with finite expected distance. Every finite lift must be truthful-in-expectation: for every \(n\ge1\), \(x\in T^n\), agent \(i\), and report \(r\in T\), with \(\mu_x=n^{-1}\sum_j\delta_{x_j}\), require \(\mathbb E_{Y\sim M(\mu_x)}|Y-x_i|\le\mathbb E_{Y\sim M(\mu_x+(\delta_r-\delta_{x_i})/n)}|Y-x_i|\).
A compact representation may be an \(\alpha\)-LRM formula: put probabilities \(1-2\alpha,\alpha,\alpha\) at \((a+b)/2,a-h,b+h\), respectively, where \(h=(1-4\alpha)d/(4\alpha)\) and \(0<\alpha\le\min\{1/4,\varepsilon/2\}\); rational parameters and lottery atoms are encoded in binary.

Can one, for every such \(T\) and \(\varepsilon>0\), construct a compact anonymous rule satisfying finite-lift truthfulness and \(\sup_{\mu}\bigl(E_\mu(M(\mu))-O(\mu)\bigr)\le\varepsilon\), with construction, representation size, and evaluation polynomial in \(m,\tau,L\)?

For finite agent profiles on the unrestricted real line, truthful-in-expectation mechanisms achieve arbitrarily small additive minimax-envy error ([Cai, Filos-Ratsikas, and Tang](https://arisfilosratsikas.com/papers/facility_envy.pdf)). No separately stated result for this distribution-input formulation was located.

Modeling choices made when packaging the task

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

Result and construction

Yes. The proposed \(\alpha\)-LRM formula defines a compact anonymous rule with all the required properties. Its construction and evaluation use polynomial time in the binary input length; no finite lift needs to be constructed.

The formula comes from [Cai, Filos-Ratsikas, and Tang](https://arisfilosratsikas.com/papers/facility_envy.pdf). Below is a direct proof for the distribution-input formulation, including singleton supports and binary encoding bounds.

Fix the positive rational accuracy parameter \(\varepsilon\), and choose
\(\alpha=\min\{1/4,\varepsilon/2\}\).
Write \(\beta=1-2\alpha\). Thus \(\alpha>0\), \(\beta>0\), and \(2\alpha\le\varepsilon\).

For any rational distribution \(\mu\) on \(T\), let
\(S=\operatorname{supp}\mu\),
\(a=\min S\),
\(b=\max S\),
\(d=b-a\), and
\(c=(a+b)/2\).
Set
\(h=(1-4\alpha)d/(4\alpha)\).
Since \(\alpha\le1/4\), we have \(h\ge0\).

Define
\(M(\mu)=\beta\delta_c+\alpha\delta_{a-h}+\alpha\delta_{b+h}\),
where \(\delta_z\) denotes unit mass at \(z\).

The probabilities are nonnegative and sum to \(1\). If \(S=\{a\}\), then \(d=h=0\), so all atoms coincide at \(a\), as required. Every output has finite support and finite expected distance. The rule is anonymous because it depends only on the reported distribution.

Expected-distance lemma

For an arbitrary true location \(z\in\mathbb R\), let \(C_S(z)\) be its expected distance under this lottery. We claim that

\(C_S(z)\ge\beta\max_{s\in S}|z-s|\),

with equality whenever \(z\in[a,b]\).

Indeed, the triangle inequality gives
\(|z-(a-h)|+|z-(b+h)|\ge d+2h\).
Furthermore,

\(\alpha(d+2h)=\alpha d+(1-4\alpha)d/2=\beta d/2\).

Consequently,

\(C_S(z)=\beta|z-c|+\alpha\bigl(|z-(a-h)|+|z-(b+h)|\bigr)\ge\beta\bigl(|z-c|+d/2\bigr)\).

For every \(z\), the endpoint identity is
\(|z-c|+d/2=\max\{|z-a|,|z-b|\}\).
Since \(a,b\in S\) and every point of \(S\) lies between them, this maximum equals \(\max_{s\in S}|z-s|\).

If \(z\in[a,b]\), then also \(z\in[a-h,b+h]\). The two distances to the lottery’s outer atoms therefore sum exactly to \(d+2h\), proving equality. This argument includes \(d=0\): equality then holds at \(z=a=b\).

Truthfulness for every finite lift

Fix any \(n\ge1\), profile \(x\in T^n\), agent \(i\), and alternative report \(r\in T\). Write \(t=x_i\), and let \(x'\) be the profile obtained by replacing \(x_i\) with \(r\).

If \(n=1\), truthful reporting produces the facility at \(t\), with cost \(0\); every deviation has nonnegative cost.

Now suppose \(n\ge2\). Since \(t\) belongs to the truthful support, the equality case of the lemma gives

\(\mathbb E_{Y\sim M(\mu_x)}|Y-t|=\beta\max_j|t-x_j|=\beta\max_{j\ne i}|t-x_j|\).

The last equality holds because the omitted self-distance is \(0\), while the remaining set is nonempty.

Applying the lower bound from the lemma to the deviating support gives

\(\mathbb E_{Y\sim M(\mu_{x'})}|Y-t|\ge\beta\max_j|t-x'_j|\ge\beta\max_{j\ne i}|t-x_j|\).

The second inequality holds because every other agent’s report remains unchanged. These two displays prove the required truthfulness inequality.

Moreover,
\(\mu_{x'}=\mu_x+(\delta_r-\delta_{x_i})/n\),
so this is exactly finite-lift truthfulness as defined in the question. The argument applies to every \(n\) with the same fixed parameter \(\alpha\).

The midpoint minimizes the stated envy objective

Suppose \(d>0\), and define
\(\rho_S(y)=\min_{s\in S}|y-s|\).

Because maximization over the two types is independent,

\(d\,g_\mu(y)=\max_{s\in S}|y-s|-\min_{t\in S}|y-t|=d/2+|y-c|-\rho_S(y)\).

Choose \(s_0\in S\) attaining \(\rho_S(c)\), which exists because \(S\) is finite. The triangle inequality implies

\(\rho_S(y)\le|y-s_0|\le|y-c|+\rho_S(c)\).

Substitution yields

\(d\,g_\mu(y)\ge d/2-\rho_S(c)=d\,g_\mu(c)\).

Thus the midpoint is a global minimizer, and

\(O(\mu)=g_\mu(c)=1/2-\rho_S(c)/d\).

Since \(0\le\rho_S(c)\le d/2\), we also obtain \(0\le O(\mu)\le1/2\).

Uniform additive error

For \(y\le a\), the largest distance to a support point is \(b-y\), and the smallest is \(a-y\); their difference is \(d\). Hence \(g_\mu(y)=1\). The same calculation gives \(g_\mu(y)=1\) for \(y\ge b\).

Because \(h\ge0\), both outer lottery atoms therefore have objective value \(1\). The midpoint has objective value \(O(\mu)\), so

\(E_\mu(M(\mu))=\beta O(\mu)+2\alpha\).

It follows that

\(E_\mu(M(\mu))-O(\mu)=2\alpha(1-O(\mu))\le2\alpha\le\varepsilon\).

For singleton supports, the error is \(0\) by definition. Consequently,

\(\sup_\mu\bigl(E_\mu(M(\mu))-O(\mu)\bigr)\le\varepsilon\).

In fact, if \(m\ge2\), the supremum equals \(2\alpha\): choose any two distinct permitted types and assign mass \(1/2\) to each. Their midpoint has equal distance to both types, so \(O(\mu)=0\). If \(m=1\), the supremum is \(0\).

Construction, representation, and evaluation complexity

Use the ordinary binary encoding of a rational as an integer numerator and a positive integer denominator.

Each evaluated parameter and atom results from a fixed number of operations on input rationals. Its numerator and denominator therefore have \(O(L)\) bits. Rational comparisons, arithmetic, and optional reduction to lowest terms all take polynomial time in \(L\). Thus evaluation takes \(\tau\operatorname{poly}(L)\) time and outputs at most three atoms with total encoding length \(O(L)\).

The masses determine which types are present but otherwise do not enter the formula. In particular, the algorithm never expands the rational masses into an explicit agent population.

This proves all the requested properties.

⟨structured verdict parsed — rendered above⟩

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

Verdict: proved. The construction resolves the distribution-input task. Every substantive step is justified, including truthfulness for all finite lifts, singleton supports, the uniform error bound, and polynomial binary complexity. No major or minor mathematical issues were found.

\(\alpha(d+2h)=\alpha d+(1-4\alpha)d/2=(1-2\alpha)d/2=\beta d/2\).
The endpoint identity \(|z-c|+d/2=\max\{|z-a|,|z-b|\}\) holds for every real \(z\). Since every support point lies between the endpoints, this is also the maximum distance to the support. Equality holds when \(z\in[a,b]\), including the stated singleton case.

\(d\,g_\mu(y)=d/2+|y-c|-\rho_S(y)\).
A nearest support point to \(c\) exists because the support is finite. The stated triangle inequality establishes
\(\rho_S(y)\le|y-c|+\rho_S(c)\), which yields \(g_\mu(y)\ge g_\mu(c)\) for every real \(y\). Thus the claimed global minimum and the bounds \(0\le O(\mu)\le1/2\) follow.

\(E_\mu(M(\mu))-O(\mu)=2\alpha(1-O(\mu))\le2\alpha\le\varepsilon\).
Singleton support has zero error by definition. The claimed exact supremum for \(m\ge2\) is also correct: a distribution supported on two distinct permitted types has \(O(\mu)=0\). The \(m=1\) case is handled separately.

Repair feedback: None required.

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