← back to the atlas

d4-journals-geb-2020-0123 (d4-journals-geb-2020-0123)

Answer: \(\text{Polynomial-time solvable}\)

The anchor (named result in the paper)

Proposition 1 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateThe deferred acceptance algorithm has the following properties: 1. It stops after a finite number of rounds. 2. It outputs a pairwise stable allocation. 3. Price Determination program (I) outputs the pointwise minimum price function at which M is stable. 4.

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

The continuous mirror question, as graded

Given finite firm and worker type sets \(B\) and \(S\), rational masses \(\mu_b,\mu_s\), type values and reservation wages \(v_b,c_s\), and an allowed-link relation \(E\subseteq B\times S\), compute a mass matching \(x_{bs}\geq 0\) satisfying \(\sum_{s:(b,s)\in E}x_{bs}\leq\mu_b\) and \(\sum_{b:(b,s)\in E}x_{bs}\leq\mu_s\), together with supporting wages for its matched mass, so that no linked firm and worker tranche can mutually benefit by rematching. For the returned matching, compute the minimum and maximum supporting wage for each active type pair.

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

Let \(B,S\) be nonempty, disjoint finite sets of firm and worker types, with values \(v_b,c_s\in\mathbb Q\) and allowed links \(E\subseteq B\times S\). Values and wages may have either sign.
A society is given by its support: the list of its \(\tau=|B|+|S|\) types with positive binary-rational masses \(\mu_b,\mu_s\). Masses need not sum to one or balance between sides; \(\tau\) counts supported types, not possible types. Set \(m=|E|\), and let \(L\) be the total input bit length.
A mass matching has \(x_{bs}\geq0\) on \(E\), with \(\sum_s x_{bs}\leq\mu_b\) and \(\sum_b x_{bs}\leq\mu_s\). Each active pair \(x_{bs}>0\) receives one wage \(w_{bs}\in[c_s,v_b]\), paid uniformly on that pair's matched mass.
A matched firm tranche earns \(v_b-w_{bs}\); a matched worker tranche receives \(w_{bs}\). Unmatched firms earn zero and unmatched workers receive \(c_s\). Tranches may leave existing partners to rematch.
Every tranche of type \(b\) can match every tranche of type \(s\) when \((b,s)\in E\). Stability excludes two currently unpaired, positive-mass linked tranches that can both strictly improve at some new wage; indifference does not block.
Equivalently, assign each firm tranche its current wage, or \(v_b\) if unmatched, and each worker tranche its current wage, or \(c_s\) if unmatched: for every linked pair of tranche statuses with positive mass, the firm's assigned number must not exceed the worker's.
Compute a stable matching and supporting wages, and, keeping that matching fixed, the minimum and maximum of each active pair's wage over all its supporting wage profiles.

Is this exact computational problem solvable in polynomial time in \(m,\tau,L\), or is it NP-hard?

