Answer: \(\mathrm{P}\)
Proposition 14 — class: algorithmic
Given a finite supported type set \(T\), rational masses \(\mu_t>0\) summing to \(1\), and each type's friend, neutral, and enemy rankings over types, can the atomless population be measurably partitioned into coalitions so that almost every type-\(t\) agent's coalition contains all mass of every friend type and zero mass of every enemy type?
A society is given by its support \(T\): the list of its \(\tau\geq 1\) types with positive binary rational masses \(\mu_t\), summing to \(1\). Here \(\tau\) is the support size, not the number of possible preference types; set \(m=|T|=\tau\), and let \(L\) be the total input bit length.
Each type \(t\) partitions \(T\) into friend, neutral, and enemy sets \(F_t,N_t,E_t\), with weak rankings on \(F_t\) and \(E_t\); neutral types are indifferent. Sets may be empty, and relationships need not be symmetric. Classification of \(t\) itself concerns other agents of type \(t\).
Realize the society as disjoint intervals \(X_t\) of lengths \(\mu_t\), with Lebesgue measure \(\lambda\), and put \(X=\bigsqcup_{t\in T}X_t\). A coalition structure \(\Gamma\) is a partition of \(X\) into nonempty measurable sets, with no restriction on their number or masses; types may split across coalitions. Write \(\Gamma(x)\) for the cell containing \(x\).
Call \(\Gamma\) perfect if there is a measurable set \(G\subseteq X\) with \(\lambda(X\setminus G)=0\) such that, for every \(t\) and \(x\in G\cap X_t\), \(\lambda(\Gamma(x)\cap X_s)=\mu_s\) for every \(s\in F_t\), and \(\lambda(\Gamma(x)\cap X_s)=0\) for every \(s\in E_t\). Neutral masses are unrestricted.
Is deciding whether such a perfect coalition structure exists in \(\mathrm{P}\), with running time polynomial in \(m,\tau,L\), or is it \(\mathrm{NP}\)-hard?
For finite agents, verification and existence of perfect partitions are in \(\mathrm{P}\); possible and necessary perfection coincide with containing every friend and no enemy. This is established in the [2015 result](https://aamas.csc.liv.ac.uk/Proceedings/aamas2015/aamas/p1229.pdf) and confirmed in the [2020 full version](https://www.lamsade.dauphine.fr/~lang/papers/KerkmannLRRSS20.pdf).
No result settling this exact atomless existence problem was located in the literature search.
The decision problem is in \(\mathrm{P}\). A friendship requirement forces both endpoint types into a single coalition up to null sets. These constraints propagate along undirected friendship paths. Types with no incident friendship requirement can instead be partitioned into singletons.
The finite-agent friendship-component algorithm appears in Proposition 26 and Corollary 28 of the [2020 full version](https://www.lamsade.dauphine.fr/~lang/papers/KerkmannLRRSS20.pdf). The proof below establishes the exact atomless criterion, including self-classifications and unrestricted measurable partitions.
Construct an undirected graph \(H\) on \(T\). For distinct types \(t,s\), put an edge between them if \(s\in F_t\) or \(t\in F_s\). Include a loop at \(t\) if \(t\in F_t\).
Call a connected component active if it contains at least one edge, counting loops. Every inactive component is therefore a single type that neither names any friend nor is named as a friend.
Theorem. A perfect coalition structure exists if and only if every active component \(C\) satisfies
\[ E_t\cap C=\varnothing \quad\text{for every }t\in C. \]
Here and below, the displayed formulas are understood as mathematical expressions; equivalently, the criterion is \(E_t\cap C=\varnothing\) for every type \(t\) in every active component \(C\).
We prove both directions directly.
Lemma. Suppose \(\Gamma\) is perfect, witnessed by a measurable conull set \(G\). If \(s\in F_t\), then some cell \(A\in\Gamma\) satisfies both \(\lambda(A\cap X_t)=\mu_t\) and \(\lambda(A\cap X_s)=\mu_s\).
Proof. Since \(G\) is conull and \(\mu_t>0\), we have \(\lambda(G\cap X_t)=\mu_t>0\). Choose \(x\in G\cap X_t\), and let \(A=\Gamma(x)\). Perfection gives \(\lambda(A\cap X_s)=\mu_s\).
For any \(y\in G\cap X_t\), perfection likewise gives \(\lambda(\Gamma(y)\cap X_s)=\mu_s\). If \(\Gamma(y)\ne A\), these are disjoint cells of a partition. Their intersections with \(X_s\) would consequently be disjoint measurable sets, each of measure \(\mu_s\). Hence \(2\mu_s\leq\lambda(X_s)=\mu_s\), contradicting \(\mu_s>0\).
Thus every point of \(G\cap X_t\) belongs to \(A\). It follows that \(\lambda(A\cap X_t)\geq\lambda(G\cap X_t)=\mu_t\). The reverse inequality follows from \(A\cap X_t\subseteq X_t\), proving equality.
This argument also applies when \(s=t\). \(\square\)
We also use the following immediate consequence of disjointness: two cells containing the full mass of the same positive-mass type must be the same cell. Indeed, distinct such cells would again imply \(2\mu_t\leq\mu_t\).
Assume that \(\Gamma\) is perfect, and fix an active component \(C\).
For each friendship edge in \(C\), the lemma provides a cell containing the full masses of its endpoint types. If two edges share a vertex, their associated cells contain the full mass of that vertex and therefore coincide.
Connectivity propagates this equality along paths. Since every vertex of an active component is incident to an edge, there is one cell \(A_C\) such that \(\lambda(A_C\cap X_t)=\mu_t\) for every \(t\in C\). For a component consisting of one vertex with a loop, this conclusion follows directly from the lemma.
Suppose that \(s\in E_t\cap C\) for some \(t\in C\). Because \(G\) is conull, \(\lambda(A_C\cap G\cap X_t)=\mu_t>0\). Choose a point \(x\) in this intersection. Its cell is \(A_C\), so perfection requires \(\lambda(A_C\cap X_s)=0\). But \(s\in C\) implies \(\lambda(A_C\cap X_s)=\mu_s>0\), a contradiction.
Thus \(E_t\cap C=\varnothing\) for every \(t\in C\). This includes the prohibition of self-enmity within an active component.
Assume the criterion holds.
For each active component \(C\), create the coalition \(B_C=\bigcup_{t\in C}X_t\). For every point \(x\) whose type belongs to an inactive component, create the singleton coalition \(\{x\}\).
These sets form a partition of \(X\): the component coalitions are disjoint, and the remaining points are partitioned into singletons. Every cell is nonempty and measurable. Each \(B_C\) is a finite union of measurable intervals, and each singleton is measurable.
We verify perfection for every point, so we may take \(G=X\).
If \(x\in X_t\) and \(t\) belongs to an active component \(C\), then \(\Gamma(x)=B_C\).
If \(t\) belongs to an inactive component, then \(F_t=\varnothing\) and \(\Gamma(x)=\{x\}\). All friendship requirements are vacuous. For every \(s\in E_t\), atomlessness gives \(\lambda(\{x\}\cap X_s)=0\).
Therefore the constructed partition is perfect. This proves sufficiency and completes the theorem. \(\square\)
The theorem gives the following decision procedure.
There are at most \(m^2\) friend relations and at most \(m^2\) enemy relations. Graph construction, component computation, and the final scan require \(O(m^2)\) elementary graph operations. Reading the encoding takes time polynomial in \(L\); vertex indices have polynomially bounded bit length. Consequently, the total running time is polynomial in \(m,\tau,L\), with \(m=\tau\).
The algorithm uses neither the numerical values of the masses nor the weak rankings. Positivity of each mass is essential to the rigidity lemma; the rankings impose no additional condition in the stated definition of perfection.
The possibly uncountable partition in the sufficiency proof is an explicit mathematical witness. The decision algorithm only needs the finite component data.
If all friend sets are empty, the singleton partition is perfect, regardless of enemy classifications.
In particular, one type with \(F_t=\varnothing\) and \(E_t=\{t\}\) is feasible. Conversely, if \(a\) names \(b\) as a friend and \(b\in E_b\), the component containing them is active and violates the criterion, so no perfect partition exists.
Thus singleton coalitions handle unrestricted friendship-free types, while the positive masses make every friendship component subject to a finite, exact compatibility test.
⟨structured verdict parsed — rendered above⟩
Verdict: proved. The prover establishes an exact criterion for the stated atomless existence problem and a polynomial-time decision algorithm. No major or minor mathematical issues were found.
The graph correctly records directed friendship requirements as undirected edges, including self-friendship as a loop. This does not assume symmetric relationships.
The distinction between active and inactive components is correct. An inactive component consists of one type with no outgoing or incoming friendship requirement, including no self-friendship.
The proposed criterion checks directed enemy relations within active components. It correctly permits self-enmity for inactive types, whose agents can occupy singleton cells of measure zero.
Every step of the lemma is justified:
The argument also works when \(s=t\). It uses only two cells at a time, so an uncountable partition causes no difficulty. No countable-additivity argument over the entire partition is assumed.
The subsequent assertion that two cells containing the full mass of the same positive-mass type must coincide follows from the same disjointness calculation.
The propagation argument is valid. Each friendship edge supplies a cell containing its endpoint masses; cells associated with edges sharing a vertex must coincide. Connectivity therefore gives one cell containing every type’s full mass in an active component. The singleton component with a loop is explicitly covered.
If \(s\in E_t\cap C\), the intersection \(A_C\cap G\cap X_t\) has measure \(\mu_t>0\), because removing the null complement of \(G\) does not change its measure. Choosing a point there applies perfection to the cell \(A_C\), requiring its \(X_s\)-mass to be zero. This contradicts its already established mass \(\mu_s>0\).
Thus the criterion is necessary, including for self-enmity in active components.
The construction satisfies precisely the partition requirements in USER_TASK:
For an active type, every friend belongs to its component, and the criterion excludes every enemy from that component. Both required mass conditions follow.
For an inactive type, the friend set is empty. Every singleton intersection with a type interval has Lebesgue measure zero, so all enemy requirements hold, including self-enmity.
The verification holds at every point, making \(G=X\) a valid witness. The uncountable family of singleton cells is expressly permitted by the task; no additional measurability condition on the family or the cell assignment is required.
The algorithm implements the proved criterion exactly. Loop information suffices to distinguish an active singleton component from an inactive one, and the enemy scan includes self-enemy relations.
There are at most \(m^2\) directed relations of either kind. Graph construction, component computation, and scanning enemy relations require \(O(m^2)\) elementary graph operations. Accounting for reading the input and manipulating encoded indices preserves polynomial bit complexity in \(m,\tau,L\), with \(m=\tau\).
Ignoring mass values and rankings is justified: the proof uses only positivity of the masses, and the stated perfection conditions do not involve rankings. The algorithm decides existence without needing to enumerate the potentially uncountable witness partition.
The cited finite-agent attribution is accurate: Proposition 26 presents the friendship-component construction, and Corollary 28 states polynomial-time verification and existence results for perfection. [2020 full version](https://www.lamsade.dauphine.fr/~lang/papers/KerkmannLRRSS20.pdf)
These results serve as background; the atomless conclusion is proved independently, so no transfer of finite-agent hypotheses is needed.
All listed boundary cases are correct. In particular, empty friend sets allow the singleton partition, while self-enmity in a component activated by friendship prevents perfection.
Required clarification or repair: none.
⟨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.