← back to the atlas

d4-journals-mss-2026-0031 (d4-journals-mss-2026-0031)

Answer: —

The anchor (named result in the paper)

Theorem 2 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateFor every instance such that the agents have at most two distinct preferences, every SD-EF assignment matrix is EF-decomposable.

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

The continuous mirror question, as graded

Given two atomless preference cohorts \(X_1,X_2\) of rational masses \(\mu_1,\mu_2>0\) summing to \(1\), ranked object classes \(J\) with rational supplies \(q_j>0\) summing to \(1\), and rational type-level marginals \(p_{tj}\), assume \(\sum_j p_{tj}=1\), \(\sum_t\mu_t p_{tj}=q_j\), and SD-EF for every ranking prefix. Can one compute in time polynomial in \(|J|\) and the input bit length a finite lottery over deterministic allocations, represented by finite interval partitions of each cohort, such that every outcome assigns each agent one whole class and allocates mass \(q_j\) of each class, every agent \(x\in X_t\) receives class \(j\) with probability \(p_{tj}\), and for every distinct pair \(x\in X_t,y\), the probability that \(x\)'s assigned class is preferred to \(y\)'s is at most \(1/2\)?

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

A society is given by its support: the list of its \(\tau=2\) preference types with positive masses, encoded as binary rationals; \(\tau\) counts supported types, not possible rankings. Let \(m=|J|\ge2\), and let \(L\) be the total input bit length.
Type \(t\) has a strict ranking \(\succ_t\) of \(J\) and consists of the tagged interval \(X_t=[0,\mu_t)\) with Lebesgue mass, where \(\mu_t>0\) and \(\mu_1+\mu_2=1\). The two rankings are distinct; agents receiving the same class are indifferent.
Supplies \(q_j>0\) and marginals \(p_{tj}\ge0\) are binary rationals satisfying \(\sum_jq_j=1\), \(\sum_jp_{tj}=1\), and \(\sum_t\mu_tp_{tj}=q_j\). Assume SD-EF: for every prefix \(B\) of \(\succ_t\) and every type \(u\), \(\sum_{j\in B}p_{tj}\ge\sum_{j\in B}p_{uj}\).
A deterministic allocation \(A:X_1\sqcup X_2\to J\) is represented by finite partitions into half-open intervals with rational endpoints, each labeled by one class, and satisfies \(\operatorname{mass}(A^{-1}(j))=q_j\) for every \(j\).
A feasible lottery is a finite list of such allocations with positive rational weights summing to \(1\), satisfying \(\Pr[A(x)=j]=p_{tj}\) for every \(x\in X_t\) and \(\Pr[A(y)\succ_t A(x)]\le\tfrac12\) for every distinct pair \(x\in X_t,y\in X_1\sqcup X_2\). These requirements hold pointwise, including partition endpoints.

Is constructing a feasible lottery, or correctly reporting that none exists, solvable in polynomial time in \(m,\tau,L\), or is this computational problem NP-hard?

