Answer: Polynomial-time solvable in \(\operatorname{poly}(m,\tau,L)\); every valid instance admits a maximum-weight matching with a stable allocation satisfying exact correct division.
Theorem 2.3 — class: algorithmic
Given a finite type set \(T\), rational masses \(\mu_t\), and type-pair eligibility, profits, and split fractions, can one compute a maximum-weight feasible mass matching and a stable cohort allocation satisfying the paper’s \(\varepsilon\)-correct-division condition, or certify that no such outcome exists, in time polynomial in \(\tau\), input bit length \(L\), and \(1/\varepsilon\)?
A society is atomless and given by its support: the list of \(\tau\) types \(T\) with positive binary-rational masses \(\mu_t\), normalized by \(\sum_t\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types.
Input also specifies undirected eligible type pairs \(E\), with \(m=|E|\), binary-rational profits \(w_{tu}\in(0,1]\), split fractions \(r_{tu}\in(0,1)\) satisfying \(r_{ut}=1-r_{tu}\), and binary-rational accuracy \(\varepsilon\in(0,1)\). Same-type pairs are permitted when eligible, with \(r_{tt}=1/2\); \(L\) is the total input bit length.
A feasible mass matching partitions each type into finitely many positive-mass cohorts. Each cohort \(c\) has type \(t(c)\) and mass \(\lambda_c\), with \(\sum_{c:t(c)=t}\lambda_c=\mu_t\), and is either unmatched or paired with a distinct cohort \(p(c)\) of equal mass, with \(p(p(c))=c\) and eligible endpoint types. Every individual participates in at most one trade; matching weight is \(\frac12\sum_{c\text{ matched}}\lambda_c w_{t(c),t(p(c))}\).
A cohort allocation assigns a constant per-person payoff \(g_c\ge0\) to each cohort, with \(g_c=0\) when unmatched and \(g_c+g_{p(c)}=w_{t(c),t(p(c))}\) when matched. Arbitrary finite cohort refinements are allowed.
Stability requires \(g_c+g_d\ge w_{t(c),t(d)}\) for every eligible pair of positive-mass cohorts, including \(c=d\) when same-type trade is eligible.
Define \(A_t=\max\bigl(\{0\}\cup\{(w_{t,t(d)}-g_d)_+:d\text{ is a positive-mass cohort},\ \{t,t(d)\}\in E\}\bigr)\), where \((z)_+=\max(z,0)\). Excluding an individual's current partner removes only a null set, so every eligible positive-mass cohort remains an outside option.
For each matched cohort \(c\), put \(t=t(c)\), \(u=t(p(c))\), and \(S_{tu}=w_{tu}-A_t-A_u\). Additive \(\varepsilon\)-correct division requires \(|g_c-A_t-r_{tu}S_{tu}|\le\varepsilon\); stability and trade feasibility remain exact.
Can one compute a maximum-weight feasible mass matching together with a stable cohort allocation satisfying additive \(\varepsilon\)-correct division, or certify that no such outcome exists, in time \(\operatorname{poly}(m,\tau,L,1/\varepsilon)\), or is this approximation task NP-hard even when \(1/\varepsilon\) is polynomially bounded in the input length?
For finite-agent networks with profits in \((0,1]\), an FPTAS computes an exactly stable, additively \(\varepsilon\)-correct outcome on a maximum-weight matching whenever one exists, and otherwise reports nonexistence. [Kanoria](https://arxiv.org/pdf/1008.0212)
No result settling the finite-support atomless cohort problem defined above was located in the literature search.
Theorem. Every instance satisfying the stated hypotheses admits a maximum-weight feasible mass matching with a stable cohort allocation satisfying exact correct division. Such an outcome can be computed in time \(\operatorname{poly}(m,\tau,L)\), using at most \(2m+\tau\) positive-mass cohorts.
The decisive feature is the specified outside-option rule: the current partner’s positive-mass cohort remains an outside option. Under this rule, stability forces typewise uniform payoffs and zero surplus on every matched pair.
Consider any feasible mass matching with a stable cohort allocation. Since each type has positive mass and finitely many cohorts, define
\(y_t=\min_{c:t(c)=t}g_c\).
For any eligible pair \(\{t,u\}\), apply stability to cohorts attaining these minima. This gives
\(y_t+y_u\ge w_{tu}\).
For a same-type pair, the permitted comparison of a minimum-payoff cohort with itself gives \(2y_t\ge w_{tt}\).
Now let \(c\) and \(p(c)\) be matched cohorts of types \(t\) and \(u\). Trade feasibility and the preceding inequality imply
\[
\text{}
\]
\(w_{tu}=g_c+g_{p(c)}\ge y_t+y_u\ge w_{tu}\).
Consequently, equality holds throughout. Because both \(g_c-y_t\) and \(g_{p(c)}-y_u\) are nonnegative and their sum is zero, we obtain
\(g_c=y_t\) and \(g_{p(c)}=y_u\).
Thus every matched cohort of type \(t\) receives \(y_t\). If that type also has an unmatched cohort, its zero payoff forces \(y_t=0\), so its unmatched cohorts receive the same payoff. If the type has no matched cohorts, all its payoffs are zero.
Therefore every cohort of type \(t\) receives \(y_t\).
By typewise uniformity, the outside option is
\(A_t=\max\bigl(\{0\}\cup\{(w_{tu}-y_u)_+:\{t,u\}\in E\}\bigr)\).
Stability gives \(w_{tu}-y_u\le y_t\), and \(y_t\ge0\). Hence \(A_t\le y_t\).
If type \(t\) participates in a matched pair with type \(u\), the preceding proof gives \(w_{tu}=y_t+y_u\). Its partner’s positive-mass cohort is included among the outside options, so
\(A_t\ge(w_{tu}-y_u)_+=y_t\).
Thus \(A_t=y_t\) for every participating type.
For a type with no matched cohorts, \(y_t=0\), and \(0\le A_t\le y_t\) again gives \(A_t=y_t\).
For every matched pair, therefore,
\(S_{tu}=w_{tu}-A_t-A_u=w_{tu}-y_t-y_u=0\).
It follows that every matched cohort satisfies
\(\left|g_c-A_t-r_{tu}S_{tu}\right|=\left|y_t-y_t-r_{tu}\cdot0\right|=0\).
This proves exact correct division for every prescribed split fraction. It remains to construct a stable allocation on a maximum-weight matching.
Introduce one variable \(x_e\ge0\) for each eligible undirected pair \(e\). It represents the total mass of trades on that pair: a trade of mass \(x_e\) consumes that mass at each endpoint.
Define the incidence coefficient \(B_{te}\) to be \(1\) when \(e\) has two different endpoints and \(t\) is one of them, \(2\) when \(e=\{t,t\}\), and \(0\) otherwise.
Consider the primal linear program
\[
\text{}
\]
\(\displaystyle
\max_{x\ge0}\sum_{e\in E}w_e x_e
\quad\text{subject to}\quad
\sum_{e\in E}B_{te}x_e\le\mu_t
\quad(t\in T).
\)
Every feasible cohort matching gives a feasible primal vector. Aggregate matched cohort pairs by their eligible type pair, counting each paired cohort pair once. The resulting variables consume exactly the corresponding matched type masses. A same-type trade consumes twice its trade mass. Its objective contribution is \(x_e w_e\), agreeing with the question’s weight convention.
Every feasible primal vector gives a feasible cohort matching. For each \(x_e>0\):
For each type, put its remaining mass
\(s_t=\mu_t-\sum_eB_{te}x_e\)
in one unmatched cohort if \(s_t>0\).
These finitely many prescribed cohorts are admissible in the atomless model. Their masses exhaust each type’s mass, and their matching weight is exactly the primal objective. Consequently, the primal optimum equals the maximum feasible mass-matching weight.
The dual linear program is
\[
\text{}
\]
\(\displaystyle
\min_{y\ge0}\sum_{t\in T}\mu_t y_t
\quad\text{subject to}\quad
y_t+y_u\ge w_{tu}
\quad(\{t,u\}\in E).
\)
For same-type pairs, the constraint means \(2y_t\ge w_{tt}\).
The primal is feasible because \(x=0\) is feasible. Its feasible region is bounded: each variable consumes positive mass at an endpoint and is bounded by that endpoint’s mass. Hence its optimum is finite and attained. The dual is feasible because \(y_t=1/2\) for all types satisfies every constraint, using \(w_{tu}\le1\). Linear-programming strong duality therefore provides optimal solutions \(x^*,y^*\) of equal objective value.
Write \(s_t=\mu_t-\sum_e B_{te}x_e^*\). Their zero duality gap has the explicit decomposition
\[
\text{}
\]
\(\displaystyle
0=
\sum_t\mu_t y_t^*-\sum_e w_e x_e^*
=
\sum_t y_t^*s_t+
\sum_{e=\{t,u\}}x_e^*(y_t^*+y_u^*-w_e).
\)
Every summand is nonnegative by primal and dual feasibility. Consequently:
Construct cohorts from \(x^*\) as in Section 3 and assign payoff \(y_t^*\) to every cohort of type \(t\). These implications verify zero payoff on unmatched cohorts and exact trade feasibility on matched cohorts. Nonnegativity follows from dual feasibility.
For any eligible cohorts of types \(t,u\), dual feasibility gives
\(g_c+g_d=y_t^*+y_u^*\ge w_{tu}\).
This includes the required same-cohort comparisons. Thus the allocation is exactly stable.
By Section 2, it also satisfies exact correct division.
Both linear programs have rational data, dimensions bounded by \(m+\tau\), and encoding length polynomial in \(L\). The standard polynomial-time theorem for rational linear programming computes exact rational optimal primal and dual solutions of polynomial encoding length. The cohort construction then uses at most two cohorts per eligible pair and one unmatched cohort per type, giving at most \(2m+\tau\) cohorts.
Thus the running time and output length are polynomial in \(m,\tau,L\), independently of \(1/\varepsilon\). Every valid instance has the required outcome; the nonexistence branch is never needed.
In the finite-agent model, outside options exclude the current partner, as specified in [Kanoria’s definition of edge surplus](https://arxiv.org/pdf/1008.0212). Here the partner’s positive-mass cohort remains available. That distinction makes the zero-surplus argument applicable to the full stated atomless problem.
⟨structured verdict parsed — rendered above⟩
Result: proved. The argument establishes the claimed polynomial-time algorithm for the precise atomless cohort model in USER_TASK. It constructs a maximum-weight feasible mass matching with an exactly stable allocation satisfying exact correct division. I found no mathematical gaps or false steps.
The minimum \(y_t=\min_{c:t(c)=t}g_c\) exists: every type has positive mass, its cohorts exhaust that mass, and the partition is finite.
For distinct eligible types, applying stability to minimum-payoff cohorts correctly gives \(y_t+y_u\ge w_{tu}\). For an eligible same-type pair, the task explicitly permits comparing a cohort with itself, so \(2y_t\ge w_{tt}\) follows. This assumption is used correctly.
For matched cohorts, the chain
\[
w_{tu}=g_c+g_{p(c)}\ge y_t+y_u\ge w_{tu}
\]
forces equality throughout. Since both deviations from the respective minima are nonnegative, each deviation must vanish. This reasoning also covers same-type matched cohorts.
The remaining cases are exhaustive:
Thus the claim that every cohort of type \(t\) receives \(y_t\) is fully justified.
The reduction of the cohort-based outside-option maximum to the stated type-based maximum is valid because every supported type has a positive-mass cohort and all cohorts of that type have the same payoff.
For every eligible neighbor \(u\), stability gives \(w_{tu}-y_u\le y_t\). Because \(y_t\ge0\), taking the positive part preserves the bound:
\[
(w_{tu}-y_u)_+\le y_t.
\]
Consequently, \(A_t\le y_t\).
If type \(t\) participates in a trade with type \(u\), trade feasibility and uniformity give \(w_{tu}=y_t+y_u\). The partner’s positive-mass cohort remains an outside option under the task’s explicit rule. Therefore its contribution to the maximum is exactly \(y_t\), proving \(A_t\ge y_t\).
For a type with no matched cohorts, \(y_t=0\), so the already-established bounds imply \(A_t=0=y_t\). This also handles types with no eligible neighbors.
Hence \(A_t=y_t\) for every type. On each matched pair, \(S_{tu}=0\), and the correct-division error is exactly zero. The conclusion holds for all specified split fractions, including \(r_{tt}=1/2\).
The incidence coefficients correctly represent resource consumption:
Aggregating each paired cohort pair once gives a feasible primal vector. Its objective agrees with the matching weight because the factor \(1/2\) in the task cancels the two matched-cohort contributions for each trade.
The reverse construction is also valid. Every positive variable produces two distinct cohorts of equal positive mass, including when both cohorts have the same type. Primal feasibility makes each residual mass nonnegative, and an unmatched cohort is created only when that residual is positive.
Atomlessness permits the prescribed finite partitions. No integrality or binary-rational restriction is imposed on output cohort masses, so exact rational LP solutions are admissible.
Thus the LP represents all feasible matching weights in both directions. Its optimum is the maximum weight over all feasible mass matchings, as required.
The stated dual is correct. A loop column has coefficient two, yielding the constraint \(2y_t\ge w_{tt}\).
The hypotheses needed for LP strong duality are verified:
The zero-gap decomposition is algebraically correct, including loop contributions. All its summands are nonnegative. Therefore positive residual mass forces zero type payoff, and a positive trade variable forces a tight dual edge constraint.
These implications establish every allocation requirement:
The construction is therefore a stable allocation on a maximum-weight matching. Section 2 then supplies exact correct division without further assumptions.
The invoked rational-LP theorem is stated with the needed conclusion: exact rational optimal primal and dual solutions can be computed in polynomial time with polynomial encoding length. Its hypotheses hold here. The constraint coefficients belong to \(\{0,1,2\}\), and the remaining LP data are rational inputs.
The explicit LP representations have polynomial size in \(m,\tau,L\). Creating the cohorts and computing residual masses require polynomially many rational operations on polynomial-length numbers.
The cohort bound is correct: at most two cohorts per positive edge variable and at most one unmatched cohort per type, hence at most \(2m+\tau\).
The degenerate cases are covered:
Since correct division is exact, the algorithm works for every allowed accuracy and its running time is independent of \(1/\varepsilon\).
The final comparison with Kanoria is accurate: the finite-agent surplus definition excludes the current partner from each endpoint’s alternative set. This is explicit in equation (1) of [Kanoria’s paper](https://arxiv.org/pdf/1008.0212). The task’s atomless outside-option rule retains the partner’s positive-mass cohort, exactly as the proof uses.
No additional mathematical clarification or repair is required. The output resolves the assigned problem under its stated definitions.
⟨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.