← back to the atlas

d4-journals-mss-2023-0027 (d4-journals-mss-2023-0027)

Answer: Polynomial-time solvable. Every original optimal assignment is preserved, and all stated extremum laws extend to cohorts; the changing seller's midpoint formula requires the correction proved above.

The anchor (named result in the paper)

Theorem 4 — class: other

PDF text-layer excerpt — equations and symbol order may be approximateLet seller k ∈M increase his reservation value by 0 ≤c ≤uk, but let all other agents keep their original valuations, so the new pairwise profits (including those with the fictitious players) become a′ kj = (akj −c)+ for all j ∈M0, a′ ij = aij for all i, j ∈M0, i ̸= k.

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

The continuous mirror question, as graded

Given finite seller and buyer type sets \(S,B\), rational masses \(r_s,q_b\), seller reservation values \(s_s\), and buyer valuations \(t_{sb}\), set \(a_{sb}=(t_{sb}-s_s)^+\). Use the mass assignment LP \(\max \sum_{s,b}a_{sb}x_{sb}\), subject to \(\sum_b x_{sb}\le r_s\), \(\sum_s x_{sb}\le q_b\), and \(x_{sb}\ge0\), and its weighted dual \(\min \sum_s r_su_s+\sum_bq_bv_b\), subject to \(u_s+v_b\ge a_{sb}\) and \(u_s,v_b\ge0\). For a seller type \(k\), let \(\underline u_k,\bar u_k\) be the minimum and maximum \(u_k\) over the dual optimal face. When \(0\le c\le\bar u_k\), raise \(s_k\) to \(s_k+c\) for the whole cohort and determine the exact changes in each type’s minimum and maximum stable payoff and their midpoint, including sharp bounds; establish whether Theorem 4’s response laws extend or give the correct replacements.

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

