← back to the atlas

Strategyproof and Proportionally Fair Facility Location (d4-conf-wine-2022-0015)

Answer: The optimal worst-case welfare approximation ratio is \((\sqrt{2}+1)/2\). A deterministic PF rule attaining it computes its location exactly in time polynomial in \(m,\tau,L\) for \(m=1\).

The anchor (named result in the paper)

Theorem 5 — class: algorithmic

The continuous mirror question, as graded

Given a finite rational type set \(T\subseteq[0,L]\) and rational mass vector \(\mu\in\Delta(T)\), determine a rule \(F\) with \(F(\mu)\in[0,L]\) that satisfies continuum PF for every measurable group \(A\), namely \(\lvert F(\mu)-x\rvert\le L(1-\mu(A))+r(A)\) for all \(x\in A\), where \(r(A)=\operatorname*{ess\,sup}_{x\in A}x-\operatorname*{ess\,inf}_{x\in A}x\). Minimize the worst-case welfare ratio \(\rho(F)=\sup_\mu\frac{\max_{y\in[0,L]}\Phi_\mu(y)}{\Phi_\mu(F(\mu))}\), where \(\Phi_\mu(y)=\int(L-\lvert y-x\rvert)\,d\mu(x)\), and compute \(F(\mu)\) exactly.

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

Let \(\ell>0\) be a binary rational interval length; there is one facility, so \(m=1\). A society is given by its support: a nonempty list \(T\subseteq[0,\ell]\cap\mathbb{Q}\) of \(\tau\) types with positive binary rational masses \(\mu_x\), where \(\sum_{x\in T}\mu_x=1\). Here \(\tau=|T|\) is the support size, not the number of possible types; \(L\) is the total input bit length.
A deterministic rule \(F\) assigns a location \(F(\mu)\in[0,\ell]\) to every such society. It satisfies continuum proportional fairness (PF) if, for every nonempty measurable group \(A\subseteq T\) and every \(x\in A\), \(|F(\mu)-x|\le\ell(1-\mu(A))+r(A)\), where \(\mu(A)=\sum_{x\in A}\mu_x\) and \(r(A)=\max A-\min A\). This includes \(A=T\).
Define \(\Phi_\mu(y)=\sum_{x\in T}\mu_x(\ell-|y-x|)\) and \(\rho(F)=\sup_\mu\frac{\max_{y\in[0,\ell]}\Phi_\mu(y)}{\Phi_\mu(F(\mu))}\), where the supremum ranges over all finite rational supports and positive rational mass vectors on the fixed interval. The admissible rules are all deterministic continuum-PF rules.

What is the optimal worst-case welfare approximation ratio \(\inf_F\rho(F)\), and can an attaining rule compute \(F(\mu)\) exactly in time polynomial in \(m,\tau,L\)?

