← back to the atlas

Mechanism Design for Connecting Regions Under Disruptions (aaai25-33496)

Answer: Exact expected-cost minimization and its decision version are polynomial-time solvable for \(m=2\), with binary-encoded rational \(k\). The weighted threshold rule is always optimal and group-strategyproof under the specified positive-mass reporting semantics, for every real \(k\in[0,1)\).

The anchor (named result in the paper)

Theorem 2 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateMechanism 1 is group strategyproof and opti- mal for the social cost.

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

The continuous mirror question, as graded

Given rational o and k, and a finite rational distribution over location types on either side of o, compute a pathway (a,b) minimizing expected agent travel cost, and determine whether the weighted threshold rule is optimal and group-strategyproof under a specified positive-mass or clone-stable reporting semantics.

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

Given rational \(o\in(0,1)\) and \(k\in[0,1)\), let \(D=[0,o)\cup(o,1]\). A society is given by its support: \(\tau\) distinct rational location types \(x_i\in D\), each with positive binary-rational mass \(w_i\), with \(\sum_i w_i=1\) and positive mass in both regions. Here \(\tau\) is the support size, not the number of possible types; \(L\) is the total input bit length and \(m=2\) is the fixed number of regions.
A feasible pathway satisfies \(0\le a<o<b\le1\). Its individual cost is \(c(a,b,x)=|x-a|+k(b-a)+1-b\) for \(x<o\), and \(c(a,b,x)=|x-b|+k(b-a)+a\) for \(x>o\); minimize \(C_\mu(a,b)=\sum_i w_i c(a,b,x_i)\).
For a reported distribution \(\nu\), write \(p=\nu([0,o))\), \(q=\nu((o,1])\), and define \(X_L=\{t\in[0,o):(\nu([0,t])+q)(1-k)<\nu((t,o))(1+k)\}\) and \(X_R=\{t\in(o,1]:(\nu([t,1])+p)(1-k)<\nu((o,t))(1+k)\}\).
The weighted threshold rule \(f(\nu)\) returns \(a=\sup X_L\), or \(a=0\) if empty, and \(b=\inf X_R\), or \(b=1\) if empty; the strict inequalities fix its tie-breaking.
Use positive-mass reporting semantics: a coalition selects finitely many positive rational portions of the true type masses, with positive total mass, and assigns each portion a rational reported location in its true region; unselected mass reports truthfully, and mass cannot be created or deleted. Group-strategyproofness means no such deviation strictly decreases \(c(f(\nu),x)\), evaluated at the true location \(x\), for every participating portion.

Is exact expected-cost minimization polynomial-time solvable in \(m,\tau,L\), or NP-hard (for its decision version, given rational \(T\), does a feasible pathway satisfy \(C_\mu(a,b)\le T\))?
Is the weighted threshold rule always optimal and group-strategyproof under the specified reporting semantics?

