Answer: \(\mathrm{NP}\)-hard for every fixed \(k\ge 2\), even when \(r=\lfloor c_k\sqrt{\tau}\rfloor\) for a positive rational constant \(c_k\).
Theorem 5.2 — class: hardness
Given indivisible goods \(G=[m]\), \(k\) groups, rational additive types \(t=(i,v)\), and a rational mass distribution \(\mu\) over those types, together with \(r\), distinguish whether there is a partition \((A_1,\ldots,A_k)\) such that every type with \(\mu_t>0\) has exact consensus \(1/k\)-division, or whether no partition is \(\mathrm{PROP}_r\) for every such type.
Fix any constant \(k\ge 2\). Let \(G=[m]\), with \(m\ge 1\), be indivisible goods. A type \(t=(i,v_t)\) belongs to group \(i\in[k]\) and has a nonnegative rational additive valuation \(v_t\in\mathbb{Q}_{\ge 0}^{m}\); write \(v_t(S)\) for its value of a bundle.
A society is given by its support: the list of the \(\tau\) types with positive mass, each with its mass as a binary rational. Here \(\tau\) is the support size, not the number of possible types. Require \(\sum_t\mu_t=1\) and \(\sum_{t:i(t)=i}\mu_t=1/k\) for every group. Let \(L\) be the total input bit length.
An allocation \((A_1,\ldots,A_k)\) is an ordered partition of all goods; empty bundles are allowed. It is an exact consensus \(1/k\)-division if \(v_t(A_j)=v_t(G)/k\) for every supported type \(t\) and every \(j\in[k]\).
For an input integer \(r\ge 0\), it is \(\mathrm{PROP}_r\) if every supported type \(t=(i,v_t)\) admits a set \(B_t\subseteq G\setminus A_i\), with \(|B_t|\le r\), such that \(v_t(A_i)\ge v_t(G)/k-v_t(B_t)\). These conditions apply separately to every supported type.
Promise that either YES: an exact consensus division exists; or NO: no allocation is \(\mathrm{PROP}_r\) for all supported types.
For each fixed \(k\ge 2\), is distinguishing these promised cases solvable in time \(\operatorname{poly}(m,\tau,L)\), or is it NP-hard, with \(r\) part of the input?
For finite societies with \(n'\) agents in each group, this distinction is NP-hard at relaxation \(\lfloor\varepsilon_k\sqrt{n'}\rfloor\) for some constant \(\varepsilon_k>0\); a deterministic polynomial-time algorithm achieves relaxation \(O(\sqrt{n})\) for \(n\) total agents. [Manurangsi–Suksompong](https://arxiv.org/html/2105.01609v2)
No result specifically addressing the stated distribution formulation was identified in the literature search.
For every fixed \(k\ge 2\), the promised distinction is \(\mathrm{NP}\)-hard. More strongly, there is a positive rational constant \(c_k\) such that hardness holds even under the restriction \(r=\lfloor c_k\sqrt{\tau}\rfloor\).
Thus the result concerns a relaxation depending on the support size, beyond the special case \(r=0\).
Fix \(k\ge 2\). By [Manurangsi–Suksompong, Theorem 5.2](https://arxiv.org/html/2105.01609v2#S5), there is a constant \(\varepsilon_k>0\) for which the following distinction is \(\mathrm{NP}\)-hard. The input explicitly lists \(n'\) agents in each of \(k\) groups, with additive valuations:
Their definition of proportionality up to goods is exactly the definition in the question.
The theorem applies to rational inputs. Indeed, its construction starts with matrix entries in \(\{0,\tfrac12,1\}\), applies a Boolean matrix product and division by a fixed positive integer, and uses the resulting entries as valuations. Hence its hard instances have nonnegative rational valuations with polynomial encoding length.
Consider such a finite instance. For each group \(i\), let \(V_i\) be the set of distinct valuation vectors occurring in that group. For \(v\in V_i\), define its multiplicity by
\[
\]
\(d_{i,v}:=\bigl|\{a:\ a\text{ belongs to group }i\text{ and has valuation }v\}\bigr|\).
Create one supported type \(t=(i,v)\) with mass
\[
\]
\(\mu_{i,v}:=\dfrac{d_{i,v}}{kn'}\).
Here rational numerators and denominators are encoded in binary. Every listed mass is positive. Since each group contains exactly \(n'\) agents,
\[
\]
\(\displaystyle\sum_{v\in V_i}\mu_{i,v}=\frac{n'}{kn'}=\frac1k,\qquad \sum_{i=1}^{k}\sum_{v\in V_i}\mu_{i,v}=1.\)
Thus the constructed society satisfies every mass constraint, and its support size obeys \(\tau=\sum_i|V_i|\le kn'\).
We now verify predicate preservation for every allocation.
Exact consensus. Its equalities depend only on the valuation vector. Replacing multiple copies of a vector by one supported type therefore preserves every equality. Consequently, an allocation is an exact consensus division for the finite instance if and only if it is one for the constructed society.
Proportionality. Fix a nonnegative integer \(s\). All agents with the same pair \((i,v)\) have precisely the same requirement:
\[
\]
\(\displaystyle\exists B\subseteq G\setminus A_i,\quad |B|\le s,\quad v(A_i)\ge \frac{v(G)}k-v(B).\)
If this requirement holds for the type, its witnessing set works for each corresponding agent. Conversely, a witness for any corresponding agent works for the type. Therefore, an allocation satisfies \(\mathrm{PROP}_s\) for every finite agent if and only if it satisfies \(\mathrm{PROP}_s\) for every supported type.
Choose a positive integer \(q_k\), depending only on fixed \(k\), sufficiently large that \(\sqrt{k}/q_k\le\varepsilon_k\). Set \(c_k:=1/q_k\) and output
\[
\]
\(\displaystyle r:=\left\lfloor\frac{\sqrt{\tau}}{q_k}\right\rfloor=\lfloor c_k\sqrt{\tau}\rfloor.\)
This integer is computed exactly as the largest nonnegative integer \(h\) satisfying \(q_k^2h^2\le\tau\); no approximation of a square root is needed.
Because \(\tau\le kn'\),
\[
\]
\(\displaystyle r\le\frac{\sqrt{\tau}}{q_k}\le\frac{\sqrt{kn'}}{q_k}\le\varepsilon_k\sqrt{n'}.\)
Since \(r\) is integral, it follows that \(r\le\lfloor\varepsilon_k\sqrt{n'}\rfloor\).
We verify the two promised cases:
Hence every promised source instance maps to the corresponding promised target case.
The source instance explicitly lists all \(kn'\) valuation vectors. Grouping equal vectors can be done in polynomial time by exact rational comparison. Every mass numerator and denominator has bit length \(O(\log(kn'))\); valuations are copied without enlargement; and \(\tau\le kn'\). The output relaxation also has polynomial encoding length. Thus the reduction runs in polynomial time and produces a polynomial-size instance.
A distinguishing algorithm running in \(\operatorname{poly}(m,\tau,L)\) would therefore distinguish the finite hard instances in polynomial time. This proves \(\mathrm{NP}\)-hardness for every fixed \(k\ge2\), including the restriction \(r=\lfloor c_k\sqrt{\tau}\rfloor\).
⟨structured verdict parsed — rendered above⟩
The output resolves the assigned promise problem in substance. The reduction is correct, including the stronger restriction \(r=\lfloor c_k\sqrt{\tau}\rfloor\). I found two minor presentation issues and no blocking mathematical gap.
[Manurangsi–Suksompong, Theorem 5.2](https://arxiv.org/html/2105.01609v2#S5) states the claimed hardness for every fixed \(k\ge 2\), with equally sized groups, exact consensus in YES instances, and failure of proportionality up to \(\varepsilon_k\sqrt{n'}\) goods in NO instances. Definition 2.1 uses precisely the outside-bundle witness condition required by USER_TASK.
The theorem’s nonintegral relaxation is consistently interpreted using its floor: the cardinality of a witnessing set is an integer. Thus the prover’s stated source promise is valid.
The cited construction starts with entries in \(\{0,\tfrac12,1\}\), multiplies arithmetically by a matrix with Boolean entries, scales by a fixed constant, and copies the resulting rows into agents’ valuations. It produces nonnegative rational valuations of polynomial encoding length. [Source construction](https://arxiv.org/html/2105.01609v2#S5.SS1)
Minor issue: “applies a Boolean matrix product” is inaccurate terminology. Boolean matrix multiplication ordinarily refers to a different operation, and one factor here contains fractional entries.
Minimum clarification: Specify that this is ordinary arithmetic matrix multiplication by a matrix with Boolean entries. The rational-encoding conclusion survives this correction.
Multiplicity \(d_{i,v}\) is positive for every \(v\in V_i\), so every listed mass is positive. The denominator \(kn'\) is positive because the source groups are nonempty.
The displayed mass calculations are correct: multiplicities sum to \(n'\) within each group, giving group mass \(1/k\) and total mass \(1\). Types retain their group labels; equal valuations in different groups are therefore correctly treated as different types.
The bound \(\tau\le kn'\) follows directly from aggregation. No lower bound on the number of distinct valuations is needed.
For every allocation, repeated agents with identical valuations impose identical equalities on every bundle. Each source agent has a corresponding supported type, and each supported type represents at least one source agent. Consequently, aggregation neither removes a distinct consensus constraint nor introduces a new one.
The argument applies to empty bundles and zero valuation vectors without exceptions.
The prover fixes an arbitrary nonnegative integer \(s\) and compares the predicates for every allocation. Agents sharing the pair \((i,v)\) have the same own bundle, valuation, admissible witness sets, and inequality.
A type’s witness can be reused for all corresponding agents. Conversely, any corresponding agent’s witness establishes the type’s requirement. The argument does not incorrectly require different types to share a witness.
A positive integer \(q_k\) satisfying \(\sqrt{k}/q_k\le\varepsilon_k\) exists because \(\varepsilon_k>0\). Since \(k\) is fixed, \(q_k\) is a fixed constant and \(c_k=1/q_k\) is positive and rational.
The integer characterization \(q_k^2h^2\le\tau\) computes exactly the stated floor. Finding the largest such integer is a routine polynomial-time integer computation; no numerical approximation assumption is hidden here.
Every inequality in the comparison with \(\varepsilon_k\sqrt{n'}\) has the correct direction. Integrality then justifies the final floor bound. The case \(r=0\) is included.
The YES implication follows from exact-consensus preservation.
For NO, an allocation satisfying the smaller relaxation \(r\) would also satisfy the source relaxation using the same witnesses. This contradicts the source NO promise. The prover uses monotonicity in the correct direction.
Exact consensus itself satisfies \(\mathrm{PROP}_r\) with empty witnesses, so the target YES and NO cases are disjoint.
Exact comparison of binary rationals and grouping equal vectors take polynomial time in the explicit source encoding. Multiplicities and mass denominators have the claimed logarithmic bit length. The valuations and goods are retained, and the output support cannot exceed the source agent count.
Therefore the target parameters and total encoding length are polynomially bounded by the source input length. A target algorithm polynomial in \(m,\tau,L\) would give a polynomial-time source distinguisher.
Several formulas are preceded by empty display delimiters.
Minimum clarification: Remove those empty displays and render each formula once with valid delimiters. The intended formulas remain identifiable, so this does not obstruct mathematical verification.
The argument establishes the claimed hardness. Only terminology and mathematical markup require revision; no additional lemma or substantive 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.