For finite societies with equally many agents and distinct objects and at most two strict preference types, every SD-EF matrix admits such an envy-bounded decomposition, constructible in polynomial time. [Discrete result](https://arxiv.org/html/2604.16973v1)
For unrestricted finite preference profiles and rational assignment matrices without the SD-EF promise, deciding whether an envy-bounded decomposition exists is strongly NP-complete. [Later result](https://arxiv.org/html/2609.35192v1)
No result settling the atomless problem with the representation above was located.

Modeling choices made when packaging the task

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

Proven results and remaining hardness question

The required explicit lottery cannot always be constructed in polynomial time in the input length: some promised inputs require exponentially many outcomes.

Nevertheless, every promised input is feasible. I prove this constructively, with polynomial preprocessing and polynomial delay between outcomes. I also prove a further support-size bound that applies even when supplies are bounded away from zero.

These results do not establish NP-hardness of the explicit search problem. Thus the requested hardness classification remains incomplete.

1. An exponential output-size obstruction

Suppose a feasible lottery has $K$ outcomes $A_1,\ldots,A_K$. For a class $j$, define
$$ S_j=\bigsqcup_{t:p_{tj}>0}X_t, \qquad s_j=\sum_{t:p_{tj}>0}\mu_t. $$

Every point of $S_j$ must receive $j$ in some outcome, because its prescribed probability of receiving $j$ is positive. Therefore
$$ S_j\subseteq\bigcup_{\ell=1}^K A_\ell^{-1}(j). $$

Each set $A_\ell^{-1}(j)$ has mass $q_j$. Subadditivity of Lebesgue mass gives
$$ s_j\leq Kq_j, \qquad K\geq\left\lceil\frac{s_j}{q_j}\right\rceil. $$

This bound does not use SD-EF or the envy inequalities.

For an explicit family, take two classes $a,b$, masses $\mu_1=\mu_2=\tfrac12$, and distinct rankings
$$ a\succ_1 b, \qquad b\succ_2 a. $$

For an integer $n\geq1$, set
$$ p_{1a}=p_{2a}=q_a=2^{-n}, \qquad p_{1b}=p_{2b}=q_b=1-2^{-n}. $$

All promises hold. In particular, identical marginal rows satisfy every SD-EF inequality with equality. The input length is $O(n)$, while the preceding bound gives
$$ K\geq2^n. $$

The bound is attained. Write $N=2^n$ and identify the tagged population with $[0,1)$ using
$$ \phi(t,x)= \begin{cases} x,&t=1,\\ \tfrac12+x,&t=2. \end{cases} $$

For each $\ell\in\{0,\ldots,N-1\}$, use an outcome assigning $a$ precisely to
$$ \phi^{-1}\bigl([\ell/N,(\ell+1)/N)\bigr) $$
and assigning $b$ elsewhere. Give each outcome weight $1/N$.

Every outcome has the required supplies, and every point receives $a$ exactly once. For a type-1 observer, strict envy requires the other point to receive $a$; for a type-2 observer, it requires the observer to receive $a$. Either event occurs in at most one outcome, so every directed envy probability is at most
$$ \frac1N\leq\frac12. $$

The half-open partitions make these statements valid at every endpoint.

Consequently, polynomial total-time construction of the stipulated explicit list is impossible, independently of any complexity-theoretic assumption.

2. A polynomial-time integer-count decomposition

The following lemma is the finite preprocessing step of the general construction.

Lemma. Let $c_1,\ldots,c_m$ be nonnegative integers, let $r$ be an integer, and suppose a rational vector $a$ satisfies
$$ 0\leq a_j\leq c_j, \qquad \sum_j a_j=r. $$

One can compute, in polynomial time in the binary input length, positive rational weights $\beta_1,\ldots,\beta_H$ and integer vectors $h^{(1)},\ldots,h^{(H)}$, where $H\leq m+1$, such that
$$ \sum_{\ell=1}^H\beta_\ell=1, \qquad \sum_{\ell=1}^H\beta_\ell h^{(\ell)}=a, $$
and
$$ 0\leq h_j^{(\ell)}\leq c_j, \qquad \sum_j h_j^{(\ell)}=r. $$

Proof. Maintain rational residuals $z,w$, initially $z=a$ and $w=1$, satisfying
$$ 0\leq z_j\leq wc_j, \qquad \sum_jz_j=wr. $$

While $w>0$, choose an integer vector $h$ satisfying
$$ h_j=0\quad\text{if }z_j=0, \qquad h_j=c_j\quad\text{if }z_j=wc_j, $$
together with
$$ 0\leq h_j\leq c_j, \qquad \sum_jh_j=r. $$

To justify existence, fix the prescribed coordinates first. The remaining required sum is an integer. The feasible vector $z/w$ shows that this sum lies between zero and the sum of the remaining integer capacities. Greedily filling those capacities therefore produces the desired $h$.

Choose $\beta$ as the minimum of $w$ and all applicable ratios
$$ \frac{z_j}{h_j}\quad(h_j>0), \qquad \frac{wc_j-z_j}{c_j-h_j}\quad(h_j<c_j). $$

All applicable ratios are positive. At a lower boundary, $h_j=0$; at an upper boundary, $h_j=c_j$; and an interior coordinate has positive slack at both boundaries.

Record $(\beta,h)$ and update
$$ z\leftarrow z-\beta h, \qquad w\leftarrow w-\beta. $$

The first family of ratios ensures nonnegative new coordinates. The second ensures
$$ z_j-\beta h_j\leq(w-\beta)c_j. $$
The sum identity is preserved because $\sum_jh_j=r$.

Existing boundary coordinates remain on their boundaries. If $\beta<w$, a minimizing ratio must make a previously interior coordinate a boundary coordinate: ratios arising from existing boundaries equal $w$. Hence there are at most $m$ iterations with $\beta<w$, followed by at most one final iteration.

When $w=0$, residual feasibility forces $z=0$. The recorded terms therefore give the asserted decomposition.

For bit complexity, handle the all-zero-capacity case separately: then $r=0$, $a=0$, and one term suffices. Otherwise put $M=\max_jc_j\geq1$. If the current residuals share denominator $D$, a selected ratio has a denominator dividing $Dd$ for some positive integer $d\leq M$, or dividing $D$ when $\beta=w$. The updated residuals share this enlarged denominator. Thus at most $m+1$ steps increase its bit length by at most
$$ (m+1)\log_2 M. $$
All residual magnitudes remain bounded by the original capacities. The greedy choices and rational arithmetic consequently have polynomial bit complexity. $\square$

3. Construction for every promised input

Choose a common denominator $N$ of the masses and supplies, and define
$$ r=N\mu_1,\qquad s=N\mu_2,\qquad c_j=Nq_j. $$

These are positive integers satisfying
$$ r+s=N=\sum_jc_j. $$

Set
$$ a_j=rp_{1j}. $$

The supply equations imply
$$ c_j=rp_{1j}+sp_{2j}. $$
Therefore
$$ 0\leq a_j\leq c_j, \qquad \sum_ja_j=r. $$

Apply the lemma to obtain $(\beta_\ell,h^{(\ell)})$.

Partition $X_1$ into $r$ consecutive half-open cells of length $1/N$, and $X_2$ into $s$ such cells. Fix one component $h=h^{(\ell)}$.

On the type-1 cell indices, choose a labeling $f_1$ consisting of consecutive class blocks with counts $h_j$. On the type-2 indices, choose such a labeling $f_2$ with counts $c_j-h_j$. Any fixed ordering of the classes suffices.

Write $d_1=r$ and $d_2=s$. Independently for each type, choose uniformly
$$ u_t\in\{0,\ldots,d_t-1\}, \qquad \varepsilon_t\in\{-1,1\}. $$

Every point in type-$t$ cell $i$ receives
$$ f_t\bigl((u_t+\varepsilon_t i)\bmod d_t\bigr). $$

For this component, list all $4rs$ parameter choices, each with weight
$$ \frac{\beta_\ell}{4rs}. $$
Repeated allocations can remain separate list entries.

Supplies and interval representation

Each parameter choice permutes the cells within each type. Class $j$ therefore receives total mass
$$ \frac{h_j}{N}+\frac{c_j-h_j}{N} =\frac{c_j}{N} =q_j. $$

A circular shift or reflection preserves the number of circular class blocks. Cutting the circle into an interval splits at most one block, so each type needs at most $m+1$ intervals. All endpoints are rational multiples of $1/N$.

The outcome weights are positive and rational. Summing over the $4rs$ parameter choices gives weight $\beta_\ell$, and summing over components gives total weight one.

Pointwise marginals

For a fixed cell $i$, the index $(u_t+\varepsilon_t i)\bmod d_t$ is uniform. Conditional on $h$, the probabilities of class $j$ are therefore
$$ \frac{h_j}{r}\quad\text{for type 1}, \qquad \frac{c_j-h_j}{s}\quad\text{for type 2}. $$

Averaging over components gives
$$ \sum_\ell\beta_\ell\frac{h_j^{(\ell)}}r =\frac{a_j}{r} =p_{1j} $$
and
$$ \sum_\ell\beta_\ell\frac{c_j-h_j^{(\ell)}}s =\frac{c_j-a_j}{s} =p_{2j}. $$

Every point, including an internal cell boundary, belongs to exactly one half-open cell. Thus these are pointwise identities.

4. Proof of every envy inequality

Points of the same type

Fix two cell indices $i,k$ in a type with $d$ cells. The map
$$ (u,\varepsilon) \longmapsto \bigl(u+\varepsilon(i+k)\bmod d,-\varepsilon\bigr) $$
is a bijection of the equally weighted parameter choices. It exchanges the transformed indices of $i$ and $k$.

Thus, conditional on each component, the pair of received classes has a distribution invariant under exchanging the points. Since the points have the same ranking, their two directed strict-envy events have equal probabilities. These events are disjoint, so each probability is at most $\tfrac12$.

Distinct points in the same cell always receive the same class and have zero strict-envy probability. Averaging over components preserves all these bounds.

A type-1 point comparing itself with a type-2 point

Index classes according to type 1’s ranking:
$$ 1\succ_1 2\succ_1\cdots\succ_1 m. $$

Define
$$ C_0=0,\qquad C_j=\sum_{i=1}^jc_i, \qquad v_j=C_{j-1}+\frac{c_j}{2}. $$

SD-EF says that, for every prefix,
$$ \frac{\sum_{j=1}^ka_j}{r} \geq \frac{\sum_{j=1}^k(c_j-a_j)}s. $$

Multiplying by $rs>0$ and using $r+s=N$ yields
$$ D_k:=\sum_{j=1}^k\left(a_j-\frac rN c_j\right)\geq0. $$
Also $D_m=0$.

Put $b_j=a_j-(r/N)c_j$, so $b_j=D_j-D_{j-1}$ with $D_0=D_m=0$. Consequently,
$$ \sum_{j=1}^m b_jv_j = -\sum_{k=1}^{m-1}D_k(v_{k+1}-v_k) \leq0, $$
because
$$ v_{k+1}-v_k=\frac{c_k+c_{k+1}}2>0. $$

Moreover,
$$ \sum_jc_jv_j = \frac12\sum_j(C_j^2-C_{j-1}^2) = \frac{N^2}{2}. $$
It follows that
$$ \sum_ja_jv_j\leq\frac{rN}{2}. $$

Conditional on $h$, the two points’ classes are independent, because their types use independent parameters. The type-1 point’s strict-envy probability is
$$ E_h=\frac1{rs}\sum_{i<j}h_j(c_i-h_i). $$

Using $\sum_jh_j=r$, expand:
$$ \begin{aligned} rsE_h &=\sum_jh_jC_{j-1}-\sum_{i<j}h_ih_j\\ &=\sum_jh_jC_{j-1} -\frac12\left(r^2-\sum_jh_j^2\right). \end{aligned} $$

Take expectation over the components, for which $\mathbb E[h_j]=a_j$. Since $v_j=C_{j-1}+c_j/2$,
$$ rs\,\mathbb E[E_h] = \sum_ja_jv_j-\frac{r^2}{2} -\frac12\mathbb E\!\left[\sum_jh_j(c_j-h_j)\right]. $$

Every term $h_j(c_j-h_j)$ is nonnegative. Hence
$$ rs\,\mathbb E[E_h] \leq \frac{rN}{2}-\frac{r^2}{2} = \frac{rs}{2}. $$
Dividing by $rs>0$ proves the required bound.

A type-2 point comparing itself with a type-1 point

Reorder the classes by type 2’s ranking and apply exactly the preceding argument with
$$ (r,s,a,h)\longmapsto(s,r,c-a,c-h). $$

The substituted counts satisfy
$$ 0\leq c_j-h_j\leq c_j, \qquad \sum_j(c_j-h_j)=s, \qquad \mathbb E[c_j-h_j]=c_j-a_j. $$

Type 2’s SD-EF inequalities give the required nonnegative prefix differences. All the remaining identities and nonnegativity arguments apply unchanged. Thus this directed envy probability is also at most $\tfrac12$.

This proves universal feasibility.

5. Computational guarantees of the construction

The denominator $N$ can be chosen as the product of the input denominators of the masses and supplies. Its bit length is $O(L)$, although its numerical value may be exponential in $L$.

The count decomposition has polynomial preprocessing cost. The constructed lottery has
$$ K=4rsH\leq4rs(m+1) $$
entries.

Each entry can be generated in polynomial time in $m,L$ without scanning all cells. For example, a block $[b,e)$ of integer indices has inverse image under a shift equal to the circular interval
$$ [b-u,e-u), $$
and under a reflected shift equal to
$$ [u-e+1,u-b+1). $$
Reducing these intervals modulo the number of cells splits each into at most two ordinary intervals. Scaling the resulting boundaries by $1/N$ produces the rational interval representation.

All component weights have polynomial bit length by the lemma. Dividing by $4rs$ preserves that property.

The construction consequently provides:

The generator is an auxiliary representation; the requested output remains the full list.

An explicit proposed lottery can also be verified in polynomial time in its combined input and output length. Refine each type’s intervals using all endpoints appearing in all outcomes. On every refined cell, the vector of received classes across outcomes is constant. Checking marginals on these cells therefore checks every point. Checking all ordered pairs of refined cells checks every directed envy inequality; two points in the same refined cell always receive identical classes. Supplies and rational weights are checked directly. The number of refined cells is bounded by the total number of supplied interval endpoints, so all these checks are polynomial.

6. A further support bound from rational denominators

The small-supply bound in Section 1 is not the only constraint on support size.

Proposition. Suppose one class $a$ has supply $q\in(0,1)$ and every point has marginal probability $q$ of receiving $a$. Write $q$ in lowest terms with denominator $D$. If an explicit lottery has $K$ outcomes, then
$$ D\leq(K+1)^{(K+1)/2}. $$

This proposition requires neither SD-EF nor envy bounds.

Proof. Let the positive outcome weights be $\lambda_1,\ldots,\lambda_K$. Every point $x$ has an allocation pattern
$$ S(x)=\{i:A_i(x)=a\}\subseteq\{1,\ldots,K\}. $$

Pointwise marginal equality gives
$$ \sum_{i\in S(x)}\lambda_i=q. $$

Let $\mathcal T$ consist of the patterns having positive population mass, and let $\alpha_S$ be the mass of pattern $S$. There are finitely many patterns, and
$$ \sum_{S\in\mathcal T}\alpha_S=1. $$

Define the $0$–$1$ matrix
$$ M_{iS}=\mathbf 1_{\{i\in S\}}. $$

The supply of $a$ in every outcome and the pointwise marginal identity imply
$$ M\alpha=q\mathbf 1, \qquad \lambda^{\mathsf T}M=q\mathbf 1^{\mathsf T}, \qquad \sum_i\lambda_i=1. $$

Consider the finite linear program maximizing $v$ subject to
$$ M\gamma\geq v\mathbf 1, \qquad \gamma\geq0, \qquad \sum_S\gamma_S=1, \qquad 0\leq v\leq1. $$

The choice $(\gamma,v)=(\alpha,q)$ is feasible. Conversely, multiplying the payoff inequalities by $\lambda^{\mathsf T}$ gives
$$ v\leq\lambda^{\mathsf T}M\gamma =q\sum_S\gamma_S =q. $$
Thus the optimum is exactly $q$.

The feasible polytope is nonempty and compact, so its optimal face has a vertex, which is also a vertex of the feasible polytope. Choose such an optimal vertex and suppose its $\gamma$ has $d$ positive coordinates.

The bounds on $v$ are inactive because $0<q<1$. Restricting to the $d$ positive coordinates and $v$, the active equalities must have rank $d+1$. Otherwise a nonzero perturbation preserving them could be taken in both directions, small enough to preserve positivity and every inactive inequality, contradicting the vertex property.

One equality is the normalization. Hence $d$ linearly independent payoff equalities can be selected with it, and $d\leq K$. These equations form a nonsingular integer system
$$ Bz=b $$
of dimension $d+1$, whose payoff rows have entries from $\{0,1\}$ in the $\gamma$ columns and entry $-1$ in the $v$ column. The normalization row has $d$ entries equal to $1$ and last entry $0$; its right-hand side is $1$, while all payoff right-hand sides are zero.

Cramer’s rule shows that the reduced denominator $D$ of $v=q$ divides $|\det B|$. Hadamard’s determinant inequality gives
$$ |\det B| \leq (d+1)^{d/2}\sqrt d \leq (d+1)^{(d+1)/2} \leq (K+1)^{(K+1)/2}. $$
This proves the bound. $\square$

For example, retain the two opposite rankings and equal type masses, but take, for $n\geq2$,
$$ p_{1a}=p_{2a}=q_a =\frac{2^{n-1}+1}{2^n}, \qquad p_{1b}=p_{2b}=q_b=1-q_a. $$

Both supplies are at least $\tfrac14$, and every promise holds. The numerator of $q_a$ is odd, so its reduced denominator is $2^n$. Therefore every feasible lottery satisfies
$$ n\leq\frac{K+1}{2}\log_2(K+1). $$
In particular,
$$ K=\Omega\!\left(\frac n{\log n}\right). $$

Thus a constant lower bound on supplies does not give a constant upper bound on the required number of outcomes. This additional bound does not rule out polynomial-time construction for that restricted family.

7. What is settled, and what remains open

The results establish that:

The finite two-type existence theorem concerns assignments of distinct objects and does not remove the atomless representation’s output-size obstruction. [Discrete result](https://arxiv.org/html/2604.16973v1)

The later hardness theorem concerns deciding decomposability for unrestricted finite profiles and arbitrary rational bistochastic matrices. Its hypotheses do not establish hardness under this task’s two-type SD-EF promises. [Theorem 7.1](https://arxiv.org/html/2609.35192v1#S7)

The remaining issue is NP-hardness of the explicit search problem under a specified search-reduction notion. An exponential output lower bound alone is not such a reduction. The promised feasibility decision problem itself has only yes-instances.

⟨structured verdict parsed — rendered above⟩

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

The output is partial, with substantial correct results. The universal-feasibility construction, exponential output-size obstruction, computational guarantees, and denominator-based support bound are rigorous. I found no false mathematical step in those arguments.

The requested complexity classification remains incomplete: the prover rules out polynomial total-time construction in the stipulated representation but does not establish NP-hardness. It explicitly acknowledges this limitation.

1. Exponential output-size obstruction

Verified.

For every point $x\in S_j$, the positive prescribed marginal $p_{tj}$ requires at least one listed outcome to assign $j$ to $x$. Hence the asserted set inclusion is pointwise, not merely almost everywhere:
$$ S_j\subseteq\bigcup_{\ell=1}^K A_\ell^{-1}(j). $$

All allocation fibers are measurable, and each has mass $q_j$. Finite subadditivity therefore gives
$$ s_j\leq Kq_j. $$
Since $K$ is an integer and $q_j>0$, the ceiling bound follows.

The example satisfies all task promises:

Its binary input length is $O(n)$, and $s_a=1$, so every feasible explicit lottery requires
$$ K\geq2^n. $$

The proposed matching construction also checks out. Every point belongs to exactly one of the $N$ half-open blocks and receives $a$ in exactly one outcome. A type-$1$ observer can strictly envy only when the other point receives $a$; a type-$2$ observer can strictly envy only when the observer receives $a$. Each necessary event has probability $1/N$, which is at most $1/2$, including the base case $n=1$.

Thus the output proves an unconditional obstruction to polynomial total-time construction of the required explicit list. It does not prove NP-hardness, and the prover correctly distinguishes those statements.

2. Integer-count decomposition lemma

Verified, including termination and bit complexity.

The hypotheses imply that $r$ is a feasible integer total. After fixing boundary coordinates, the remaining required total is an integer lying between zero and the sum of the remaining integer capacities. The stated greedy filling therefore produces a permissible $h$.

All applicable ratios are positive:

Coordinates with $c_j=0$ cause no difficulty: both prescriptions give $h_j=0$, and neither ratio applies.

The two ratio families enforce precisely the two residual bounds
$$ 0\leq z_j-\beta h_j\leq(w-\beta)c_j. $$
The sum invariant is preserved because $\sum_jh_j=r$.

Existing boundary coordinates remain boundary coordinates. Every applicable ratio from such a coordinate equals $w$. Consequently, an iteration with $\beta<w$ makes at least one previously interior coordinate a boundary coordinate. There are at most $m$ such iterations, followed by at most one terminating iteration. When $w=0$, the residual bounds force $z=0$, establishing the stated convex decomposition.

The denominator argument is also valid. Starting with a common denominator of polynomial bit length, each update enlarges it by a factor at most $M$, apart from updates requiring no enlargement. There are at most $m+1$ updates. Residual magnitudes remain bounded, so numerator lengths and rational arithmetic costs remain polynomial.

The all-zero-capacity case is explicitly handled. No missing lemma is needed here.

3. Construction and pointwise marginals

Verified.

A common denominator of the masses and supplies makes $r,s,c_j$ positive integers. The supply equations imply
$$ c_j=rp_{1j}+sp_{2j}, $$
so the lemma applies to $a_j=rp_{1j}$.

For every component, the type-specific counts are nonnegative integers with totals $r$ and $s$. Every map
$$ i\longmapsto(u_t+\varepsilon_t i)\bmod d_t $$
is a permutation, including when $d_t=1$. Thus every outcome has exactly the stipulated supply for each class.

Consecutive class blocks, circular shifts, and reflections give finite interval partitions. Cutting the resulting circular labeling introduces at most one additional block per type. Zero-count classes do not create a representation problem.

For each fixed cell, the transformed index is uniform because $u_t$ is uniform. Averaging the resulting conditional marginals over the count decomposition gives exactly $p_{1j}$ and $p_{2j}$, as written.

The endpoint treatment is sufficient: every point of each tagged interval belongs to exactly one half-open cell. The excluded right endpoint $\mu_t$ is not an agent. Thus the construction establishes the marginals everywhere required by the task.

4. Envy inequalities

Same-type comparisons

Verified.

The displayed transformation of $(u,\varepsilon)$ exchanges the two transformed cell indices and is a bijection of the equally weighted parameter choices. This establishes exchangeability of the received-class pair conditional on each component.

Under a shared strict ranking, the two directed strict-envy events are disjoint and have equal probabilities. Each therefore has probability at most $1/2$. Distinct points in the same cell receive identical classes in every outcome and have zero strict-envy probability.

Averaging over components preserves the bounds. Degenerate cases such as a type having only one cell are covered.

Type-$1$ comparisons with type-$2$

Verified; the signs and constants are correct.

Multiplying the SD-EF prefix inequality by $rs$ gives
$$ N\sum_{j=1}^k a_j\geq r\sum_{j=1}^k c_j, $$
which is exactly $D_k\geq0$. The total-count identities give $D_m=0$.

The summation-by-parts identity has the correct negative sign. Since
$$ v_{k+1}-v_k=\frac{c_k+c_{k+1}}2>0, $$
it yields the asserted upper bound on $\sum_j a_jv_j$. The identity
$$ c_jv_j=\frac{C_j^2-C_{j-1}^2}{2} $$
also verifies the telescoping calculation.

Conditional independence is justified by the independent parameter choices for the two types. The formula
$$ rsE_h=\sum_{i<j}h_j(c_i-h_i) $$
uses the correct envy orientation: the other point receives a class ranked above the observer’s class.

Both subsequent expansions are correct. In particular,
$$ rs\,\mathbb E[E_h] = \sum_j a_jv_j-\frac{r^2}{2} -\frac12\mathbb E\!\left[\sum_jh_j(c_j-h_j)\right]. $$
The final expectation is nonnegative, and the resulting upper bound is $rs/2$. Division is legitimate because $r,s>0$.

Type-$2$ comparisons with type-$1$

Verified.

The stated substitution preserves all hypotheses used in the preceding argument. Reordering by type $2$ and using its own SD-EF inequalities supplies the required prefix inequalities. The complementary counts have the correct total and expectation.

Together, these arguments cover every ordered pair required by the task and prove universal feasibility.

5. Computational guarantees and verification

Verified, with the claimed representations kept distinct.

The product-denominator choice has bit length $O(L)$. Although the cell counts can be exponentially large numerically, their binary representations have polynomial length.

The inverse-image formulas for shifted and reflected integer blocks are correct. In particular, the reflected formula’s offsets by $1$ correctly account for the exclusive upper endpoint. Processing the class blocks avoids enumerating all cells.

The component weights, outcome weights, and rational interval endpoints have polynomial bit length. Consequently, the claims of polynomial preprocessing, polynomial delay, output-sensitive polynomial time, and polynomial time per indexed entry are supported.

These claims do not imply polynomial total time in the original input length. The prover expressly preserves that distinction.

The explicit verification procedure is also valid. Common endpoint refinement makes the outcome-label vector constant on each refined cell, including its left endpoint. Marginal checks on these cells and envy checks on ordered pairs of cells therefore cover all points. Two points in the same refined cell always receive identical classes. The number of cells and the rational arithmetic costs are polynomial in the combined input and explicit-output length.

6. Denominator-based support bound

Verified.

The pattern equations follow from the common pointwise marginal and the supply constraint in every outcome. Patterns of zero population mass need not be included in $\mathcal T$; omitting them does not affect those equations.

The linear program has optimum exactly $q$: $(\alpha,q)$ is feasible, and multiplication by the nonnegative normalized weight vector $\lambda$ bounds every feasible $v$ by $q$.

The feasible polytope is nonempty and compact. An optimal vertex exists. At that vertex, the bounds on $v$ are inactive because $0<q<1$.

After restricting to the $d$ positive coordinates, the rank argument is valid. Rank deficiency would permit a sufficiently small two-sided perturbation preserving active equalities, positivity, and inactive inequalities, contradicting the vertex property. Normalization together with $d$ selected payoff equalities therefore gives a nonsingular system of dimension $d+1$, with $d\leq K$.

Cramer’s rule applies to the integer system and gives the claimed denominator divisibility. Hadamard’s inequality applies with payoff-row norms at most $\sqrt{d+1}$ and normalization-row norm $\sqrt d$, giving exactly the displayed determinant bound.

For the example with $n\geq2$, the numerator is odd, so the reduced denominator is $2^n$. Both supplies are at least $1/4$. The resulting inequality and asymptotic lower bound are correct.

As the prover notes, this additional bound does not exclude polynomial-size output for that restricted family.

7. External results and unresolved classification

The descriptions of the finite results match their stated domains. The earlier theorem concerns finite assignments of distinct objects with at most two preferences; the later hardness theorem concerns a supplied profile and rational bistochastic matrix without this task’s restrictions. Neither is applied as a theorem proving the atomless construction or its hardness. Their stated scope supports the prover’s caution. [Earlier Theorem 2](https://arxiv.org/html/2604.16973v1), [Later Theorem 7.1](https://arxiv.org/html/2609.35192v1#S7)

Major issue — target completeness, rather than a defect in the proved arguments. The output does not establish NP-hardness of the requested explicit construction problem. Exponential necessary output length rules out polynomial total-time construction but does not provide a hardness reduction.

The minimum additional specification needed for a verifiable hardness claim is the precise search-reduction notion and its treatment of potentially exponential outputs. Resolving the remaining branch would then require a hardness argument under that specification. This is substantive additional work, not an expositional repair.

The prover’s own claim of partial progress is accurate. Its established results should be retained; no repair to those mathematical arguments is required.

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