For finite equally weighted agents, the threshold rule is polynomial-time computable, social-cost optimal, and group-strategyproof with within-region reports. [Verified discrete result](https://arxiv.org/html/2605.18626v1#S4).
No result settling this exact mass-input problem and reporting semantics was located in the sources checked.

Modeling choices made when packaging the task

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

Result and computational interpretation

Exact expected-cost minimization is polynomial-time solvable for the stated model with \(m=2\). The weighted threshold rule is always optimal and group-strategyproof under the specified reporting semantics.

For the bit-complexity claim, I interpret \(k\) as a binary-encoded rational, or a fixed rational constant. An arbitrary real \(k\) without an effective representation does not define a bit-complexity problem. The optimality and group-strategyproofness proofs below hold for every real \(k\in[0,1)\).

These conclusions extend the discrete statement in [Theorem 2 of the cited paper](https://arxiv.org/html/2605.18626v1#S4). The proofs below work directly with masses.

1. Exact characterization of the threshold rule

Let \(\rho\) be any finitely supported probability distribution on \(D\), with positive mass in both regions. Define

\[ p=\rho([0,o)),\qquad q=\rho((o,1]),\qquad s=\frac{1-k}{2},\qquad \alpha=p-s,\qquad \beta=q-s. \]

Here and below, display equations use the same mathematical notation as inline equations. Since \(k<1\), we have \(s>0\), so \(\alpha<p\) and \(\beta<q\).

For \(t\in[0,o)\), put \(F(t)=\rho([0,t])\). The left threshold inequality is equivalent to

\[ (F(t)+q)(1-k)<(p-F(t))(1+k) \quad\Longleftrightarrow\quad F(t)<\alpha. \]

For \(t\in(o,1]\), put \(G(t)=\rho([t,1])\). Likewise, the right threshold inequality is equivalent to \(G(t)<\beta\).

Consequently, the rule has the following finite characterization:

To verify the left characterization when \(\alpha>0\), such a support location exists because the cumulative mass at the largest left support location is \(p>\alpha\). Before the first qualifying location, \(F(t)<\alpha\); at and after it, \(F(t)\ge\alpha\). Thus \(X_L=[0,a)\) if \(a>0\), and \(X_L\) is empty if \(a=0\).

The right characterization follows identically using descending cumulative mass: \(X_R=(b,1]\) if \(b<1\), and it is empty if \(b=1\).

In particular, the returned pathway is feasible. Every nondefault endpoint belongs to its corresponding support, hence remains strictly outside the obstacle.

Two strict inequalities will be essential later. Whenever \(\alpha>0\) and \(a>0\),

\[ \rho([0,a))<\alpha\le\rho([0,a]). \]

Whenever \(\beta>0\) and \(b<1\),

\[ \rho((b,1])<\beta\le\rho([b,1]). \]

2. Proof of optimality

Expanding the expected cost gives

\[ C_\rho(a,b)=p+A(a)+B(b), \]

where

\[ A(a)=\sum_{x_i<o}w_i|x_i-a|+(q-k)a, \qquad B(b)=\sum_{x_i>o}w_i|x_i-b|+(k-p)b. \]

Thus the two endpoint choices are independent minimization problems.

The function \(A\) is continuous and piecewise linear. Its right derivative at every \(t\in[0,o)\) is

\[ A'_+(t) =\rho([0,t])-\rho((t,o))+q-k =2(F(t)-\alpha). \]

The derivative formula includes atoms at \(t\): their right derivative contribution is their positive mass.

If \(\alpha\le0\), every slope is nonnegative, so \(a=0\) minimizes \(A\). If \(\alpha>0\), the endpoint characterized in Section 1 has negative slopes everywhere before it and nonnegative slopes everywhere after it. Summing slope times interval length over the finitely many linear pieces proves

\[ A(a)\le A(u)\qquad\text{for every }u\in[0,o). \]

Similarly, the left derivative of \(B\) at \(t\in(o,1]\) is

\[ B'_-(t) =\rho((o,t))-\rho([t,1])+k-p =2(\beta-G(t)). \]

If \(\beta\le0\), every slope is nonpositive, so \(b=1\) minimizes \(B\). If \(\beta>0\), the endpoint characterized in Section 1 has nonpositive slopes before it and positive slopes after it. Therefore

\[ B(b)\le B(v)\qquad\text{for every }v\in(o,1]. \]

Adding these inequalities proves that \(f(\rho)\) minimizes \(C_\rho\) over every feasible pathway.

This also resolves attainment despite the open boundaries at \(o\): a feasible minimizer actually exists. When there are flat intervals of minimizers, the rule selects the smallest minimizing left endpoint and the largest minimizing right endpoint.

3. Polynomial-time exact computation

Partition the support by region and sort each part. Compute \(p,q,\alpha,\beta\), then scan cumulative masses in increasing order on the left and decreasing order on the right. Section 1 identifies the returned endpoints through exact comparisons.

This takes \(O(\tau\log\tau)\) rational comparisons and \(O(\tau)\) rational arithmetic operations. Evaluate the cost of the resulting pathway using the original cost formula.

All these operations have polynomial bit complexity in \(L\). For example, a common denominator obtained by multiplying the input denominators has bit length bounded by their total encoded length. Cumulative masses, threshold comparisons, and objective evaluation therefore involve rational numbers with polynomially bounded bit length.

The algorithm never expands masses into equally weighted agents.

For the decision problem, compute the attained minimum \(C^*=C_\mu(f(\mu))\) and answer yes exactly when \(C^*\le T\). Hence the decision problem belongs to \(\mathrm P\). This establishes polynomial-time solvability for the specified fixed value \(m=2\); it makes no assertion about an unspecified extension to more regions.

4. Proof of group-strategyproofness

Let a coalition select finitely many portions indexed by \(j\), with positive masses \(v_j\), true locations \(x_j\), and reported locations \(y_j\) in their true regions. Write \(\nu\) for the resulting distribution.

For every set \(S\subseteq D\),

\[ \nu(S)-\mu(S) =\sum_j v_j\bigl(\mathbf 1_{\{y_j\in S\}}-\mathbf 1_{\{x_j\in S\}}\bigr). \]

Therefore, a strict increase of mass in \(S\) requires at least one participating positive portion to enter \(S\); a strict decrease requires one to leave.

Within-region reporting preserves \(p\) and \(q\), and consequently preserves \(\alpha\) and \(\beta\). Let

\[ f(\mu)=(a,b),\qquad f(\nu)=(a',b'), \qquad d_a=|a'-a|,\qquad d_b=|b'-b|. \]

If both displacements vanish, nobody strictly benefits. Otherwise, consider an endpoint whose displacement is largest.

4.1. The left endpoint moves at least as far

Suppose \(d_a\ge d_b\) and \(d_a>0\). Necessarily \(\alpha>0\), since otherwise the left endpoint is constantly zero.

Case \(a'>a\). The quantile characterization gives

\[ \mu([0,a])\ge\alpha>\nu([0,a]). \]

Thus some participating portion has true location \(x\le a\) and reports beyond \(a\). For this portion, both endpoints \(a,a'\) lie weakly to its right, so its cost change is exactly

\[ c(a',b',x)-c(a,b,x) =(1-k)(a'-a)-(1-k)(b'-b) \ge(1-k)(d_a-d_b)\ge0. \]

This participant does not strictly benefit.

Case \(a'<a\). Here \(a>0\), and

\[ \mu([0,a))<\alpha \le\nu([0,a']) \le\nu([0,a)). \]

Some participating portion therefore has true location \(x\ge a\) and reports below \(a\). Both left endpoints lie weakly to its left. Its cost change is

\[ c(a',b',x)-c(a,b,x) =(1+k)(a-a')-(1-k)(b'-b) \ge(1+k)d_a-(1-k)d_b \ge2k\,d_a\ge0. \]

Again, this participant does not strictly benefit.

4.2. The right endpoint moves farther

Suppose \(d_b>d_a\). Necessarily \(\beta>0\).

Case \(b'>b\). Since \(b<1\),

\[ \mu((b,1])<\beta \le\nu([b',1]) \le\nu((b,1]). \]

Some participating portion has true location \(x\le b\) and reports above \(b\). Both right endpoints lie weakly to its right. Its cost change is

\[ c(a',b',x)-c(a,b,x) =(1+k)(b'-b)+(1-k)(a'-a) \ge(1+k)d_b-(1-k)d_a \ge0. \]

Case \(b'<b\). The quantile characterization gives

\[ \mu([b,1])\ge\beta>\nu([b,1]). \]

Some participating portion has true location \(x\ge b\) and reports below \(b\). Both right endpoints lie weakly to its left. Its cost change is

\[ c(a',b',x)-c(a,b,x) =(1-k)(b-b')+(1-k)(a'-a) \ge(1-k)(d_b-d_a)>0. \]

Thus every possible changed outcome has a participating positive portion whose true-location cost does not strictly decrease. This proves group-strategyproofness under exactly the stated semantics. The proof includes \(k=0\), threshold equalities, and default endpoints.

⟨structured verdict parsed — rendered above⟩

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

The prover’s argument resolves both questions for the stated model with \(m=2\). The threshold characterization, optimality proof, exact algorithm, and group-strategyproofness proof are correct. I found no mathematical gaps requiring repair.

The polynomial-time conclusion uses the explicitly stated convention that \(k\) is a binary-encoded rational or a fixed rational constant. The optimality and incentive conclusions hold for every real \(k\in[0,1)\).

1. Scope and assumptions

The proof addresses finitely supported probability distributions with positive mass in both regions. Every allowed deviation produces another distribution of this form: only finitely many portions are reassigned, all reported locations remain in their true regions, and total mass is preserved.

Consequently, applying the threshold characterization to both \(\mu\) and \(\nu\) is justified. The proof does not assume equally weighted agents or expand rational masses into agents.

The convention concerning the representation of \(k\) appropriately resolves the task’s encoding ambiguity. The restriction to \(m=2\) also matches the task; no generalization to additional regions is needed.

2. Threshold characterization

Both algebraic reductions are correct. Using \(p+q=1\), the left inequality reduces to \(2F(t)<2p-(1-k)\), equivalently \(F(t)<\alpha\). The right inequality similarly reduces to \(G(t)<\beta\).

Since \(k<1\), the quantities satisfy \(\alpha<p\) and \(\beta<q\). Therefore, whenever a threshold is positive, a qualifying support location exists.

The finite characterizations correctly implement the prescribed supremum and infimum:

The descriptions \(X_L=[0,a)\) and \(X_R=(b,1]\), with the stated empty-set exceptions, correctly handle atoms and threshold equalities.

The strict inequalities involving mass immediately before the selected support location follow from choosing the first qualifying location in the relevant ordering. These inequalities are precisely the ones subsequently used in the deviation proof.

Feasibility follows: selected support locations lie strictly on their respective sides of \(o\), and the defaults \(0\) and \(1\) are feasible.

Assessment: Correct, including endpoint atoms, empty threshold sets, and exact threshold ties.

3. Expected-cost decomposition and optimality

The expansion \(C_\rho(a,b)=p+A(a)+B(b)\) is correct. In particular, the coefficients of \(a\) and \(b\) are respectively \(q-k\) and \(k-p\); no constant or coupling term is missing.

Both one-sided derivative formulas are correct:

The slope signs asserted in each threshold case follow from Section 1. Finite piecewise linearity justifies comparing function values by summing slopes over the intervening linear pieces. This establishes minimization over the entire feasible endpoint domains, rather than merely over support locations.

The open boundaries at \(o\) cause no attainment problem: the proof identifies actual feasible minimizing endpoints. The stated tie-breaking—smallest minimizing left endpoint and largest minimizing right endpoint—is consistent with the slope signs and threshold equalities.

Assessment: Correct. No missing convexity theorem or existence lemma is required.

4. Exact polynomial-time computation

Sorting the support and scanning cumulative masses implements the characterization directly. The stated counts of rational comparisons and arithmetic operations are valid.

The bit-complexity justification is sufficient. Products of input denominators have bit length bounded by the sum of their encoded lengths. The cumulative sums, threshold calculations, and cost evaluation therefore admit rational representations of polynomial bit length. Exact rational comparisons and arithmetic on these representations take polynomial time.

The endpoints are input support locations or defaults, so their output representations also have polynomial size.

Because the minimum is attained, comparing its exact value with \(T\) correctly decides whether any feasible pathway has cost at most \(T\). This establishes membership in \(\mathrm P\) under the stated representation of \(k\).

Assessment: Correct. The proof establishes polynomial dependence on the encoded input size and support size for fixed \(m=2\).

5. Group-strategyproofness

The mass-change identity is valid under the specified reporting semantics. A strict increase or decrease in a set’s mass forces at least one participating positive portion to enter or leave that set, respectively.

Within-region reporting preserves \(p,q,\alpha,\beta\). The displacement split covers every changed outcome, including equal displacements.

Left endpoint dominates, moving right

When \(a'>a\), the inequality \(\mu([0,a])\ge\alpha>\nu([0,a])\) is valid, including when \(a=0\).

A participating portion must leave \([0,a]\). Its true location satisfies \(x\le a\), and within-region reporting ensures it is a left-region portion. The displayed cost change is exact. Its lower bound is nonnegative because \(d_a\ge d_b\).

Left endpoint dominates, moving left

When \(a'<a\), necessarily \(a>0\). The strict pre-threshold inequality and \([0,a']\subseteq[0,a)\) give the stated strict mass increase in \([0,a)\).

An entering portion has true location \(x\ge a\). Its report belongs to the left region, so its true location does too. The displayed cost change and both subsequent bounds are correct. The final bound remains nonnegative when \(k=0\).

Right endpoint dominates, moving right

When \(b'>b\), necessarily \(b<1\). The strict post-threshold inequality and \([b',1]\subseteq(b,1]\) justify the strict mass increase.

An entering portion has true location \(x\le b\) in the right region. The exact cost change has the stated coefficients and signs. Its lower bound is nonnegative under \(d_b>d_a\).

Right endpoint dominates, moving left

When \(b'<b\), the inequality \(\mu([b,1])\ge\beta>\nu([b,1])\) is valid, including when \(b=1\).

A leaving portion has true location \(x\ge b\). The displayed cost change is correct, and its lower bound is strictly positive because \(1-k>0\) and \(d_b>d_a\).

Thus every changed outcome has a participating positive portion that fails to benefit strictly. An unchanged outcome cannot strictly benefit any participant. This is exactly the group-strategyproofness definition in the task.

Assessment: Correct under the specified semantics, including partial mass selection, split reports, default endpoints, and \(k=0\).

6. Citation and repair feedback

The cited [Theorem 2](https://arxiv.org/html/2605.18626v1#S4) does state optimality and group-strategyproofness for the discrete mechanism. The submitted mass argument is self-contained and does not rely on importing that theorem into different reporting semantics.

No mathematical repair or additional clarification is needed. The explicit encoding convention for \(k\) should remain attached to the complexity claim.

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