← back to the atlas

d4-conf-atal-2015-0289 (d4-conf-atal-2015-0289)

Answer: The existence decision problem is in \(\mathrm{P}\). Every valid input admits a core-stable mass partition with at most \(\tau\) nonzero coalition vectors.

The anchor (named result in the paper)

Theorem 5(i) — class: hardness

The continuous mirror question, as graded

Given a finite type set \(T\), rational masses \(\mu_t\ge 0\) summing to \(1\), and a symmetric rational affinity matrix \(w_{ts}=w_{st}\), decide whether there is a countable family of nonzero coalition mass vectors \(x^j\in\mathbb{R}_{\ge 0}^{T}\) and isolated mass \(\sigma_t\ge 0\), with \(\sigma_t+\sum_j x_t^j=\mu_t\), such that no nonzero composition \(y\in\mathbb{R}_{\ge 0}^{T}\) can be formed from positive masses of every type \(t\) with \(y_t>0\) whose current utility is strictly below \(u_t(y)=\frac{\sum_s w_{ts}y_s}{\sum_s y_s}\). Is such a core-stable mass partition guaranteed to exist?

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

A society is given by its support \(T\): the list of \(\tau=|T|\) types with positive binary rational masses \(\mu_t\), summing to \(1\). The input also contains a symmetric matrix \(w\in\mathbb{Q}^{T\times T}\), with either sign allowed. Its diagonal describes affinity between distinct individuals of the same type; isolated individuals receive utility \(0\).
A mass partition consists of a finite or countable family of nonzero vectors \(x^j\in\mathbb{R}_{\ge0}^{T}\) and isolated masses \(\sigma_t\ge0\), satisfying \(\sigma_t+\sum_jx_t^j=\mu_t\). Type \(t\) mass in coalition \(z\ne0\) receives \(u_t(z)=\frac{\sum_s w_{ts}z_s}{\sum_s z_s}\).
Mass is divisible. For a proposed coalition \(y\in\mathbb{R}_{\ge0}^{T}\setminus\{0\}\), define its available strictly improving mass by \(B_t(y)=\sigma_t\mathbf{1}_{\{u_t(y)>0\}}+\sum_{j:u_t(x^j)<u_t(y)}x_t^j\). It blocks precisely when \(y_t\le B_t(y)\) for every \(t\).
A partition is core stable if no coalition blocks and \(u_t(x^j)\ge0\) whenever \(x_t^j>0\), since individuals may also leave to become isolated. Indifference never suffices for blocking. Measure running times in \(\tau\) and total binary input length \(L\).

Is deciding whether a core-stable mass partition exists in \(\mathrm{P}\), or is it \(\mathrm{NP}\)-hard? Does every input admit such a partition?