For finite agents with a common reservation value and grid-valued firm values, a terminating deferred-acceptance procedure returns a stable allocation and its pointwise minimum and maximum supporting prices; the stated result does not establish a polynomial bound in binary input length. [Source](https://mpra.ub.uni-muenchen.de/66999/1/MPRA_paper_66999.pdf)
No complexity result for exactly the support-encoded mass problem above was located.

Modeling choices made when packaging the task

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

1. Result

The exact problem is polynomial-time solvable in \(m,\tau,L\). Three rational linear programs suffice: one computes the matching, and two compute supporting wage profiles that simultaneously attain every active pair’s minimum and maximum wage.

The key is that the stated tranche-level stability condition forces a common assigned number for every type. This identifies stable outcomes with primal–dual optimal solutions of a maximum-surplus matching LP.

2. Stability forces a common assigned number within each type

Fix a feasible matching \(x\). Define its active links and unmatched masses by

\(A(x)=\{(b,s)\in E:x_{bs}>0\}\),

\(r_b=\mu_b-\sum_{s:(b,s)\in E}x_{bs}\), and \(r_s=\mu_s-\sum_{b:(b,s)\in E}x_{bs}\).

Suppose wages support stability.

If \((b,s)\) and \((b,t)\) are active, compare the firm tranche matched to \(t\) with the worker tranche of type \(s\). The stated stability inequality gives \(w_{bt}\leq w_{bs}\). Reversing the roles gives \(w_{bs}\leq w_{bt}\). Thus all active wages incident to a firm type coincide.

Similarly, if \((b,s)\) and \((d,s)\) are active, comparing the firm tranche of type \(b\) with the worker tranche matched to \(d\) gives \(w_{bs}\leq w_{ds}\), and the reverse comparison gives equality. All active wages incident to a worker type therefore coincide.

If \(r_b>0\) and \((b,s)\) is active, comparing an unmatched firm tranche with a matched worker tranche gives \(v_b\leq w_{bs}\). Individual rationality gives \(w_{bs}\leq v_b\), so \(w_{bs}=v_b\).

Likewise, if \(r_s>0\) and \((b,s)\) is active, stability gives \(w_{bs}\leq c_s\), while individual rationality gives the reverse inequality. Hence \(w_{bs}=c_s\).

Consequently, every positive-mass status of type \(t\) has the same assigned number, denoted \(p_t\). A completely unmatched firm has \(p_b=v_b\), and a completely unmatched worker has \(p_s=c_s\).

It follows that supporting wage profiles correspond exactly to vectors in the following polyhedron \(Q(x)\):

The necessity of these constraints follows from the preceding comparisons and the stated stability inequality.

For sufficiency, take any \(p\in Q(x)\) and assign \(w_{bs}=p_b=p_s\) on every active link. The first constraints guarantee \(c_s\leq w_{bs}\leq v_b\). The unmatched-mass equalities ensure that every positive-mass tranche of type \(t\) has assigned number \(p_t\). Finally, \(p_b\leq p_s\) on every allowed link is precisely the stability condition supplied in the question.

Thus \(Q(x)\) describes all supporting wage profiles, without restricting their possible variation beyond what stability itself requires.

3. Computing a supportable matching by linear programming

Put \(a_{bs}=v_b-c_s\). Consider the primal LP \(P\):

\( \displaystyle \text{maximize } W(x)=\sum_{(b,s)\in E}a_{bs}x_{bs} \),

subject to

Its dual \(D\) is

\( \displaystyle \text{minimize } F(u)=\sum_{t\in B\cup S}\mu_tu_t \),

subject to \(u_t\geq0\) for every type and

\(u_b+u_s\geq a_{bs}\qquad((b,s)\in E)\).

The primal is feasible because \(x=0\) is feasible. Its feasible region is compact: each variable lies between zero and \(\min\{\mu_b,\mu_s\}\). The dual is also feasible: take all worker variables to be zero and all firm variables to equal

\(K=\max\bigl(\{0\}\cup\{a_{bs}:(b,s)\in E\}\bigr)\).

Therefore strong LP duality applies: optimal solutions exist and their objective values coincide. This is the standard finite-dimensional [LP duality theorem](https://courses.csail.mit.edu/6.854/18/Notes/n12-duality.html).

For completeness, the relevant complementary-slackness conditions follow directly from the gap identity. For any primal-feasible \(x\) and dual-feasible \(u\),

\( \displaystyle F(u)-W(x)=\sum_{t\in B\cup S}r_tu_t+\sum_{(b,s)\in E}x_{bs}(u_b+u_s-a_{bs}). \)

To verify this identity, substitute \(r_b=\mu_b-\sum_sx_{bs}\) and \(r_s=\mu_s-\sum_bx_{bs}\), and collect the coefficient of each \(x_{bs}\).

Every term on the right is nonnegative. Hence, for any optimal \(x\) and optimal \(u\),

\(r_tu_t=0\) for every type, and \(u_b+u_s=a_{bs}\) on every active link.

Now define

\(p_b=v_b-u_b\), and \(p_s=c_s+u_s\).

Nonnegativity of \(u\) gives \(p_b\leq v_b\) and \(p_s\geq c_s\). Dual feasibility gives

\(p_b\leq p_s\qquad((b,s)\in E)\).

On active links, complementary slackness gives \(p_b=p_s\). If \(r_b>0\), it gives \(u_b=0\), hence \(p_b=v_b\); if \(r_s>0\), it gives \(p_s=c_s\).

Thus \(p\in Q(x)\). By Section 2, every optimal solution of \(P\) admits supporting stable wages.

Conversely, a stable outcome yields \(p\in Q(x)\). Set \(u_b=v_b-p_b\) and \(u_s=p_s-c_s\). These variables are dual-feasible, and all terms in the gap identity vanish. Weak duality then proves that \(x\) and \(u\) are optimal.

We have therefore proved the exact characterization: the supportable matchings are precisely the optimal solutions of \(P\).

4. Exact wage extrema for the fixed matching

Fix the optimal matching \(x\) computed above. We have proved that \(Q(x)\) is nonempty.

It is also compact. It is closed because its defining constraints are non-strict linear equalities and inequalities. To establish boundedness, consider any type:

Every coordinate therefore has finite bounds.

Moreover, \(Q(x)\) is closed under coordinatewise minimum and maximum. Indeed, for \(p,q\in Q(x)\), define

\((p\wedge q)_t=\min\{p_t,q_t\}\), and \((p\vee q)_t=\max\{p_t,q_t\}\).

Constant bounds, fixed-coordinate equalities, and active-link equalities are preserved by both operations. For an allowed-link inequality, \(p_b\leq p_s\) and \(q_b\leq q_s\) imply

\(\min\{p_b,q_b\}\leq\min\{p_s,q_s\}\)

and

\(\max\{p_b,q_b\}\leq\max\{p_s,q_s\}\).

Thus both new vectors belong to \(Q(x)\).

Compute \(p^{-}\) by minimizing \(\sum_t p_t\) over \(Q(x)\). Compactness guarantees an optimizer. This optimizer is componentwise least: if some \(q\in Q(x)\) had \(q_j<p^{-}_j\), then \(p^{-}\wedge q\) would be feasible, would not increase any coordinate, and would strictly decrease coordinate \(j\). Its coordinate sum would be smaller, contradicting optimality.

Similarly, maximizing \(\sum_t p_t\) over \(Q(x)\) produces a componentwise greatest vector \(p^{+}\).

Hence every active pair has the exact wage bounds

\(\min w_{bs}=p^{-}_b=p^{-}_s\), and \(\max w_{bs}=p^{+}_b=p^{+}_s\).

Both endpoint wage profiles support the same fixed matching \(x\). In particular, the minima are simultaneously attainable, as are the maxima.

5. Algorithm and binary-input complexity

The algorithm is:

The standard rational-LP complexity theorem provides exact rational optimizers in time polynomial in the number of variables, constraints, and total binary encoding length; it also bounds the output encoding length polynomially. See the discussion of polynomial algorithms and exact optimum recovery in [MIT’s LP algorithm notes](https://courses.csail.mit.edu/6.854/18/Notes/n14-LP_algorithms.html).

Here \(P\) has \(m\) variables and \(O(m+\tau)\) constraints. Its coefficients are input masses, differences \(v_b-c_s\), and zeros or ones, so its encoding length is polynomial in \(m,\tau,L\).

The returned \(x\) has polynomial encoding length. Exact rational arithmetic therefore computes \(A(x)\), the residual masses, and their zero tests in polynomial time. Each wage LP has \(\tau\) variables and \(O(m+\tau)\) constraints, with coefficients drawn from \(v_b,c_s\) and \(\{-1,0,1\}\). Their encoding lengths are likewise polynomial.

All three LPs are feasible and bounded, as proved above. Consequently, the algorithm and its exact output have polynomial bit complexity.

The proof permits either sign for values and wages and requires no normalization or balance of masses. If \(m=0\), the empty matching is stable and there are no active wage bounds to report.

⟨structured verdict parsed — rendered above⟩

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

Verification report

Verdict: proved. The output resolves the requested computational problem. The stability characterization, primal–dual correspondence, simultaneous wage extrema, and polynomial bit complexity are correct. No major or minor mathematical issues were found.

The argument uses the explicit tranche-status inequality supplied in USER_TASK, allows signed values and wages, and operates on supported types and rational masses without expanding masses into individual agents.

1. Common assigned numbers within types

The comparisons in Section 2 are valid.

For two distinct active links incident to the same firm type, the firm tranche matched along one link and the worker tranche matched along the other have positive mass and are currently unpaired. Both required links are allowed. Stability therefore supplies the two opposing wage inequalities, yielding equality. Comparing an active link with itself requires no stability argument: the wages already coincide.

The corresponding worker-type argument also uses positive-mass, currently unpaired tranches and allowed links. Its inequality directions are correct.

When a firm has positive unmatched mass and an active incident link, stability gives \(v_b\leq w_{bs}\), while the required wage interval gives \(w_{bs}\leq v_b\). The worker counterpart correctly gives \(w_{bs}=c_s\).

These cases exhaust the positive-mass statuses of each supported type. A type with no active link is completely unmatched because its mass is positive. Thus the assigned number \(p_t\) is well defined for every supported type.

Finding: correct, including partially unmatched and completely unmatched types.

2. Exact description of supporting wages

Every constraint defining \(Q(x)\) is necessary:

The sufficiency argument also checks every requirement. On an active link, \(p_b=p_s\), together with the endpoint bounds, places the wage in \([c_s,v_b]\). The unmatched-mass constraints ensure that unmatched statuses receive their prescribed assigned numbers. The remaining allowed-link inequalities then enforce the stated stability condition for every positive-mass status comparison.

There are no unused type coordinates that could invalidate the correspondence: every type has positive mass and therefore at least one positive-mass status.

Finding: \(Q(x)\) describes all supporting wage profiles for the fixed matching.

3. Matching LP, duality, and optimality

The primal constraints reproduce precisely the mass-matching constraints. Its objective coefficients \(a_{bs}=v_b-c_s\) are rational and may have either sign.

The stated dual is correct. Each matching variable participates in its firm and worker capacity constraints, producing the dual inequality \(u_b+u_s\geq a_{bs}\). The capacity-inequality directions correctly require nonnegative dual variables.

The existence arguments satisfy the hypotheses of finite-dimensional LP duality:

The cited strong-duality result applies to this feasible primal–dual pair and yields attained, equal finite optimal values. The relevant statement is supported by the linked [MIT duality notes](https://courses.csail.mit.edu/6.854/18/Notes/n12-duality.html).

The displayed gap identity is correct. Expanding the residual-mass terms gives
\[ \sum_t r_tu_t = \sum_t\mu_tu_t-\sum_{(b,s)\in E}x_{bs}(u_b+u_s), \]
which yields exactly the asserted identity after adding the edge-slack terms.

All terms are nonnegative. Consequently, for any primal optimum and any dual optimum, each residual-mass product vanishes and every active edge has zero dual slack. No special selection of compatible optimal solutions is needed.

The substitutions \(p_b=v_b-u_b\) and \(p_s=c_s+u_s\) correctly translate dual feasibility and these equalities into every constraint of \(Q(x)\).

Conversely, a vector in \(Q(x)\) gives nonnegative, dual-feasible variables under the inverse substitutions. Every term of the gap identity vanishes. Equality of feasible primal and dual objective values then certifies both solutions as optimal.

Finding: the characterization of supportable matchings as exactly the primal optima is established in both directions.

4. Wage extrema for the fixed matching

The proof of compactness of \(Q(x)\) is complete. Closedness follows from its finite system of non-strict linear constraints. For a type incident to an active edge, that edge supplies both finite coordinate bounds. For a type with no active edge, positive mass fixes its coordinate to its outside option.

Closure under coordinatewise minimum and maximum is also correct. Constant bounds, fixed coordinates, and active-edge equalities are preserved. The two displayed order inequalities correctly show that allowed-link inequalities are preserved as well.

The sum-minimization argument establishes a componentwise least vector, rather than merely a vector with the smallest coordinate sum. If another feasible vector lowered any coordinate, its coordinatewise minimum with the optimizer would remain feasible and strictly lower the sum. The analogous maximum argument is valid.

Since an active wage equals both endpoint coordinates, these least and greatest vectors yield each active pair’s exact minimum and maximum wage. Their membership in the same \(Q(x)\) establishes simultaneous attainability while keeping the matching fixed.

Finding: the two wage LPs compute precisely the extrema requested.

5. Exact polynomial complexity and edge cases

The rational-LP theorem invoked in Section 5 is stated at the needed level: exact rational optimizers with polynomial output length can be computed in polynomial time for explicitly encoded rational LPs with finite attained optima. Its hypotheses hold for all three optimization problems. The cited [MIT algorithm notes](https://courses.csail.mit.edu/6.854/18/Notes/n14-LP_algorithms.html) discuss polynomial algorithms, coordinate bit bounds, and recovery of optimal vertices.

The encoding analysis is sound:

The algorithm requires only the claimed three LP optimizations. The dual is used to establish existence of supporting wages; computing a dual optimum separately is unnecessary.

Signed values and wages do not invalidate any bound or substitution. Unequal or unnormalized masses do not affect feasibility, duality, or the complexity analysis. Isolated types are covered by the completely unmatched case. The case \(m=0\) is explicitly handled and has no active wage extrema to report.

Finding: exact polynomial time in \(m,\tau,L\), including polynomial output length, is established.

Required feedback

No repair or additional clarification is needed. The write-up establishes the full target, including simultaneous attainment of the wage extrema for its returned matching.

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