← back to the atlas

d4-journals-geb-2015-0052 (d4-journals-geb-2015-0052)

Answer: Polynomial-time decidable for \(m=\tau=3\); a stable partition can also be constructed in polynomial time as an exact algebraic mass table whenever one exists.

The anchor (named result in the paper)

Proposition 5 — class: other

The continuous mirror question, as graded

Given three productivity types with rational masses \(\mu_h,\mu_m,\mu_l\) summing to \(1\), their productivity levels \(\lambda_h>\lambda_m>\lambda_l\), and a minimum productive organization mass \(\alpha\), decide whether a measurable partition into organizations exists in which every productive organization has mass at least \(\alpha\), its mass median selects meritocracy or egalitarianism under the paper’s voting rule, and no positive-mass group can form a blocking organization; construct such a partition when one exists.

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

A society is an atomless probability space partitioned into three measurable productivity types, with positive masses \(\mu_h+\mu_m+\mu_l=1\) and productivities \(\lambda_h>\lambda_m>\lambda_l\geq0\). All input numbers, including the threshold \(0<\alpha\leq1\), are binary rationals.
The society is given by its support: the list of types with positive mass and their masses. Here the number of productivity levels is \(m=3\), and the support size is \(\tau=3\); support size means listed positive-mass types, not possible types. Let \(L\) be the total input bit length; state running times in \(m,\tau,L\), and any dependence on \(\alpha\).
An organizational structure is a finite or countable partition into positive-mass measurable organizations, covering society up to a null set; types may be split arbitrarily among organizations.
For any positive-mass coalition \(G\), write \(s_G=\mu(G)\) and \(a_G=s_G^{-1}\int_G\lambda\,d\mu\). It is productive exactly when \(s_G\geq\alpha\), producing \(s_Ga_G\); otherwise every member receives zero.
Define its upper mass median by \(d_G=\max\{\lambda_j:\mu(G\cap\{\lambda\geq\lambda_j\})\geq s_G/2\}\). A productive coalition chooses meritocracy when \(d_G\geq a_G\), paying each type \(j\) the amount \(\lambda_j\); otherwise it chooses egalitarianism, paying everyone \(a_G\).
Individuals compare organizations lexicographically by their own payment and then the organization's mean productivity \(a_G\), including for unproductive organizations.
A blocking coalition is any positive-mass measurable group whose members almost everywhere strictly prefer its resulting organization to their assigned organization. Such a group may draw arbitrary portions from several organizations and is subject to the same production and voting rules, even when unproductive. A partition is core stable if no blocking coalition exists.

Is deciding whether a core-stable partition exists solvable in polynomial time, or is it NP-hard? If it is in polynomial time, can a stable partition also be constructed in polynomial time whenever one exists?