For finite agents, deciding existence of a core-stable partition in symmetric fractional hedonic games is \(\mathrm{NP}\)-hard; existence can fail even with symmetric zero/one valuations. [Brandl, Brandt, and Strobel](https://brandlf.com/docs/fhg_stability.pdf).
No result settling this exact divisible-mass model was identified in the literature search.

Modeling choices made when packaging the task

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

Result

Every valid input admits a core-stable mass partition. Consequently, deciding existence is in \(\mathrm{P}\): every valid instance has answer YES.

More strongly, there is always such a partition with at most \(\tau\) nonzero coalition vectors. The proof does not require symmetry of \(w\).

The main ingredients are Scarf’s lemma for a finite collection of coalition compositions and a compactness argument that preserves stability under strict blocking.

1. Normalized compositions and blocking

Write

\(\displaystyle \Delta=\left\{p\in\mathbb{R}_{\geq 0}^{T}:\sum_{t\in T}p_t=1\right\}.\)

Every nonzero coalition can be written uniquely as \(y=cp\), where \(c>0\) and \(p\in\Delta\). Its utilities satisfy

\(\displaystyle u_t(cp)=(wp)_t.\)

Thus utilities, and consequently the available strictly improving masses, depend only on the composition \(p\), not on \(c\).

For a fixed partition, define

\(\displaystyle b_t(p)=\sigma_t\mathbf{1}_{\{(wp)_t>0\}}+\sum_{j:u_t(x^j)<(wp)_t}x_t^j.\)

Let \(S=\{t:p_t>0\}\). Some coalition with composition \(p\) blocks if and only if

\(\displaystyle b_t(p)>0\qquad\text{for every }t\in S.\)

Indeed, if \(cp\) blocks, then \(b_t(p)\geq cp_t>0\) for every \(t\in S\). Conversely, if all these available masses are positive, the finiteness of \(S\) allows us to choose

\(\displaystyle c=\frac12\min_{t\in S}\frac{b_t(p)}{p_t}>0.\)

Then \(cp_t\leq b_t(p)\) for every participating type; the remaining coordinates are zero. Hence \(cp\) blocks.

This is the point where divisibility enters the proof.

2. Scarf’s lemma and finite collections of compositions

We use the following matrix form of Scarf’s lemma, stated as Lemma 1 in [Biró, Csáji, and Schlotter, *Stable Hypergraph Matching in Unimodular Hypergraphs*](https://drops.dagstuhl.de/storage/00lipics/lipics-vol334-icalp2025/html/LIPIcs.ICALP.2025.31/LIPIcs.ICALP.2025.31.html).

Let \(A\in\mathbb{R}_{\geq0}^{n\times m}\) have no zero column, let \(b\in\mathbb{R}_{>0}^{n}\), and give each row \(i\) a strict total order on the columns \(j\) for which \(A_{ij}>0\). Then the polytope

\(\displaystyle P=\{\lambda\in\mathbb{R}_{\geq0}^{m}:A\lambda\leq b\}\)

has an extreme point \(\lambda\) with the following property: for every column \(j\), there is a row \(i\) such that

We call this last property domination of column \(j\) at row \(i\).

Application to a finite collection

Fix any finite set \(D\subseteq\Delta\). Introduce the following activities:

Here \(e_t\) is the unit vector at \(t\). Importantly, \(C_{e_t}\), when present, is distinct from \(I_t\): the former gives utility \(w_{tt}\), while the latter gives utility \(0\).

Let \(A\) have these contribution vectors as its columns, and set \(b=\mu\). In each row \(t\), rank incident activities by their numerical utilities, resolving equal utilities arbitrarily into a strict total order.

All hypotheses of Scarf’s lemma hold:

Let \(\lambda\) be the extreme point supplied by the lemma.

All type masses are allocated. The isolation column \(I_t\) is incident only to row \(t\). Its domination therefore requires

\(\displaystyle (A\lambda)_t=\mu_t.\)

This holds for every \(t\), so \(A\lambda=\mu\).

Every allocated activity is individually rational. Domination of \(I_t\) also says that every activity receiving positive type-\(t\) mass is ranked at least as highly as isolation. Because the order refines numerical utility, all such activities give type \(t\) utility at least \(0\).

No composition in \(D\) can block. For \(p\in D\), domination of \(C_p\) supplies a participating type \(t\) whose entire allocated mass receives utility at least \((wp)_t\). Consequently \(b_t(p)=0\), which excludes blocking by the criterion in Section 1.

Interpret each positive \(\lambda_{C_p}\) as the coalition vector \(\lambda_{C_p}p\), and each \(\lambda_{I_t}\) as isolated mass. We have obtained a partition that is individually rational and stable against all compositions in \(D\).

A uniform bound on the number of activities

The extreme point \(\lambda\) has at most \(\tau\) positive coordinates.

To prove this, suppose its positive support had more than \(\tau\) columns. Those columns would be linearly dependent, giving a nonzero vector \(h\), supported on positive coordinates of \(\lambda\), with \(Ah=0\). For sufficiently small \(\varepsilon>0\), both \(\lambda+\varepsilon h\) and \(\lambda-\varepsilon h\) would be nonnegative. They would remain feasible because their images under \(A\) equal \(A\lambda\). Their midpoint would be \(\lambda\), contradicting extremality.

Thus the finite-collection construction uses at most \(\tau\) positive activities, counting isolation activities as well as coalitions.

3. Passing to all compositions

For each positive integer \(n\), use the finite grid

\(\displaystyle D_n=\left\{p\in\Delta:p_t=\frac{k_t}{n},\ k_t\in\mathbb{Z}_{\geq0},\ \sum_tk_t=n\right\}.\)

Section 2 gives a partition \(\Pi_n\), stable against every composition in \(D_n\), using at most \(\tau\) positive activities.

Represent its activities in \(\tau\) slots, padding unused slots with zero intensity. For slot \(r\), write:

For an isolation slot of type \(t\), necessarily \(q_{r,n}=e_t\). Since all contribution vectors sum to \(1\) and all masses are allocated,

\(\displaystyle \sum_{r=1}^{\tau}\alpha_{r,n}=1,\qquad \sum_{r=1}^{\tau}\alpha_{r,n}q_{r,n}=\mu.\)

There are finitely many possible slot-label patterns. Pass to an infinite subsequence on which the pattern is fixed. Then, by compactness of \([0,1]^\tau\times\Delta^\tau\), pass to a further subsequence on which

\(\displaystyle \alpha_{r,n}\longrightarrow\alpha_r,\qquad q_{r,n}\longrightarrow q_r\)

for every slot \(r\). Indices \(n\) below refer to this subsequence and tend to infinity.

Taking limits gives

\(\displaystyle \sum_{r=1}^{\tau}\alpha_rq_r=\mu.\)

Each coalition slot with \(\alpha_r>0\) becomes the nonzero coalition \(x^r=\alpha_rq_r\). Each isolation slot contributes \(\alpha_r\) to its isolated type. Discard slots of zero intensity. This defines a finite mass partition \(\Pi\).

Individual rationality survives the limit

Suppose a coalition slot has \(\alpha_rq_{r,t}>0\). Then \(\alpha_{r,n}q_{r,n,t}>0\) for all sufficiently large \(n\). Individual rationality of \(\Pi_n\) gives

\(\displaystyle (wq_{r,n})_t\geq0.\)

By continuity,

\(\displaystyle u_t(x^r)=(wq_r)_t\geq0.\)

Hence \(\Pi\) is individually rational.

Strict blocking cannot appear in the limit

Suppose, for contradiction, that a coalition blocks \(\Pi\). Let \(p\in\Delta\) be its composition and \(S=\{t:p_t>0\}\).

Section 1 gives \(b_t(p)>0\) for every \(t\in S\). Because \(\Pi\) has finitely many activities, for each \(t\in S\) there is a slot \(r(t)\) carrying positive type-\(t\) mass whose utility is strictly below \((wp)_t\).

Denote that source utility by \(v_t\). Thus

\(\displaystyle \alpha_{r(t)}q_{r(t),t}>0,\qquad v_t<(wp)_t.\)

For a coalition source, \(v_t=(wq_{r(t)})_t\); for an isolation source, \(v_t=0\).

We next approximate \(p\) by grid compositions with exactly the same support. Enumerate \(S=\{t_1,\ldots,t_s\}\). Set

\(\displaystyle k_{t_i,n}=\lfloor np_{t_i}\rfloor\quad(i<s),\qquad k_{t_s,n}=n-\sum_{i<s}k_{t_i,n},\)

and set all coordinates outside \(S\) to zero. Let \(p^{(n)}_t=k_{t,n}/n\). Then \(p^{(n)}\in D_n\), \(p^{(n)}\to p\), and, for sufficiently large \(n\), every coordinate indexed by \(S\) is positive. This also covers \(s=1\), when \(p^{(n)}=p\).

The source slot \(r(t)\) carries positive type-\(t\) mass in \(\Pi_n\) for all sufficiently large \(n\), because its mass converges to a positive number. Its utility converges to \(v_t\): coalition utilities are continuous in composition, and isolation utility remains \(0\). Meanwhile,

\(\displaystyle (wp^{(n)})_t\longrightarrow(wp)_t.\)

The strict inequality \(v_t<(wp)_t\) therefore persists for sufficiently large \(n\). Since \(S\) is finite, for all sufficiently large \(n\), every participating type has positive mass in \(\Pi_n\) that strictly prefers \(p^{(n)}\).

By Section 1, a sufficiently small coalition with composition \(p^{(n)}\) blocks \(\Pi_n\). This contradicts its stability against all compositions in \(D_n\).

Therefore \(\Pi\) is core stable. It has at most \(\tau\) coalitions, since it arose from at most \(\tau\) activity slots.

4. Decision complexity

The proof establishes universal existence for the exact model in the question, including arbitrary signs, same-type diagonal affinities, isolation utility \(0\), and strictly improving deviations.

Accordingly, on valid inputs the existence algorithm simply returns YES. If input validation is included, positivity and normalization of the rational masses and symmetry of the rational matrix can be checked in polynomial time in \(\tau\) and \(L\). Thus the decision problem is in \(\mathrm{P}\).

The compactness proof does not establish a polynomial-time algorithm for constructing a stable partition; construction is a separate question. No construction bound is needed to settle the requested existence decision.

⟨structured verdict parsed — rendered above⟩

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

Verification report

Verdict: proved. The argument establishes universal existence of a core-stable mass partition with at most \(\tau\) nonzero coalition vectors. Consequently, the existence decision problem is in \(\mathrm{P}\). I found no major or minor mathematical gaps.

The cited version of Scarf’s lemma is accurate, its hypotheses are satisfied, and the compactness argument preserves stability under the exact strict-blocking definition in USER_TASK.

1. Normalization and the blocking criterion

For every nonzero nonnegative coalition vector \(y\), the representation \(y=cp\) is unique: \(c=\sum_t y_t>0\) and \(p=y/c\in\Delta\). Substituting into the utility definition gives \(u_t(cp)=(wp)_t\), so both utilities and the available strictly improving masses depend only on \(p\).

The equivalence between blocking by some coalition of composition \(p\) and positivity of \(b_t(p)\) for every participating type is correct.

This reasoning also applies to countable partitions: each defining sum is bounded by the corresponding total type mass. No assumption that all available mass must participate is introduced.

Finding: correct, with all relevant quantifiers and domain restrictions accounted for.

2. The external theorem

I checked [Lemma 1 in Biró, Csáji, and Schlotter](https://drops.dagstuhl.de/storage/00lipics/lipics-vol334-icalp2025/html/LIPIcs.ICALP.2025.31/LIPIcs.ICALP.2025.31.html). It supplies a dominating extreme point for a nonnegative matrix with no zero column and strict row orders on incident columns. Its domination condition is exactly the one used by the prover. The source permits nonnegative capacities; the prover’s restriction to positive capacities is valid.

The theorem applies to arbitrary nonnegative column entries, not merely binary hypergraph incidence matrices. Thus using composition vectors as columns is legitimate. Repeated contribution vectors with distinct activity labels are also permitted.

Finding: the theorem is stated sufficiently precisely and is correctly attributed. There is no unverified theorem application.

3. Application to finitely many compositions

Hypotheses and boundedness

Every activity column belongs to \(\Delta\), including each isolation vector \(e_t\). Therefore every column is nonnegative and nonzero. The capacity vector \(\mu\) has strictly positive entries.

The finite activity set permits a strict total order in each row obtained by refining numerical utility. Isolation ensures that every row has an incident column.

The boundedness calculation is correct: since every column sums to one, summing \(A\lambda\leq\mu\) over rows gives \(\sum_j\lambda_j\leq\sum_t\mu_t=1\). The zero vector establishes nonemptiness.

Complete allocation

The isolation column \(I_t\) is incident only to row \(t\). Consequently, its domination must occur in that row and requires \((A\lambda)_t=\mu_t\). Applying this to every type establishes \(A\lambda=\mu\).

This step correctly eliminates any unallocated residual mass.

Individual rationality

Domination of \(I_t\) requires every activity carrying positive type-\(t\) mass to rank at least as highly as isolation. Because the order refines numerical utility and isolation has utility zero, every such activity has numerical utility at least zero.

Arbitrary tie-breaking does not undermine this implication. Equal numerical utilities may be ordered differently, but an activity with negative utility cannot rank above isolation.

Stability against the finite set

For each \(p\in D\), domination of \(C_p\) supplies a participating type \(t\) whose entire allocated mass receives utility at least \((wp)_t\). Hence no mass of that type strictly prefers the proposed composition, and \(b_t(p)=0\).

This includes isolated mass: if positive isolated mass occurs in that row, its numerical utility must also be at least the proposed utility. Thus the isolation contribution to \(b_t(p)\) vanishes as required.

The blocking criterion then excludes every composition in \(D\).

Interpretation as a partition

A positive coalition intensity produces the nonzero vector \(\lambda_{C_p}p\), with the stipulated utility. Isolation intensities produce isolated masses. The equation \(A\lambda=\mu\) is exactly the mass-conservation requirement.

Keeping \(C_{e_t}\) distinct from \(I_t\) correctly preserves the distinction between same-type coalition utility \(w_{tt}\) and isolation utility zero.

Finding: all parts of the finite-composition construction are correct.

4. The uniform activity bound

If more than \(\tau\) coordinates of \(\lambda\) were positive, their columns in \(\mathbb{R}^{\tau}\) would be linearly dependent. The resulting nonzero vector \(h\), supported on those coordinates, satisfies \(Ah=0\).

Because the support is finite and all its coordinates of \(\lambda\) are positive, sufficiently small positive \(\varepsilon\) makes both perturbations nonnegative. Their images under \(A\) remain unchanged, so both are feasible. They are distinct, and their midpoint is \(\lambda\), contradicting extremality.

The bound counts isolation activities as well as coalitions, as the prover explicitly states.

Finding: correct; no nondegeneracy or integrality assumption is needed.

5. Compactness and the limiting partition

Each grid \(D_n\) is finite. The preceding construction therefore supplies the stated partition for every positive integer \(n\).

Padding to \(\tau\) slots is legitimate because unused slots have zero intensity. There are finitely many label patterns, so an infinite subsequence with fixed labels exists. All intensities lie in \([0,1]\), and all contribution vectors lie in the compact simplex. The stated simultaneous convergent subsequence follows.

The mass-conservation identities survive the limit because the number of slots is fixed and finite. An isolation slot retains its unit contribution vector under the fixed label pattern. A positive coalition intensity yields a nonzero coalition because its limiting composition remains in \(\Delta\). Discarding zero-intensity slots changes no mass.

Valid inputs necessarily have \(\tau\geq1\), since positive masses sum to one.

Finding: the limit defines a valid finite mass partition with the claimed coalition bound.

6. Individual rationality in the limit

If \(\alpha_rq_{r,t}>0\), convergence ensures positive type-\(t\) mass in that same slot for all sufficiently large subsequence indices. Individual rationality of the approximating partitions therefore applies.

For coalition slots, utility is the continuous linear function \((wq_r)_t\). Passing to the limit preserves its nonnegativity.

The argument only requires rationality for types with positive limiting mass, exactly as USER_TASK requires.

Finding: correct.

7. Preservation of strict nonblocking

This is the decisive limiting step, and it is sound.

If the limiting partition were blocked, the criterion from Section 1 would give positive available mass for every type in the proposed composition’s support. Since the limiting partition has finitely many activities, each participating type has at least one positive-mass source with a strictly lower utility. The source may be a coalition or isolation; both cases are explicitly handled.

The grid approximation has the required properties:

Thus \(p^{(n)}\to p\) with exactly the same support for sufficiently large \(n\).

For each selected source, positive limiting mass ensures positive approximating mass eventually. Its utility converges to the limiting source utility. The proposed utility also converges. Because the limiting preference inequality is strict, it persists eventually.

There are only finitely many participating types, so one sufficiently large threshold works for all of them. Section 1 then produces a blocking coalition for the corresponding approximating partition, contradicting its stability against \(D_n\).

The proof does not assume continuity of the indicator-based function \(b_t(p)\). Its argument uses persistent positive sources and strict utility inequalities, which is sufficient.

Finding: correct; no missing stability-closure lemma is needed.

8. Scope and decision complexity

The proof handles arbitrary signs, diagonal affinities, isolated utility zero, and strictly improving deviations. Symmetry is indeed unused.

Universal existence makes returning YES correct on every valid input. If validity checking is part of the decision problem, exact rational positivity, normalization, and matrix symmetry can be checked in polynomial time in the stated input parameters.

The proof supplies an existence result rather than a polynomial-time construction algorithm. The prover explicitly distinguishes these claims, and construction is not required to settle the requested existence decision.

Issues and repair feedback

No issues were identified. No additional clarification or repair is necessary to make the argument verifiable.

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