← back to the atlas

d4-conf-aaai-2021-0123 (d4-conf-aaai-2021-0123)

Answer: Polynomial-time solvable: every valid input is a YES-instance. The promised-input decision time is \(O(1)\), or \(O(L)\) when reading the entire input.

The anchor (named result in the paper)

Theorem 3 — class: other

PDF text-layer excerpt — equations and symbol order may be approximateIn every Euclidean deliberation space, every maximal run of compromise transitions is a successful deliberation.

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

The continuous mirror question, as graded

Given \(d\), a rational status quo \(r\), a finite type set \(T\subseteq\mathbb{Q}^d\), rational masses \(\mu_t>0\) summing to \(1\), and a valid finite initial coalition structure with rational per-type allocations, does every maximal run of two-coalition compromise transitions terminate at a coalition whose proposal maximizes approval mass and whose mass equals that proposal’s total approval mass? Proposals are in \(\mathbb{Q}^d\); each transition moves all approving mass from its two source coalitions into the new coalition, which must be larger than either source.

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

Given \(d\geq1\), let the proposal space be \(\mathbb Q^d\) and the status quo be \(r\in\mathbb Q^d\). Type \(t\) approves \(p\) exactly when \(\|t-p\|_2<\|t-r\|_2\); equality means disapproval.
A society is given by its support: \(T\subseteq\mathbb Q^d\), with \(\tau=|T|\) positive masses \(\mu_t\in\mathbb Q\) encoded in binary and summing to \(1\). Require \(T\setminus\{r\}\neq\varnothing\); \(\tau\) counts listed types, not possible types.
The input includes \(k\) positive-mass coalitions \((a_i,p_i)\), where \(a_{it}\in\mathbb Q_{\geq0}\), \(\sum_i a_{it}=\mu_t\), and \(p_i\in\mathbb Q^d\). If \(p_i\neq r\), every type with \(a_{it}>0\) approves \(p_i\); if \(p_i=r\), only type \(r\) may have positive allocation. Distinct coalitions may support the same proposal, and a type may be split among coalitions.
Write \(s(a)=\sum_t a_t\) and \(a^p_t=a_t\mathbf1\{t\text{ approves }p\}\). A transition chooses two distinct coalitions \((a,p_a),(b,p_b)\) and any \(p\in\mathbb Q^d\setminus\{r\}\), replacing them by \((a^p+b^p,p)\), \((a-a^p,p_a)\), and \((b-b^p,p_b)\), provided \(s(a^p+b^p)>\max\{s(a),s(b)\}\). Omit zero-mass remnants; leave all other coalitions unchanged. No additional splitting or transfers are permitted.
Let \(A(p)=\sum_{t\text{ approves }p}\mu_t\) and \(M=\max_{p\in\mathbb Q^d\setminus\{r\}}A(p)\). A structure is successful if it contains \((a,p)\) with \(A(p)=s(a)=M\). A maximal run is infinite or finite with no available transition; it succeeds exactly when it is finite and its final structure is successful.
Let \(L\) be the total binary input length and \(m=d\); state running times in \(m,\tau,k,L\).

Is deciding whether every maximal run from the supplied initial structure succeeds solvable in polynomial time, or is it NP-hard?