Let \(S,B\) be disjoint, nonempty finite seller and buyer type sets, with \(m=|S|\). A society is given by its support: the list of its \(\tau=|S|+|B|\) types with positive masses \(r_s,q_b\), each encoded as a binary rational; \(\tau\) counts supported types, not possible types. Masses need not sum to one, and the two sides may have unequal total mass. Reservation values \(s_s\) and valuations \(t_{sb}\) are arbitrary rationals; \(L\) is the total input bit length.
Put \(a_{sb}=\max\{t_{sb}-s_s,0\}\). Feasible mass assignments satisfy \(x_{sb}\ge0\), \(\sum_bx_{sb}\le r_s\), and \(\sum_sx_{sb}\le q_b\); their objective is \(\max\sum_{s,b}a_{sb}x_{sb}\).
Stable payoff rates are the optimal solutions of the weighted dual \(\min\{\sum_sr_su_s+\sum_bq_bv_b:u_s+v_b\ge a_{sb},\ u_s,v_b\ge0\}\). Rates are uniform within each type and measured relative to the current reservation values; monetary transfers are unrestricted.
For each seller and buyer, write \(\underline u_s,\bar u_s,\underline v_b,\bar v_b\) for the coordinate minima and maxima over this optimal face, and define midpoints \(\tilde u_s=(\underline u_s+\bar u_s)/2\), \(\tilde v_b=(\underline v_b+\bar v_b)/2\).
Choose \(k\in S\) and rational \(0\le c\le\bar u_k\). Raise the entire cohort's reservation value to \(s_k+c\), leaving all other data fixed: \(a'_{kb}=\max\{a_{kb}-c,0\}\). Primes denote the resulting payoff extrema and midpoints.
Is exact computation of every type's changes in these extrema and midpoints polynomial in \(m,\tau,L\), or NP-hard?
Do the single-seller response laws below, including preservation of every original optimal assignment, extend to this cohort change; if not, what exact response laws and sharp bounds replace them for both sides?
For discrete unit agents, such a single-seller change preserves optimal assignments and gives \(\underline u'_k=\max\{\underline u_k-c,0\}\), \(\bar u'_k=\bar u_k-c\); for \(i\ne k\), \(\underline u_i\le\underline u'_i\le\underline u_i+c\) and \(\bar u'_i=\bar u_i\). Consequently \(\tilde u'_k=\tilde u_k-c+\min\{c,\underline u_k\}/2\) and \(\tilde u_i\le\tilde u'_i\le\tilde u_i+c/2\), with sharp bounds. [Solymosi (2023)](https://unipub.lib.uni-corvinus.hu/9034/1/Sensitivity_of_fair_prices_in_assignment_market_ST_23.pdf).
No result settling this exact cohort sensitivity question was located in the literature search.

Modeling choices made when packaging the task

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

Exact cohort sensitivity is polynomial-time solvable

All the stated assignment-preservation and extremum laws extend to arbitrary positive rational masses. There are also exact shortest-path formulas for every type’s response.

The displayed midpoint formula for the changing seller needs correction, even for unit agents. Its stated extrema imply

\(\displaystyle \tilde u'_k=\tilde u_k-\frac{c+\min\{c,\underline u_k\}}2=\tilde u_k-c+\frac{(c-\underline u_k)_+}{2}.\)

This is the formula in Theorem 4(4) of [Solymosi’s paper](https://unipub.lib.uni-corvinus.hu/9034/1/Sensitivity_of_fair_prices_in_assignment_market_ST_23.pdf). Here and below, \((z)_+=\max\{z,0\}\).

1. The optimal-face identity and preservation of assignments

Let \(V\) denote the original primal optimum and let \(F\) denote the original optimal dual face. Define \(V'\) and \(F'\) analogously.

The primal feasible set is nonempty and compact: the zero assignment is feasible, and every variable is bounded by the corresponding positive capacities. The dual is feasible, for example by taking every seller rate equal to \(\max_{s,b}a_{sb}\) and all buyer rates zero. Strong linear-programming duality therefore gives attained, finite optima.

Moreover, \(F\) is compact. On this face, nonnegativity and positivity of every mass give

\(\displaystyle 0\le u_s\le V/r_s,\qquad 0\le v_b\le V/q_b.\)

Thus all coordinate extrema are attained.

Proposition 1. Under \(0\le c\le\bar u_k\),

\(\displaystyle V'=V-r_kc,\)

and the entire new optimal face is

\(\displaystyle F'=\{(u-ce_k,v):(u,v)\in F,\ u_k\ge c\},\)

where \(e_k\) is the seller-coordinate unit vector.

Proof. Choose an original optimal dual vector satisfying \(u_k\ge c\), which exists because \(c\le\bar u_k\). Subtracting \(c\) from \(u_k\) gives a feasible new dual vector. Indeed, for the changed row:

Its objective is \(V-r_kc\), so \(V'\le V-r_kc\).

For any original optimal assignment \(x\),

\(\displaystyle \sum_{s,b}a'_{sb}x_{sb} =V-\sum_b\min\{a_{kb},c\}x_{kb} \ge V-c\sum_bx_{kb} \ge V-r_kc.\)

Hence \(V'=V-r_kc\). The same calculation applies to every original optimal assignment, proving that each remains optimal.

It also proves that every original optimal dual vector with \(u_k\ge c\), after translation, belongs to \(F'\).

Conversely, if \((u',v')\in F'\), then \((u'+ce_k,v')\) is feasible for the original dual, since

\(\displaystyle u'_k+c+v'_b\ge a'_{kb}+c\ge a_{kb}.\)

Its objective is \(V'+r_kc=V\), so it belongs to \(F\). This proves the face identity. \(\square\)

There is a stronger assignment statement.

Proposition 2. If \(c<\bar u_k\), the original and new optimal-assignment sets are identical. At \(c=\bar u_k\), the new set can be strictly larger.

Proof. Take an original optimal dual vector with \(u_k=\bar u_k\). Its translated new rate satisfies \(u'_k=\bar u_k-c>0\). Complementary slackness with any new optimal assignment \(x'\) therefore gives

\(\displaystyle \sum_bx'_{kb}=r_k.\)

Every positive changed-row entry also satisfies

\(\displaystyle a'_{kb}=u'_k+v'_b>0,\)

so \(a_{kb}>c\). Consequently its original objective is

\(\displaystyle \sum_{s,b}a_{sb}x'_{sb} =\sum_{s,b}a'_{sb}x'_{sb}+r_kc =V.\)

Thus \(x'\) was originally optimal.

For strict enlargement at the endpoint, take one seller and one buyer, both of mass \(2\), with surplus \(A>0\). Originally only \(x=2\) is optimal and \(\bar u_k=A\). At \(c=A\), the new surplus is zero, so every \(0\le x\le2\) is optimal. \(\square\)

2. Simultaneous extrema of the weighted dual

The familiar lattice property continues to hold with arbitrary positive weights.

Lemma 3. If \((u,v)\) and \((U,W)\) belong to \(F\), then both

\(\displaystyle (\min\{u,U\},\max\{v,W\})\)

and

\(\displaystyle (\max\{u,U\},\min\{v,W\})\)

belong to \(F\), with coordinatewise minima and maxima.

Proof. For the first vector, whichever seller rate realizes the minimum is paired with a buyer rate at least as large as its original partner rate. Thus every dual inequality remains satisfied. The second vector is feasible by the symmetric argument, starting from whichever buyer rate realizes the minimum.

Their weighted objectives sum to \(2V\), because coordinatewise minimum plus maximum equals the sum of the original coordinates. Each feasible dual objective is at least \(V\), so both equal \(V\). \(\square\)

Combining finitely many coordinate extremizers using this lemma yields simultaneous optimal vectors

\(\displaystyle (\underline u,\bar v)\in F,\qquad (\bar u,\underline v)\in F.\)

In particular, \((\bar u,\underline v)\) satisfies \(u_k\ge c\). Proposition 1 therefore immediately gives

\(\displaystyle \bar u'_k=\bar u_k-c,\qquad \bar u'_s=\bar u_s\quad(s\ne k),\qquad \underline v'_b=\underline v_b\quad(b\in B).\)

The remaining extrema require understanding the restriction \(u_k\ge c\).

3. A graph giving every exact response

Put

\(\displaystyle \ell_s=\underline u_s,\qquad h_b=\bar v_b,\qquad d=(c-\ell_k)_+.\)

Fix any original optimal assignment \(x^*\). Construct a directed graph on the supported types \(S\cup B\):

\(\displaystyle w_{sb}=\ell_s+h_b-a_{sb}.\)

All lengths are nonnegative, since \((\ell,h)\) is dual feasible. On a positive-support pair, complementary slackness gives \(\ell_s+h_b=a_{sb}\), so the reverse arc \(b\to s\) also has length zero.

Let \(\lambda_j\) be the shortest-path distance from \(k\) to type \(j\), allowing \(\lambda_j=\infty\) when no path exists. Define

\(\displaystyle \rho_j= \begin{cases} (d-\lambda_j)_+,&\lambda_j<\infty,\\ 0,&\lambda_j=\infty. \end{cases}\)

In particular, \(\lambda_k=0\) and \(\rho_k=d\).

Theorem 4. The exact changes are:

| Type | Change in minimum | Change in maximum | Change in midpoint |
|---|---|---|---|
| Seller \(k\) | \(-\min\{c,\ell_k\}\) | \(-c\) | \(-c+d/2\) |
| Seller \(s\ne k\) | \(\rho_s\) | \(0\) | \(\rho_s/2\) |
| Buyer \(b\) | \(0\) | \(-\rho_b\) | \(-\rho_b/2\) |

These formulas hold for every choice of the original optimal assignment \(x^*\).

Proof of the graph formula

For an original optimal vector \((u,v)\), define nonnegative movement coordinates

\(\displaystyle z_s=u_s-\ell_s,\qquad z_b=h_b-v_b.\)

They are nonnegative by the definitions of \(\ell_s\) and \(h_b\).

We first characterize exactly which movement vectors correspond to original dual optima. They satisfy:

For the last condition, an unsaturated seller has \(u_s=\ell_s=0\), while an unsaturated buyer has \(v_b=h_b=0\), by complementary slackness.

The arc \(b\to s\) expresses the original dual inequality:

\(\displaystyle u_s+v_b-a_{sb}=w_{sb}+z_s-z_b\ge0.\)

On a positive-support pair, the two zero-length arcs impose \(z_s=z_b\), which expresses equality in that dual constraint.

Conversely, any movement vector satisfying these conditions produces a nonnegative feasible dual vector

\(\displaystyle u_s=\ell_s+z_s,\qquad v_b=h_b-z_b.\)

It is tight on every positive-support pair and has zero rate at every unsaturated type. Hence it is optimal. Explicitly, the duality gap is

\(\displaystyle \sum_sr_su_s+\sum_bq_bv_b-\sum_{s,b}a_{sb}x^*_{sb} = \sum_su_s\Bigl(r_s-\sum_bx^*_{sb}\Bigr) +\sum_bv_b\Bigl(q_b-\sum_sx^*_{sb}\Bigr) +\sum_{s,b}x^*_{sb}(u_s+v_b-a_{sb}),\)

and every term on the right is zero.

The restriction \(u_k\ge c\) is equivalent to \(z_k\ge d\). Along any directed path from \(k\) to \(j\) of length \(D\), the arc inequalities imply

\(\displaystyle z_j\ge z_k-D\ge d-D.\)

Together with nonnegativity, this gives \(z_j\ge\rho_j\) for every vector in the restricted face.

We now prove that \(z=\rho\) itself is admissible. For any arc \(i\to j\) of length \(w\), the shortest-path inequality gives

\(\displaystyle \lambda_j\le\lambda_i+w\)

whenever \(\lambda_i\) is finite. Since \(w\ge0\), it follows that

\(\displaystyle \rho_j\ge\rho_i-w.\)

If \(\lambda_i=\infty\), then \(\rho_i=0\), so the same inequality follows from \(\rho_j\ge0\).

It remains to check buyer upper bounds and forced-zero coordinates. The restricted face is nonempty: it contains \((\bar u,\underline v)\). Let \(\widehat z\) be its movement vector. The preceding path argument shows \(\rho_j\le\widehat z_j\) for every \(j\). Therefore \(\rho_b\le h_b\), and every forced-zero coordinate of \(\rho\) is zero. Also \(\rho_k=d\).

Thus \(\rho\) is the coordinatewise least admissible movement vector satisfying the restriction. Consequently the restricted original face has simultaneous seller minima and buyer maxima

\(\displaystyle u_s=\ell_s+\rho_s,\qquad v_b=h_b-\rho_b.\)

Translate its \(k\)-coordinate by Proposition 1. This proves every entry of the table. \(\square\)

4. Response laws and sharp bounds on both sides

For the changing seller, Theorem 4 gives exactly

\(\displaystyle \underline u'_k=(\underline u_k-c)_+,\qquad \bar u'_k=\bar u_k-c,\)

and the corrected midpoint law

\(\displaystyle \tilde u'_k=\tilde u_k-c+\frac{(c-\underline u_k)_+}{2}.\)

For every other seller,

\(\displaystyle 0\le\underline u'_s-\underline u_s\le d,\qquad \bar u'_s=\bar u_s,\qquad 0\le\tilde u'_s-\tilde u_s\le d/2.\)

For every buyer,

\(\displaystyle \underline v'_b=\underline v_b,\qquad 0\le\bar v_b-\bar v'_b\le d,\qquad -d/2\le\tilde v'_b-\tilde v_b\le0.\)

Since \(d\le c\), these include the quoted bounds for other sellers. The strengthened bounds show that no other type’s extrema change when \(c\le\underline u_k\).

The original coordinate widths give further bounds:

\(\displaystyle \rho_s\le\min\{d,\bar u_s-\underline u_s\},\qquad \rho_b\le\min\{d,\bar v_b-\underline v_b\}.\)

The two sides also satisfy the exact weighted balance identity

\(\displaystyle \sum_sr_s\rho_s=\sum_bq_b\rho_b.\)

Indeed, \((\ell+\rho,h-\rho)\) and \((\ell,h)\) are both original dual optima. Equivalently,

\(\displaystyle \sum_bq_b(\bar v_b-\bar v'_b) = r_kd+\sum_{s\ne k}r_s(\underline u'_s-\underline u_s).\)

Sharpness with a genuine cohort

Take sellers \(k,i\) of masses \(2,1\), and one buyer \(b\) of mass \(3\). Choose \(\alpha>0\), \(\beta\ge0\), and surpluses

\(\displaystyle a_{kb}=\alpha+\beta,\qquad a_{ib}=\alpha.\)

The assignment \(x_{kb}=2,\ x_{ib}=1\) is optimal: it attains the upper bound obtained by selling every seller’s capacity at its row surplus. Complementary slackness characterizes the entire dual optimal face by

\(\displaystyle u_k+v_b=\alpha+\beta,\qquad u_i+v_b=\alpha,\qquad 0\le v_b\le\alpha.\)

Therefore

\(\displaystyle \underline u_k=\beta,\quad \bar u_k=\alpha+\beta,\quad \underline u_i=0,\quad \bar u_i=\alpha,\quad \underline v_b=0,\quad \bar v_b=\alpha.\)

For any \(0\le c\le\alpha+\beta\), put \(d=(c-\beta)_+\). After the change, complementary slackness with the preserved assignment gives

\(\displaystyle u'_k+v'_b=\alpha+\beta-c,\qquad u'_i+v'_b=\alpha,\qquad 0\le v'_b\le\alpha-d.\)

Thus

\(\displaystyle \underline u'_i-\underline u_i=d,\qquad \tilde u'_i-\tilde u_i=d/2,\qquad \bar v_b-\bar v'_b=d,\qquad \tilde v_b-\tilde v'_b=d/2.\)

This attains all strengthened upper bounds, with changing-cohort mass \(2\). Taking \(\beta=0\) attains the original bounds \(c\) and \(c/2\).

For the zero endpoints, take two independent pairs with masses

\(\displaystyle r_k=q_{b_k}=2,\qquad r_i=q_{b_i}=1,\)

diagonal surpluses \(\alpha>0\), and cross surpluses zero. Each pair’s optimal-face condition is \(u+v=\alpha\); the cross inequalities impose no additional restriction. Changing row \(k\) by \(0<c<\alpha\) leaves every extremum and midpoint of \(i\) and \(b_i\) unchanged.

Finally, the changing seller’s midpoint satisfies

\(\displaystyle -c\le\tilde u'_k-\tilde u_k\le-c/2.\)

The first example attains the left endpoint when \(\beta\ge c\), and the right endpoint when \(\beta=0\). Hence these bounds are sharp as well.

5. Exact polynomial-time computation

Use the standard rational linear-programming theorem: a feasible rational linear program with finite optimum can be optimized exactly, with a rational optimal solution, in polynomial bit complexity.

Its hypotheses hold here as established above. An exact algorithm is:

\(\displaystyle \sum_sr_su_s+\sum_bq_bv_b=V\)
to the dual constraints. Minimize and maximize each coordinate over this face, using \(2\tau\) linear programs.

The primal has \(m|B|\) variables. The coordinate programs have \(\tau\) variables and polynomially many constraints. All have rational descriptions of polynomial bit length in the input.

The graph has \(\tau\) vertices and at most \(2m|B|\) arcs. Its lengths have polynomial bit length. Because lengths are nonnegative, every finite shortest distance has a simple-path representative using at most \(\tau-1\) arcs. Exact shortest-path arithmetic therefore also has polynomial bit complexity.

Thus the complete computation is polynomial in \(m,\tau,L\). No normalization of masses, equality of total masses, or expansion into unit agents is required.

⟨structured verdict parsed — rendered above⟩

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

Verdict

The output proves the target result. Exact cohort sensitivity is polynomial-time computable, every original optimal assignment is preserved, and the stated extremum laws extend to arbitrary positive rational masses. The graph formulas correctly give the responses on both sides.

The prover also correctly identifies an algebraic error in the task’s changing-seller midpoint formula. No major or minor mathematical gaps were found.

Step-by-step verification

1. Existence, attainment, and compactness

The primal feasible set is nonempty and compact: the zero assignment is feasible, and each coordinate satisfies \(0\le x_{sb}\le\min\{r_s,q_b\}\).

The proposed dual vector is feasible because all surpluses are nonnegative and bounded by their finite maximum. The application of finite-dimensional linear-programming strong duality is justified: primal feasibility and boundedness give a finite attained primal optimum, and the dual has the same attained optimum.

On the optimal dual face, positivity of every mass and nonnegativity of every rate imply the stated coordinate bounds. The face is also closed, so it is compact and every coordinate extremum is attained. This reasoning includes the case \(V=0\).

Assessment: Correct.

2. Proposition 1: value change and optimal-face identity

The assumption \(c\le\bar u_k\), together with attainment, supplies an original optimum with \(u_k\ge c\).

Subtracting \(c\) from that coordinate preserves nonnegativity. The two cases \(a_{kb}\ge c\) and \(a_{kb}<c\) correctly verify every changed-row constraint. The translated objective is \(V-r_kc\), giving the required upper bound on \(V'\).

For every original optimal assignment, the objective calculation is exact. Both subsequent inequalities have the correct direction because
\(\min\{a_{kb},c\}\le c\) and \(\sum_bx_{kb}\le r_k\). Thus every such assignment has new objective at least \(V-r_kc\). Combining this with the dual upper bound establishes both the value identity and preservation of every original optimum.

For the converse face inclusion, adding \(c\) to the new seller coordinate restores feasibility because \(a'_{kb}+c\ge a_{kb}\). Its objective becomes \(V\), so it is an original dual optimum satisfying \(u_k\ge c\).

Assessment: Correct; the face identity holds in both directions.

3. Proposition 2: equality of assignment sets below the endpoint

For \(c<\bar u_k\), the translated dual optimum has strictly positive changed-seller rate. Complementary slackness with any new optimal assignment therefore forces that seller’s capacity to be saturated.

Complementary slackness also makes every used changed-row constraint tight. Its right-hand side is strictly positive because the changed-seller rate is positive and buyer rates are nonnegative. Hence every used changed-row surplus satisfies \(a_{kb}>c\), and restoring the original objective adds exactly \(r_kc\).

This establishes the claimed reverse inclusion of assignment sets.

The endpoint example is valid: with one seller and one buyer of mass \(2\), positive surplus gives the unique optimal mass \(2\); reducing the surplus to zero makes every feasible mass optimal.

Assessment: Correct, including the strict endpoint distinction.

4. Lemma 3: weighted lattice property

Both coordinatewise combinations are feasible. For each constraint, the coordinate taking the minimum can be paired with an opposite-side coordinate at least as large as its value in the corresponding original vector.

The sum of the two weighted objectives is exactly \(2V\), independently of whether the weights are equal. Since each feasible objective is at least \(V\), both combinations are optimal.

Attained coordinate extrema and finitely many applications of the lemma yield the two simultaneous extremal vectors. The seller-maximal, buyer-minimal vector satisfies the restriction \(u_k\ge c\); consequently, the unchanged maxima and buyer minima follow directly from the face identity.

Assessment: Correct; no equal-mass assumption is hidden here.

5. Graph construction and movement-vector characterization

The arc lengths are nonnegative by feasibility of \((\ell,h)\). On every positive-support pair of \(x^*\), complementary slackness makes the corresponding length zero.

The movement coordinates are nonnegative by the definitions of seller minima and buyer maxima. The buyer upper bounds are exactly the conditions needed for nonnegative buyer rates.

The arc inequalities correctly encode dual feasibility. On positive-support pairs, the two zero-length arcs impose the equality required by complementary slackness.

For an unsaturated seller, complementary slackness forces its rate to zero at every dual optimum, hence also \(\ell_s=0\). For an unsaturated buyer, it similarly forces every buyer rate, including \(h_b\), to zero. Thus the forced-zero movement conditions are justified.

Conversely, the displayed duality-gap identity is correct. Every term vanishes under the listed conditions, proving optimality of the reconstructed vector.

Assessment: The characterization is necessary and sufficient.

6. Shortest-path formula and Theorem 4

Within the nonnegative movement domain, the restriction \(u_k\ge c\) is indeed equivalent to \(z_k\ge d\), including when \(c\le\ell_k\).

Summing arc inequalities along a path gives the stated coordinate lower bound. Taking shortest distances and imposing nonnegativity yields \(z_j\ge\rho_j\). Unreachable vertices contribute only the nonnegativity bound.

The shortest-path inequality verifies every arc condition for \(\rho\). The separate treatment of an unreachable arc source is correct.

The restricted face is nonempty because it contains the seller-maximal, buyer-minimal optimum. Its movement vector dominates \(\rho\), which verifies all buyer upper bounds and forced-zero conditions for \(\rho\). Also, \(\rho_k=d\).

Therefore \(\rho\) is an admissible coordinatewise least movement vector. It simultaneously realizes restricted seller minima and buyer maxima. Translating the changed coordinate gives every entry of the response table.

Because the characterization was established for an arbitrary original optimal assignment, the formulas are valid for every allowed choice of \(x^*\).

Assessment: Correct.

7. Midpoint correction

Averaging the proved changing-seller extrema gives exactly
\[ \tilde u'_k-\tilde u_k =-\frac{c+\min\{c,\underline u_k\}}{2} =-c+\frac{(c-\underline u_k)_+}{2}. \]

The task’s displayed midpoint expression is inconsistent with its own extrema. Correcting it is necessary to answer the task accurately.

The attribution to Theorem 4(4) is also accurate: the cited paper states the corrected expression. The cohort argument itself does not rely on extending the paper’s discrete theorem. [Solymosi, Theorem 4](https://unipub.lib.uni-corvinus.hu/9034/1/Sensitivity_of_fair_prices_in_assignment_market_ST_23.pdf).

Assessment: Correct correction, not a defect in the prover’s argument.

8. Bounds, balance identity, and sharpness

Nonnegative path lengths give \(0\le\rho_j\le d\), establishing the response bounds on both sides. Admissibility in the original optimal face gives the additional coordinate-width bounds.

When \(c\le\underline u_k\), \(d=0\), so the claim that every other type’s extrema remain unchanged follows directly.

The weighted balance identity follows by subtracting the objectives of the two explicitly established original optima. Its rewritten form correctly includes \(\rho_k=d\).

The sharpness examples check out:

Assessment: Correct calculations and valid sharpness examples with cohort mass greater than one.

9. Exact polynomial-time computation

The rational linear-programming theorem is stated in the relevant exact bit-complexity form. Its hypotheses hold for the original primal and all coordinate programs: their feasible sets are nonempty and their objectives have finite attained optima.

The number of variables, constraints, and coordinate programs is polynomial in the supported-type counts. Standard rational LP output bounds ensure that \(V\), \(x^*\), and the extrema have polynomial encoding length, so adding the optimal-value equality and constructing the graph preserves polynomial input size.

The graph has the stated polynomial size. Nonnegative lengths permit a simple representative for each finite shortest distance, with at most \(\tau-1\) arcs. Exact distance arithmetic and the final rational response calculations therefore have polynomial bit complexity.

Assessment: Correct. The algorithm does not expand binary-encoded masses into unit agents.

Required clarification or repair

None. The output settles both the computational question and the cohort response laws under the task’s stated assumptions.

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