For finite three-type societies, a necessary-and-sufficient existence characterization and constructions of stable partitions are known, without a stated complexity classification. The authors also report continuum robustness, but give no computational classification for the problem above; no such classification was located in the search. [Barberà, Beviá and Ponsatí](https://bw.bse.eu/wp-content/uploads/2015/09/737-file.pdf).

Modeling choices made when packaging the task

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

1. Answer and representation of a constructed partition

For \(m=\tau=3\), existence is decidable in polynomial time, and a stable partition can be constructed in polynomial time whenever one exists. The construction outputs a finite table of exact real algebraic type masses.

A mass table is the appropriate representation because the input specifies only type masses. If its entries are \(x_{ij}\), row \(i\) describes an organization containing mass \(x_{ij}\) of type \(j\). On any atomless society with the given support, this table can be realized by measurable subsets.

The central result is that, whenever a stable partition exists, one exists with at most

\[ K=(m+3)(2^\tau-1) \]

organizations. Thus \(K=42\) here. Crucially, this bound is independent of \(\alpha\).

The proof below establishes this compression result and then gives an exact algorithm.

2. Preliminary facts

Let \(J\) be the set of listed types, so \(|J|=\tau\). For an organization \(G\), define its type support by

\[ S(G)=\{j\in J:\mu(G\cap T_j)>0\}, \]

where \(T_j\) is the measurable set of type \(j\).

Write an individual’s outcome as \((p,a)\), consisting of payment and organizational mean, ordered lexicographically.

We use the standard divisibility theorem for atomless finite measures: if \(A\) is measurable and \(0\leq t\leq\mu(A)\), there is a measurable subset of \(A\) with measure \(t\). Restrictions of the society’s measure to measurable type and organization intersections remain finite and atomless. Consequently, all portions selected below exist.

Voting identity. If \(G\) has mean \(a\), then

\[ d_G\geq a \quad\Longleftrightarrow\quad \mu(G\cap\{\lambda\geq a\})\geq s_G/2. \]

Indeed, if \(d_G\geq a\), the upper tail at \(a\) contains the upper tail at \(d_G\). Conversely, if the upper tail at \(a\) has at least half the mass, let \(\lambda_j\) be the smallest listed productivity at least \(a\). Its upper tail is precisely the upper tail at \(a\), so \(d_G\geq\lambda_j\geq a\).

Thus productive meritocracy is characterized by the weak inequality in this identity, and productive egalitarianism by its strict complement.

Monotonicity of stability. Suppose a stable partition is replaced by a partition under which almost every individual’s outcome weakly improves. The replacement remains stable.

To prove this, a coalition blocking the replacement would give its members outcomes strictly above their replacement outcomes, hence strictly above their original outcomes by transitivity of the lexicographic order. It would therefore block the original partition. Coalition outcomes depend only on their membership, so they are identical in this comparison.

3. The exchange lemma

Lemma. Suppose two organizations \(G,H\) have the same type support and belong to the same category: unproductive, productive egalitarian, or productive meritocratic. Suppose their means satisfy \(A=a_G>B=a_H\).

Then the partition is blocked in either of the following circumstances:

Proof. The common support must contain at least two productivity levels: otherwise both means would be identical.

Let \(\lambda_+\) and \(\lambda_-\) be its highest and lowest productivities, and put \(\Delta=\lambda_+-\lambda_->0\). Remove mass \(\varepsilon\) of type \(\lambda_-\) from \(G\), and replace it with mass \(\varepsilon\) of type \(\lambda_+\) from \(H\). Atomlessness permits this for every sufficiently small positive \(\varepsilon\).

The resulting coalition \(G_\varepsilon\) has unchanged mass and mean

\[ A_\varepsilon=A+\frac{\varepsilon\Delta}{s_G}>A>B. \]

We check each category.

Unproductive organizations. Since mass is unchanged, \(G_\varepsilon\) remains unproductive. Every participant still receives zero and obtains a strictly higher mean than in their assigned organization. Hence every participant strictly improves.

Productive egalitarian organizations. By the voting identity,

\[ \delta=\frac{s_G}{2}-\mu(G\cap\{\lambda\geq A\})>0. \]

Choose \(\varepsilon<\delta\), in addition to the availability constraints. Replacing mass \(\varepsilon\) can increase any upper-tail mass by at most \(\varepsilon\), and \(A_\varepsilon>A\). Therefore

\[ \mu(G_\varepsilon\cap\{\lambda\geq A_\varepsilon\}) \leq \mu(G\cap\{\lambda\geq A\})+\varepsilon < s_G/2. \]

Thus \(G_\varepsilon\) remains egalitarian. Its payment \(A_\varepsilon\) exceeds both original payments \(A\) and \(B\), so every participant strictly improves.

Productive meritocratic organizations with \(A<d_G\). Choose \(\varepsilon\) small enough that \(A_\varepsilon<d_G\). Replacing a lowest-productivity member by a highest-productivity member cannot decrease the upper-tail mass at \(d_G\). Consequently,

\[ \mu(G_\varepsilon\cap\{\lambda\geq d_G\})\geq s_G/2, \]

and the new median is at least \(d_G>A_\varepsilon\). Thus \(G_\varepsilon\) remains meritocratic. Every participant keeps their productivity payment and obtains a strictly higher mean than before.

In all three cases, \(G_\varepsilon\) blocks. This proves the lemma.

4. Compression to at most \(42\) organizations

Theorem. If a core-stable finite or countable partition exists, there is a core-stable finite partition with at most \(K=(m+3)(2^\tau-1)\) organizations.

Proof. Fix a stable partition and a nonempty type support \(S\).

The exchange lemma implies that all unproductive organizations with support \(S\) have the same mean. It likewise implies that all productive egalitarian organizations with support \(S\) have the same mean.

Consider productive meritocratic organizations with support \(S\). There are at most \(m\) distinct means equal to a productivity level. There is at most one additional distinct mean. Indeed, if two additional means satisfy \(A>B\), the organization with mean \(A\) is meritocratic and \(A\) is not a productivity level. Its median is a productivity level, so

\[ A\leq d_G \quad\text{and}\quad A\neq d_G, \]

giving \(A<d_G\). The exchange lemma then contradicts stability.

Therefore, for each support, there are at most \(m+3\) classes specified by category and mean. There are at most \(2^\tau-1\) nonempty supports. Hence there are at most \(K\) such classes.

Merge all organizations within each class. Countable unions are measurable. If the common mean is \(A\), their union also has mean \(A\), by countable additivity of mass and productivity integrals.

For a productive meritocratic class, each organization has at least half its mass at productivities at least \(A\). Summing these inequalities proves the same property for the union. The union remains productive and meritocratic, preserving every member’s outcome.

For a productive egalitarian class, each organization has strictly less than half its mass at productivities at least \(A\). The sum remains strictly less than half: the sum of the positive deficits is positive. The union remains productive and egalitarian, again preserving outcomes.

For an unproductive class, the union retains mean \(A\). If its total mass is below \(\alpha\), outcomes are unchanged. If its mass reaches \(\alpha\), it becomes productive. Every new payment is nonnegative, because all productivities are nonnegative. Thus every member weakly improves from their original outcome \((0,A)\).

The merged partition weakly improves everyone’s outcome. By monotonicity of stability, it is stable. It has at most \(K\) organizations.

For \(m=\tau=3\), this gives \(K=42\).

5. Exact algebraic encoding of stability

Fix \(n\), with \(1\leq n\leq K\). We describe a formula whose solutions are precisely stable partitions with \(n\) organizations.

For organization \(i\), introduce masses \(x_{ij}\), mean \(a_i\), and type payments \(p_{ij}\). Set

\[ s_i=\sum_{j\in J}x_{ij}. \]

Impose

\[ x_{ij}\geq0,\qquad \sum_{i=1}^{n}x_{ij}=\mu_j,\qquad s_i>0,\qquad s_i a_i=\sum_{j\in J}\lambda_jx_{ij}. \]

Atomless divisibility shows that every mass table satisfying these constraints is realizable as a measurable partition.

For any nonnegative type-mass vector \(z\) with positive total mass and mean \(c\), define the polynomial predicate

\[ \mathsf M(z,c)= \bigvee_{j\in J} \left( c\leq\lambda_j \ \wedge\ 2\sum_{r:\lambda_r\geq\lambda_j}z_r \geq \sum_r z_r \right). \]

By the definition of the upper median, this says exactly that the median is at least \(c\).

For each organization impose the following disjunction:

\[ \begin{aligned} & \left(s_i<\alpha\ \wedge\ \bigwedge_j p_{ij}=0\right) \\ {}\vee{}& \left(s_i\geq\alpha\ \wedge\ \mathsf M(x_i,a_i) \ \wedge\ \bigwedge_j p_{ij}=\lambda_j\right) \\ {}\vee{}& \left(s_i\geq\alpha\ \wedge\ \neg\mathsf M(x_i,a_i) \ \wedge\ \bigwedge_j p_{ij}=a_i\right). \end{aligned} \]

Call the resulting partition predicate \(\mathsf{Part}_n(x,a,p)\).

To encode a potential blocker, introduce variables \(y_{ij}\), describing how much type-\(j\) mass it draws from organization \(i\), together with its mean \(b\) and payments \(q_j\). Impose

\[ 0\leq y_{ij}\leq x_{ij},\qquad t=\sum_{i,j}y_{ij}>0,\qquad tb=\sum_{i,j}\lambda_jy_{ij}. \]

Apply the same production and voting disjunction to the blocker’s type masses \(z_j=\sum_i y_{ij}\), total mass \(t\), mean \(b\), and payments \(q_j\).

Finally, impose strict preference on every source cell used with positive mass:

\[ \bigwedge_{i,j} \left[ y_{ij}=0 \ \vee\ q_j>p_{ij} \ \vee\ \left(q_j=p_{ij}\ \wedge\ b>a_i\right) \right]. \]

Let \(\mathsf{Block}_n(x,a,p;y,b,q)\) denote these constraints.

This encoding is exact. Every measurable blocker supplies such variables. Conversely, every satisfying assignment supplies a measurable blocker: independently select the prescribed mass from each disjoint organization–type cell using atomless divisibility. Within each cell, assigned outcomes are constant, so the preference constraints are precisely strict preference almost everywhere.

Consequently, a stable partition with \(n\) organizations exists exactly when the following real-algebraic sentence is true:

\[ \exists x,a,p\ \left[ \mathsf{Part}_n(x,a,p) \ \wedge\ \neg\exists y,b,q\ \mathsf{Block}_n(x,a,p;y,b,q) \right]. \]

By the compression theorem, the original question is equivalent to the truth of this sentence for at least one \(n\leq K\).

6. Running time and construction

We use the standard algorithmic result that cylindrical algebraic decomposition decides polynomial formulas over the reals and produces exact algebraic sample points. With fixed numbers of variables and polynomials and fixed degrees, its bit complexity is polynomial in coefficient bit length. Quantifier elimination complexity and coefficient-size bounds are given in [Basu’s survey, Theorems 2.4 and 2.18](https://www.math.purdue.edu/~sbasu/raag_survey2011_final.pdf); algebraic sampling is treated in [Basu–Pollack–Roy](https://link.springer.com/book/10.1007/978-3-662-05355-3).

Here the hypotheses are satisfied:

A deliberately coarse bound for decision and construction is

\[ T(m,\tau,L) \leq \left[(m+\tau+1)K(L+1)\right]^{\,2^{O(K(\tau+1))}}, \qquad K=(m+3)(2^\tau-1). \]

The factor for trying all \(n\leq K\) is absorbed in this bound.

For \(m=\tau=3\), all parameters other than \(L\) are constants. Therefore the running time is polynomial in \(L\). The threshold \(\alpha\) appears only as a rational coefficient; there is no dependence on its numerical reciprocal \(1/\alpha\).

For construction, order the decomposition variables so that partition variables precede blocker variables. Evaluating the quantified blocker condition identifies cells consisting of stable partitions. If such a cell exists, its algebraic sample point yields the required mass table. For fixed \(m=\tau=3\), that table and its exact algebraic encoding have polynomial bit length.

For a concrete realization, represent each type by a separate interval of length \(\mu_j\) and split it into consecutive intervals of lengths \(x_{1j},\ldots,x_{nj}\). Organization \(i\) is the union of its pieces across types. On an arbitrary atomless society, the same mass table is realized by the divisibility theorem.

Thus both requested tasks are polynomial-time solvable under the given support representation.

⟨structured verdict parsed — rendered above⟩

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

Verification report

Assessment: proved with a minor gap in the specification of the constructed output. The compression argument and the encoding of stability are correct. They establish polynomial-time decision and construction for the stated support representation with \(m=\tau=3\). No central false statement or mathematical gap was found.

1. Scope and representation

The output addresses the continuous problem as stated, including countable partitions, arbitrary splitting of types, unproductive blocking coalitions, and lexicographic preferences.

A type-mass table is an appropriate construction output: the input contains no computational description of the underlying measurable space. The prover correctly distinguishes computing this table from realizing it on an arbitrary atomless society.

The stated divisibility theorem has the required hypotheses. Each measurable organization–type intersection inherits a finite atomless measure. Thus the selections used in the exchange lemma and blocker encoding are legitimate.

2. Preliminary facts

Voting identity: correct. The mean of a positive-mass coalition lies between its lowest and highest represented productivities. Consequently, the listed productivity used in the converse exists. Its upper tail equals the upper tail at the mean, as asserted.

The identity respects the specified voting tie: equality of the upper-tail mass with half the coalition mass yields meritocracy.

Monotonicity of stability: correct. Outside the null set where improvement may fail, strict preference over a weakly improved assignment implies strict preference over the original assignment. A positive-mass blocker is therefore also a blocker of the original partition. Its resulting outcome is unchanged because its membership is unchanged.

3. Exchange lemma

The common support contains at least two distinct productivities whenever the means differ. Positive support masses make the required removals and additions available for sufficiently small positive \(\varepsilon\).

The computation
\(A_\varepsilon=A+\varepsilon\Delta/s_G>A>B\)
is correct.

The removed members need not improve because they are not members of the proposed blocking coalition. The proof uses the blocking definition correctly.

4. Compression theorem

The class count is correct.

For each support:

For the last assertion, two different non-productivity means would let the larger mean satisfy the strict median condition in the exchange lemma. That contradiction is valid.

Thus the bound is \(K=(m+3)(2^\tau-1)\), giving \(K=42\) when \(m=\tau=3\).

Merging is valid, including countable classes.

Countable additivity preserves the common mean. Summing the meritocratic inequalities preserves their weak inequality. Summing the egalitarian deficits preserves strict positivity: a nonempty countable class contains at least one strictly positive deficit.

A merged productive class remains productive. A merged unproductive class either remains unproductive or becomes productive with nonnegative payments and the same mean. The latter weakly improves every member, including members whose productivity is zero.

Monotonicity therefore applies. No dependence on \(1/\alpha\) enters this argument.

5. Algebraic encoding

Partition constraints: correct. They enforce nonnegative type masses, conservation of every type, positive organization masses, and the correct means.

Median predicate: correct. Its disjunction asserts that some listed productivity at least the mean has an upper tail containing at least half the mass. This is exactly the required median comparison, including equality cases.

Production and payment disjunction: correct. It assigns unproductive status precisely below \(\alpha\), productive status at equality, and the correct payments under both voting outcomes.

Blocker constraints: correct.

The bounds on \(y_{ij}\) encode arbitrary portions from all organization–type cells. The positive total mass excludes empty coalitions, and the mean equation is valid without division.

For a positive source cell, the preference disjunction exactly expresses strict lexicographic improvement. Cells of zero selected mass impose no preference requirement.

Measurable blockers produce satisfying assignments, and satisfying assignments produce measurable blockers by atomless divisibility. Null exceptions in an almost-everywhere blocker do not change these masses or outcomes.

Accordingly, the quantified sentence expresses stability exactly. Together with compression, trying all \(n\leq K\) resolves the original existence question.

6. Complexity and construction

The variable and predicate counts have the stated orders, and the polynomial degrees are at most two. Clearing rational denominators can be done with positive multipliers and coefficient bit lengths \(O(L)\).

The cited real-algebraic algorithmic facts support polynomial bit complexity when dimension, degree, and predicate count are fixed. The survey states CAD bounds and quantifier-elimination coefficient bounds; the latter are also explicit in its [updated version, Theorem 2.27](https://arxiv.org/pdf/1409.1534). [The cited survey](https://www.math.purdue.edu/~sbasu/raag_survey2011_final.pdf) supports the CAD complexity assertion.

The displayed coarse running-time bound is consistent with these parameter counts. For \(m=\tau=3\), its exponent is constant. Dependence on \(\alpha\) is through its binary encoding, already included in \(L\).

The proposed variable ordering and evaluation of the quantified blocker condition correctly identify cells of stable assignments. Exact algebraic sampling supplies a mass table, and the interval realization describes a partition on the canonical society.

Minor issue — output encoding specification. “Exact real algebraic type masses” does not specify a finite encoding format. The construction claim would be more directly verifiable if the prover named the representation used for sample coordinates and identified the sampling theorem or book location supporting its size and computation bounds.

Minimum clarification: Specify the exact algebraic-number representation and the corresponding sampling reference. This is an expositional clarification of the invoked algorithm, requiring no new mathematical argument.

7. Overall adjudication

Both requested tasks are established in substance. The argument handles the threshold boundary, voting ties, zero lowest productivity, singleton supports, and countable original partitions. The sole identified issue concerns making the construction’s finite output specification explicit.

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