For \(n\ge2\) equally weighted agents, the rule returning the median of their locations and the phantoms \(j\ell/n\), \(1\le j<n\), is optimal among all PF rules, with ratio \(\max_{k\in\mathbb{Z},\,0\le k\le n/2}\frac{n(n-k)}{k^2+(n-k)^2}\); these ratios converge to \((\sqrt{2}+1)/2\). [Discrete approximation result](https://arxiv.org/pdf/2111.01566v3).
No result addressing exactly this mass-input PF approximation problem was identified in the literature search.

Modeling choices made when packaging the task

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

Result

The optimal worst-case ratio is \(\displaystyle \inf_F\rho(F)=\frac{\sqrt2+1}{2}\).

An attaining deterministic PF rule can compute its location exactly in time polynomial in \(\tau,L\), hence in \(m,\tau,L\) for the prescribed \(m=1\). In fact, the rule below maximizes welfare among all PF-feasible locations on every input.

1. Normalize the interval

Set \(a=x/\ell\) and \(z=y/\ell\). Then the interval becomes \([0,1]\), PF becomes

\(\displaystyle |z-a|\le 1-\mu(A)+r(A),\)

and welfare becomes \(\Phi_\mu(\ell z)=\ell W_\mu(z)\), where

\(\displaystyle W_\mu(z)=\sum_a\mu_a(1-|z-a|).\)

Thus normalization preserves welfare ratios and rationality. We work on \([0,1]\) and rescale the output by \(\ell\).

Write the distinct normalized support locations as \(a_1<\cdots<a_\tau\), their masses as \(w_1,\ldots,w_\tau\), and their cumulative masses as

\(\displaystyle S_0=0,\qquad S_i=\sum_{j=1}^i w_j.\)

2. Exact characterization of PF locations

Lemma. The PF-feasible locations form the interval \([\alpha,\beta]\), where

\(\displaystyle \alpha=\max\left\{0,\max_{1\le i\le\tau}(a_i-S_{i-1})\right\},\qquad \beta=\min\left\{1,\min_{1\le i\le\tau}(a_i+1-S_i)\right\}.\)

Proof. For a nonempty group \(A\), let \(a=\min A\), \(b=\max A\), and \(w=\mu(A)\). Its PF constraints are

\(\displaystyle |z-x|\le 1-w+b-a\quad\text{for every }x\in A.\)

The strongest lower bound comes from \(x=b\), and the strongest upper bound from \(x=a\). Consequently, these constraints are equivalent to

\(\displaystyle a+w-1\le z\le b+1-w.\)

Among groups whose minimum is \(a_i\), the largest mass is \(1-S_{i-1}\), attained by the entire suffix \(\{a_i,\ldots,a_\tau\}\). Hence the strongest lower bound with that minimum is \(a_i-S_{i-1}\).

Among groups whose maximum is \(a_i\), the largest mass is \(S_i\), attained by the entire prefix \(\{a_1,\ldots,a_i\}\). Hence the strongest upper bound with that maximum is \(a_i+1-S_i\).

Intersecting these bounds with \([0,1]\) gives exactly the stated interval. \(\square\)

This interval is always nonempty. Indeed, the mean \(\bar z=\sum_iw_i a_i\) satisfies PF: for any group \(A\) and \(x\in A\), the triangle inequality gives

\(\displaystyle |\bar z-x| \le\sum_iw_i|a_i-x| \le\mu(A)r(A)+(1-\mu(A)) \le r(A)+1-\mu(A). \)

Therefore \(\alpha\le\bar z\le\beta\).

Also, singleton PF constraints imply that every PF-feasible \(z\) has positive welfare:

\(\displaystyle W_\mu(z)\ge\sum_iw_i^2>0.\)

Thus all ratios used below are well-defined.

3. An exact polynomial-time rule

Define the candidate set

\(\displaystyle C_\mu=\{\alpha,\beta\}\cup\{a_i:\alpha\le a_i\le\beta\}.\)

Let \(z^\star\) be the smallest candidate maximizing \(W_\mu\), and return \(F^\star(\mu)=\ell z^\star\).

This rule maximizes welfare over the entire PF interval. To see this, \(W_\mu\) is continuous and affine between consecutive support locations. Partition \([\alpha,\beta]\) at its support locations. On each resulting interval, an affine function attains its maximum at an endpoint. All such endpoints belong to \(C_\mu\).

The algorithm sorts the support, computes cumulative masses and the two interval endpoints, and evaluates welfare at at most \(\tau+2\) candidates. It uses \(O(\tau\log\tau)\) rational comparisons and \(O(\tau^2)\) rational arithmetic operations.

All calculations involve rational sums, differences, products, and comparisons of polynomial bit length: a common denominator can be formed by multiplying input denominators, whose combined bit length is bounded by the input length. Consequently, the algorithm runs in polynomial bit time and returns an exact rational location.

4. Transfer of the discrete upper bound

We use the supplied finite-agent result: for \(N\ge2\), the uniform phantom median satisfies PF and has welfare ratio

\(\displaystyle R_N=\max_{\substack{k\in\mathbb Z\\0\le k\le N/2}} \frac{N(N-k)}{k^2+(N-k)^2}. \)

These are Proposition 3 and Theorem 5 of the [cited paper](https://arxiv.org/pdf/2111.01566v3).

Fix any rational-mass society. Choose a common denominator \(N\ge2\), so that \(n_i=Nw_i\) is a positive integer for every \(i\). Form an auxiliary finite-agent profile containing \(n_i\) agents at \(a_i\), and let \(u_N\) be its uniform phantom outcome.

For every support group \(A\), take the agent group consisting of all copies of its types. This group has relative size \(\mu(A)\) and range \(r(A)\). Its discrete PF inequalities are exactly the mass-input PF inequalities for \(A\). Hence \(u_N\in[\alpha,\beta]\).

The auxiliary profile’s total welfare at any \(z\) is \(NW_\mu(z)\). Its welfare ratio therefore equals the normalized mass-input ratio. Since \(z^\star\) maximizes welfare over the PF interval,

\(\displaystyle \frac{\max_zW_\mu(z)}{W_\mu(z^\star)} \le \frac{\max_zW_\mu(z)}{W_\mu(u_N)} \le R_N. \)

This replication is only a proof device; the algorithm in Section 3 never constructs the \(N\) agents or phantoms.

To bound \(R_N\), define

\(\displaystyle f(q)=\frac{1-q}{q^2+(1-q)^2}\qquad(0\le q\le\tfrac12).\)

Then \(R_N=\max_k f(k/N)\), and differentiation gives

\(\displaystyle f'(q)=\frac{1-4q+2q^2}{(q^2+(1-q)^2)^2}. \)

The numerator changes from positive to negative at \(q_\star=1-1/\sqrt2\). Thus

\(\displaystyle R_N\le f(q_\star)=\frac{\sqrt2+1}{2}. \)

Since the society was arbitrary, \(\rho(F^\star)\le(\sqrt2+1)/2\).

5. Matching lower bound for every PF rule

For any rational \(q\in(0,\tfrac12]\), consider the two-type society with mass \(1-q\) at \(0\) and mass \(q\) at \(1\).

Singleton PF for the type at \(0\) requires \(z\le q\). Singleton PF for the type at \(1\) requires \(z\ge q\). Therefore every PF rule must return \(z=q\).

For this society,

\(\displaystyle W_\mu(z)=(1-q)(1-z)+qz=1-q+(2q-1)z. \)

Because \(q\le\tfrac12\), its unrestricted maximum is \(1-q\), attained at \(z=0\). At the forced PF location,

\(\displaystyle W_\mu(q)=(1-q)^2+q^2.\)

Thus every PF rule has ratio at least \(f(q)\) for every such rational \(q\). Rational numbers in this interval approach \(q_\star=1-1/\sqrt2\), and continuity yields

\(\displaystyle \rho(F)\ge f(q_\star)=\frac{\sqrt2+1}{2}.\)

Together with Section 4, this proves the claimed optimum and its attainment by the exact polynomial-time rule \(F^\star\). The lower bound uses a supremum over rational societies; an irrational input mass is not required.

⟨structured verdict parsed — rendered above⟩

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

The prover resolves both parts of the task. The optimal ratio and exact polynomial-time attainment follow from the argument as written. I found no major or minor mathematical issues.

1. Normalization

Dividing locations and distances by \(\ell>0\) correctly converts PF to its unit-interval form. The range \(r(A)\) in the normalized inequality is understood to be the range of the normalized group.

The welfare identity \(\Phi_\mu(\ell z)=\ell W_\mu(z)\) is correct, so normalization preserves approximation ratios. Rational normalization and subsequent rescaling are exact operations with polynomial bit complexity.

2. Characterization of PF-feasible locations

For a nonempty group with minimum \(a\), maximum \(b\), and mass \(w\), intersecting its distance constraints gives precisely
\[ a+w-1\le z\le b+1-w. \]
The extreme members supply the strongest bounds; all other members’ bounds are weaker.

For a fixed minimum \(a_i\), the complete suffix has the greatest possible group mass, hence supplies the strongest lower bound. The corresponding prefix argument correctly supplies the strongest upper bound. Every nonempty group has a minimum and maximum, so this reduction accounts for all groups, including the entire support.

Thus the formulas for \(\alpha\) and \(\beta\) characterize the feasible set exactly.

The mean establishes nonemptiness correctly: within-group distances are bounded by the group range, and outside-group distances are bounded by the unit interval length. The final inequality uses only \(0\le\mu(A)\le1\) and \(r(A)\ge0\).

The positivity claim also follows directly from singleton PF: each type receives normalized utility at least its own mass. Consequently, \(W_\mu(z)\ge\sum_iw_i^2>0\) at every feasible location.

3. Exact welfare-maximizing rule and complexity

The candidate-set argument is valid. Welfare is continuous and affine between support locations, so its maximum on the feasible interval occurs at an interval endpoint or a support location within that interval.

The specified tie-breaking makes the rule deterministic. Nonemptiness of the feasible interval ensures that the candidate set is nonempty, and every candidate is PF-feasible.

The stated operation counts are sufficient for polynomial time. The bit-complexity justification also holds: cumulative masses, normalized locations, feasible endpoints, and candidate welfare values admit rational representations of polynomial bit length. Welfare evaluation uses products of these bounded-size quantities; it does not involve an uncontrolled sequence of repeated multiplications.

The argument covers the relevant edge cases:

The algorithm’s complexity depends on support size and input length, not on the potentially enormous replicated population.

4. Discrete theorem and replication

The cited results match the theorem used. Proposition 3 states that the Uniform Phantom mechanism satisfies PF; Theorem 5, together with Lemma 2, gives the stated finite-agent welfare ratio. The paper’s displayed PF inequality uses group relative size and group range exactly as required here, and includes the full agent set. Its welfare objective is interval length minus distance. [Cited paper, Definition 6, Proposition 3, Lemma 2, and Theorem 5](https://arxiv.org/pdf/2111.01566v3).

The application satisfies the hypotheses:

Therefore the replicated phantom outcome satisfies every mass-input PF constraint. Its total welfare is \(N\) times normalized mass welfare, so the approximation ratio is unchanged.

Since the constructed rule maximizes welfare over the PF interval, its welfare is at least that of the replicated phantom outcome. Positivity established earlier justifies the ratio comparison.

5. Maximization of the ratio bound

The derivative calculation is correct:
\[ f'(q)=\frac{1-4q+2q^2}{\bigl(q^2+(1-q)^2\bigr)^2}. \]
The denominator is positive throughout the stated domain. The numerator has exactly one root there, at \(q_\star=1-1/\sqrt2\), with the stated sign change.

The value \(f(q_\star)=(\sqrt2+1)/2\) is correct. Since every grid point used in \(R_N\) lies in the continuous maximization domain, this establishes the claimed upper bound for every rational society.

6. Matching lower bound and attainment

For the two-type society, the singleton constraints correctly force \(z=q\). The welfare expression, its unrestricted maximum for \(q\le1/2\), and its value at the forced location are all correct, including the boundary case \(q=1/2\).

The quantifiers are sufficient: every PF rule has ratio at least \(f(q)\) for every admissible rational \(q\). Continuity and rational approximation to \(q_\star\) therefore give the lower bound on the supremum for each rule. No irrational input or maximizing society is required.

Combining this universal lower bound with the constructed rule’s upper bound proves both the optimal ratio and attainment by an exact polynomial-time rule.

No additional clarification or repair is needed.

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