For finite agent lists in full Euclidean proposal spaces, every maximal two-coalition compromise run succeeds; this also holds with rational proposals. [Discrete guarantee](https://link.springer.com/article/10.1007/s00355-024-01561-y).
For finite agent lists, every such run has at most \(2^n\) transitions, where \(n\) is the number of agents. [Discrete length bound](https://arxiv.org/html/2202.12594). No result explicitly treating the mass-allocation decision problem above was located.

Modeling choices made when packaging the task

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

Resolution

The decision problem is polynomial-time solvable: every valid input is a YES-instance. Rational masses and the prescribed transition rule allow an exact transfer to the finite-agent theorem given in the question. The transfer is a proof device; the decision algorithm does not construct the expanded agent list.

1. The maximum approval is attained

For any proposal \(p\), its approval set is a subset of the finite support \(T\). Consequently, \(A(p)\) takes values in the finite set
\(\{\sum_{t\in S}\mu_t:S\subseteq T\}\).
The proposal domain is nonempty, so its approval values have an attained maximum \(M\).

Moreover, \(M>0\): choose \(t\in T\setminus\{r\}\). The rational proposal \(p=t\) is approved by type \(t\), since
\(\|t-t\|_2=0<\|t-r\|_2\).

2. Exact expansion into finitely many agents

Choose a positive integer \(D\) divisible by the denominators of every \(\mu_t\) and every \(a_{it}\). Then all \(D\mu_t\) and \(Da_{it}\) are nonnegative integers.

For each type \(t\), introduce \(D\mu_t\) distinct labeled agents, each located at \(t\). Labels distinguish agents even when their locations coincide. This is a finite agent list, with total length
\(N=\sum_t D\mu_t=D\).

Partition the agents of type \(t\) among the initial coalitions, assigning exactly \(Da_{it}\) to coalition \(i\). This is possible because
\(\sum_i Da_{it}=D\mu_t\).
Let \(C_i\) be the resulting labeled-agent coalition, supporting \(p_i\).

This is a valid finite-agent coalition structure:

The expansion accommodates every initially split type by placing different labeled agents of that type in different coalitions.

3. Transitions correspond exactly

At any corresponding state, suppose a mass coalition \((a,p_a)\) is represented by \((C_a,p_a)\), with exactly \(Da_t\) agents of type \(t\). Thus
\(|C_a|=Ds(a)\).

For every rational proposal \(p\), all agents located at \(t\) make the same approval decision. Therefore
\(|C_a^p|=Ds(a^p)\).

Consider two distinct coalitions represented by \(C_a,C_b\). Since their agent sets are disjoint,
\(|C_a^p\cup C_b^p|=Ds(a^p+b^p)\).
Multiplication by the positive number \(D\) gives the equivalence
\[ \text{ } \]
\(s(a^p+b^p)>\max\{s(a),s(b)\}\)
if and only if
\(|C_a^p\cup C_b^p|>\max\{|C_a|,|C_b|\}\).

The moving agents represent precisely the allocation \(a^p+b^p\). The two remnants represent precisely \(a-a^p\) and \(b-b^p\). Empty agent remnants correspond to zero-mass remnants and are omitted.

Hence every mass transition lifts to a finite-agent compromise transition, using the same rational proposal. Conversely, every finite-agent compromise transition projects to an allowed mass transition. No additional splitting or transfers are introduced.

Induction on the transitions therefore lifts any mass run to a corresponding finite-agent run. An infinite mass run lifts to an infinite run. A finite terminal mass run lifts to a terminal run: any available finite-agent transition would project to an available mass transition.

4. Applying the finite-agent guarantee

We use the theorem supplied in the question: for a finite agent list in a full Euclidean proposal space, every maximal two-coalition compromise run terminates successfully; the conclusion also holds for rational proposals. The transition requires all approvers in the selected coalitions to move and the resulting coalition to exceed both original sizes. See [Theorem 3, Definition 10, and the rational-space observation following Theorem 3](https://link.springer.com/article/10.1007/s00355-024-01561-y).

All hypotheses were checked above: finitely many labeled agents, Euclidean strict approval, the full rational proposal space, a valid initial partition, and exactly the specified compromise rule.

For any rational proposal \(p\), the expanded approval count is
\(|V^p|=DA(p)\).
Its maximum is consequently \(DM\).

Now take any maximal mass run. Its lift is maximal, so the finite-agent theorem says that it is finite and ends with a coalition \((C,p)\) satisfying
\(|C|=|V^p|=DM\).
For the corresponding mass coalition \((a,p)\), this gives
\(Ds(a)=DA(p)=DM\), and therefore
\(s(a)=A(p)=M\).

Thus the original maximal run succeeds. Since the run was arbitrary, every maximal run succeeds.

5. A direct termination bound using the listed allocations

The denominator expansion is unnecessary even for proving termination. A sharper bound follows from the transition rule itself.

For each initially positive allocation \(a_{it}\), create one labeled packet of mass \(a_{it}\) and type \(t\). Let
\(B=|\{(i,t):a_{it}>0\}|\), so \(1\le B\le k\tau\).

A packet is never split: whenever its current coalition participates in a transition, approval depends only on its type, so the entire packet moves or the entire packet remains. Every reachable coalition structure therefore partitions these \(B\) packets into nonempty blocks.

For each structure, sort its coalition masses in nonincreasing order and pad with zeros to obtain a vector of length \(B\). Every transition strictly increases this vector lexicographically. Indeed, if the two selected masses are \(x,y\) and the new mass is \(c\), then \(c>\max\{x,y\}\). Both remnants have mass less than \(c\). Thus all preexisting masses at least \(c\) remain unchanged, and one additional mass \(c\) appears. At the first changed coordinate, the new vector has \(c\) and the old vector has a smaller value.

There are at most \(\operatorname{Bell}(B)\) possible mass vectors, because a partition of the packets determines its vector. Consequently every run has at most
\(\operatorname{Bell}(B)-1\le B^B-1\le(k\tau)^{k\tau}-1\)
transitions. The inequality \(\operatorname{Bell}(B)\le B^B\) follows by encoding a partition through the function sending each packet label to the least label in its block.

This bound is independent of the denominators and of \(m\). It proves finiteness directly; the finite-agent theorem supplies the success of terminal states.

6. Decision algorithm and running time

On the promised valid inputs, the algorithm simply returns YES. Its decision time is \(O(1)\), or \(O(L)\) if it reads the complete encoding.

If malformed inputs must also be rejected, the stated validity conditions can be checked in polynomial time using exact rational arithmetic. A conservative bound is
\(O\!\left(m(k\tau+\tau^2)L^3\right)\)
bit operations, including pairwise checks that the listed types are distinct. Approval is checked by comparing squared distances, so no square roots or numerical approximation are needed.

Although \(D\) can be exponentially large in \(L\), neither decision algorithm constructs the expanded society.

⟨structured verdict parsed — rendered above⟩

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

Assessment

The polynomial-time conclusion is sound, with minor presentational gaps. The rational expansion preserves the prescribed mass transitions and success condition. The packet argument independently rules out infinite runs. No major mathematical error was found.

The output addresses the decision problem for the supplied initial structure, including split types, repeated proposals, strict approval, and binary-encoded rational masses.

Step-by-step verification

1. Attainment and positivity of the maximum

Correct.

The support is finite, so the set of approval values realized by rational proposals is a nonempty finite set. It therefore contains its maximum. This argument does not assume that every subset of types is realizable.

The proposal domain is nonempty because \(d\geq1\). Choosing \(t\in T\setminus\{r\}\) gives an admissible rational proposal \(p=t\), approved by a type of positive mass. Hence \(M>0\).

2. Expansion into labeled agents

Correct.

There are finitely many rational input allocations and masses, so a common positive denominator \(D\) exists. The quantities \(D\mu_t\) and \(Da_{it}\) are integers, and the allocation identities permit the asserted partition.

The total number of agents is exactly \(D\), because the masses sum to one. Positive-mass coalitions become nonempty agent coalitions.

The validity checks are correct:

Repeated agent locations are compatible with the finite-agent-list guarantee explicitly supplied in USER_TASK.

The expansion is used only for correctness. Its potentially exponential size therefore does not undermine the claimed decision complexity.

3. Transition correspondence

The numerical and allocation correspondence is correct.

At a corresponding state, the identities \(|C_a|=Ds(a)\) and \(|C_a^p|=Ds(a^p)\) follow from type-dependent approval. Disjointness of the selected coalitions gives
\[ |C_a^p\cup C_b^p|=Ds(a^p+b^p). \]
Multiplication by \(D>0\) preserves the strict improvement condition.

The new coalition and both remnants have exactly the claimed type counts. These operations preserve integral multiples of \(1/D\), so the same denominator remains valid throughout a run.

The converse also respects the prohibition on additional splitting: a compromise moves every approving agent in each selected coalition, rather than choosing an arbitrary subset.

Minor issue: empty-coalition convention. The cited paper permits empty coalitions and formally retains the remnants in Definition 10; the task and prover omit empty remnants. Thus “correspond exactly” requires an explicit convention identifying structures after empty coalitions are discarded. This is a routine representational clarification, but it should be stated when asserting that lifted terminal runs are terminal under the cited definition. See [Definitions 2 and 10 of the cited paper](https://link.springer.com/article/10.1007/s00355-024-01561-y).

Apart from this convention, the induction and maximality transfer are valid.

The empty display before the improvement equivalence is a cosmetic artifact; the equivalence itself remains fully stated.

4. Application of the finite-agent theorem

Correct in substance.

The cited Theorem 3 guarantees success of every maximal compromise run in full Euclidean proposal space. The following paragraph explicitly extends the argument to \(\mathbb Q^d\). Definition 10 uses all approvers from the two selected coalitions and requires the resulting coalition to exceed both original sizes. These are the required rules. [Theorem 3 and its rational-space observation](https://link.springer.com/article/10.1007/s00355-024-01561-y).

The supplied finite-agent-list guarantee covers the labeled-agent interpretation. The initial partition, strict Euclidean approval, rational proposal domain, and status-quo restriction have all been checked.

The identities \(|V^p|=DA(p)\) and maximum approval \(DM\) are correct for the same rational proposal domain used by the mass problem. Consequently, the successful terminal agent coalition projects to \(s(a)=A(p)=M\).

The argument applies to an arbitrary maximal mass run, establishing the required universal quantifier.

5. Packet termination bound

The bound is correct.

Each initially positive allocation defines a packet of fixed type and mass. Since approval depends only on type, a transition moves or retains an entire packet. Every reachable structure therefore partitions the same \(B\) packets.

The lexicographic argument is valid, including ties among coalition masses. The two removed masses and both remnants are strictly below the new mass \(c\). Existing masses at least \(c\) remain unchanged, while one additional occurrence of \(c\) appears. Thus the padded sorted vector strictly increases.

A packet partition determines its mass vector; injectivity is unnecessary for the asserted upper bound. There are at most \(\operatorname{Bell}(B)\) vectors, so there are at most \(\operatorname{Bell}(B)-1\) transitions. The least-label encoding correctly establishes \(\operatorname{Bell}(B)\leq B^B\). The remaining inequalities follow from \(1\leq B\leq k\tau\).

The edge case \(B=1\) gives zero transitions, as required.

Minor issue: “sharper” is not uniformly justified. Relative to the supplied discrete bound \(2^D\), the packet bound can be larger. For example, when \(B=D=5\), it gives \(\operatorname{Bell}(5)-1=51\), whereas \(2^5=32\). This affects only the comparative wording; the packet bound and termination conclusion remain valid.

6. Algorithm and running time

Correct.

Once every promised valid input is established to be a YES-instance, returning YES requires constant decision time. Reading the complete encoding takes \(O(L)\).

The optional validity checks involve exact rational comparisons, sums, coordinate equality, and squared-distance comparisons. These are polynomial-time operations. The stated bound \(O\!\left(m(k\tau+\tau^2)L^3\right)\) is conservative and consistent with these checks.

Neither computing \(M\), constructing the expanded society, nor simulating a run is necessary. The exponential termination bound is therefore compatible with a polynomial-time decision algorithm.

Minimal feedback

No new mathematical lemma or alternative argument is needed.

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