Answer: —
Theorem 5.1 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateIn the indivisible-goods setting where agents have bi-valued utilities, \Cref{alg:efx_fpo} computes in polynomial time an integral allocation sampled from a randomized allocation that is ex-ante EF, ex-post EFX and ex-post fPO.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given \(m\) indivisible good kinds, rational \(0<a<b\), a finite type set \(T\subseteq\{a,b\}^{m}\) with rational mass distribution \(\mu\), and rational per-capita supplies \(\rho\in\mathbb{Q}_{\ge 0}^{m}\), compute a polynomial-size lottery or compact sampler over measurable assignments of integral bundles to a unit-mass population. Type-level expected bundles must satisfy ex-ante \(\mathrm{EF}\), while almost every realization must satisfy ex-post \(\mathrm{EFX}\) and continuum \(\mathrm{fPO}\), in time polynomial in \(m\), \(|T|\), and input length \(L\), rather than in the denominator-cleared population \(Q\).
Let \(m\geq1\), let \(0<a<b\) be binary rationals shared by all types, and let supplies be \(\rho\in\mathbb Q_{\geq0}^{m}\); utilities are additive.
A society is given by its support: the list of \(\tau\) types \(T\subseteq\{a,b\}^{m}\) with positive binary-rational masses \(\mu_t\), summing to \(1\). Here \(\tau=|T|\) is the support size, not the number of possible types; \(L\) is the total input bit length.
Represent the population by disjoint intervals \(I_t\) of lengths \(\mu_t\), with Lebesgue measure \(\lambda\); write \(t(x)\) for the type of person \(x\).
A feasible realization is a measurable assignment \(z(x)\in\mathbb Z_{\geq0}^{m}\) satisfying \(\int z_g\,d\lambda=\rho_g\) for every kind \(g\); multiple copies of a kind are allowed.
For a lottery over realizations, define \(\bar z_t=\mu_t^{-1}\mathbb E[\int_{I_t}z\,d\lambda]\). Type-level ex-ante EF means \(t\cdot\bar z_t\geq t\cdot\bar z_s\) for all \(t,s\in T\).
Ex-post EFX means that, for almost every pair \((x,y)\), \(t(x)\cdot z(x)\geq t(x)\cdot(z(y)-e_g)\) whenever \(z_g(y)>0\), where \(e_g\) is the unit vector for kind \(g\).
Continuum fPO means there is no measurable fractional assignment \(w(x)\in\mathbb R_{\geq0}^{m}\) with the same supplies, weakly improving utility almost everywhere and strictly improving it on a set of positive measure.
Compute a lottery whose realizations satisfy EFX and fPO with probability \(1\), and whose type-level expectations satisfy EF. Encode realizations by rational interval partitions with binary-encoded integral bundles; permit either an explicit rational lottery or an exact compact sampler producing such encodings.
Is this construction problem solvable in polynomial time in \(m,\tau,L\), or is it NP-hard, when output size and expected sampling time must also be polynomial in \(m,\tau,L\)?
For explicitly listed finite agents and individual goods with shared bi-valued utilities, a polynomial-time algorithm samples from a lottery satisfying ex-ante EF, ex-post EFX, and ex-post fPO ([verified result](https://arxiv.org/html/2410.06877v2#S5)).
No result settling this exact continuum construction problem was identified in the literature search.
I do not settle the general polynomial-time-versus-hardness question. I prove two additional results:
$$
\sum_g\rho_g\leq \frac ab.
$$
In this regime, a single deterministic realization suffices.
I also give a polynomial-time test extending the second construction to some larger-supply instances, and an explicit example showing why that test does not resolve the general problem.
For a feasible realization $z$, define
$$
A_{tg}=\int_{I_t}z_g\,d\lambda,
\qquad
U_t=\sum_g t_gA_{tg}.
$$
These quantities are finite: all coordinates are nonnegative, supplies are finite, and utility coefficients are bounded.
Lemma 1. The realization $z$ is continuum fPO if and only if there is no matrix $Y\in\mathbb R_{\geq0}^{T\times m}$ satisfying
$$
\sum_tY_{tg}=\rho_g
$$
for every $g$, and
$$
t\cdot Y_t\geq U_t
$$
for every $t$, with strict inequality for at least one type.
Proof. Suppose a measurable fractional assignment $w$ is a continuum Pareto improvement. Set
$$
Y_{tg}=\int_{I_t}w_g\,d\lambda.
$$
Integration gives the supply equalities and weak utility inequalities. The utility difference is a nonnegative integrable function almost everywhere. If it is positive on a set of positive measure, its integral is positive. Because there are finitely many types, at least one type inequality is strict.
Conversely, suppose such a matrix $Y$ exists. Write
$$
u(x)=t(x)\cdot z(x),
\qquad
V_t=t\cdot Y_t.
$$
For a type with $U_t>0$, define, on $I_t$,
$$
w_g(x)=\frac{u(x)}{U_t}Y_{tg}.
$$
Then $\int_{I_t}w_g\,d\lambda=Y_{tg}$, and its utility is
$$
t\cdot w(x)=\frac{V_t}{U_t}u(x)\geq u(x).
$$
If $V_t>U_t$, this improvement is strict wherever $u(x)>0$, a set of positive measure since $\int_{I_t}u\,d\lambda=U_t>0$.
For a type with $U_t=0$, nonnegativity implies $u(x)=0$ almost everywhere on $I_t$. Define
$$
w_g(x)=\frac{Y_{tg}}{\mu_t}.
$$
Its aggregate allocation is $Y_t$, and its utility is $V_t/\mu_t$. Thus it weakly improves utility and strictly improves it throughout that type when $V_t>0$.
These definitions produce a measurable fractional assignment with the required supplies and a strict improvement on a set of positive measure. $\square$
Set
$$
c=\frac ba>1,
\qquad
\varepsilon_{tg}=
\begin{cases}
0,&t_g=a,\\
1,&t_g=b.
\end{cases}
$$
Thus $t_g=a c^{\varepsilon_{tg}}$.
Given a feasible aggregate matrix $A$, construct a directed multigraph with vertex set $T$. For every incidence $(t,g)$ with $A_{tg}>0$, and every type $s$, insert an edge
$$
t\longrightarrow s
$$
labelled by $g$, with weight
$$
d(t,s;g)=\varepsilon_{tg}-\varepsilon_{sg}\in\{-1,0,1\}.
$$
Theorem 2. A feasible realization with aggregate matrix $A$ is continuum fPO if and only if this graph has no negative directed cycle.
Moreover, when it is fPO, there are integers
$$
h_t\in\{0,\ldots,\tau-1\}
$$
such that the rational weights and prices
$$
\beta_t=c^{h_t},
\qquad
p_g=\max_{s\in T}\beta_s s_g
$$
satisfy
$$
p_g\geq\beta_t t_g
$$
for every $t,g$, with equality whenever $A_{tg}>0$.
Suppose there is a negative directed cycle. We may choose one with distinct vertices: a negative closed walk with a repeated vertex splits into shorter closed walks, at least one of which is negative.
Write the cycle as
$$
t_1\longrightarrow t_2\longrightarrow\cdots
\longrightarrow t_k\longrightarrow t_1,
$$
and let $g_j$ label its $j$-th edge. Indices are cyclic. In particular,
$$
A_{t_jg_j}>0,
\qquad
\sum_{j=1}^k d(t_j,t_{j+1};g_j)<0.
$$
Transfer an amount $q_j>0$ of kind $g_j$ from type $t_j$ to type $t_{j+1}$. Starting with $q_1>0$, choose
$$
q_j=
\frac{t_j(g_{j-1})}{t_j(g_j)}q_{j-1},
\qquad 2\leq j\leq k.
$$
Every type $t_j$ with $j\geq2$ then has zero net utility change:
$$
t_j(g_{j-1})q_{j-1}-t_j(g_j)q_j=0.
$$
For type $t_1$, the ratio of gained utility to lost utility is
$$
\frac{t_1(g_k)q_k}{t_1(g_1)q_1}
=
\prod_{j=1}^k
\frac{t_{j+1}(g_j)}{t_j(g_j)}
=
c^{-\sum_{j=1}^k d(t_j,t_{j+1};g_j)}
>1.
$$
Its utility therefore strictly increases.
All $q_j$ are fixed positive multiples of $q_1$. Choose $q_1$ sufficiently small that
$$
q_j\leq A_{t_jg_j}
$$
for every $j$. The resulting aggregate matrix is nonnegative and preserves every supply. Types outside the cycle are unchanged.
It is consequently an aggregate Pareto improvement. Lemma 1 converts it into a continuum Pareto improvement.
Now suppose there is no negative directed cycle. Add a source vertex with a zero-weight edge to every type, and let $\ell_t$ be the shortest-path distance from the source to $t$.
These distances are finite. A shortest path can be chosen without repeated vertices, because every directed cycle has nonnegative weight. Such a path has at most $\tau-1$ edges between types. Since those edges have weights in $\{-1,0,1\}$ and there is a direct zero-weight source edge,
$$
-(\tau-1)\leq\ell_t\leq0.
$$
Every original edge satisfies
$$
\ell_s\leq\ell_t+d(t,s;g).
$$
Set
$$
h_t=\ell_t-\min_{r\in T}\ell_r.
$$
Then $h_t$ is an integer in $\{0,\ldots,\tau-1\}$. For every edge arising from $A_{tg}>0$,
$$
h_s-h_t\leq\varepsilon_{tg}-\varepsilon_{sg}.
$$
Exponentiating with base $c$ gives
$$
c^{h_s}s_g\leq c^{h_t}t_g.
$$
Thus, with $\beta_t=c^{h_t}$ and $p_g=\max_s\beta_s s_g$,
$$
p_g=\beta_t t_g
\qquad\text{whenever }A_{tg}>0.
$$
For any feasible fractional assignment $w$,
$$
\begin{aligned}
\sum_t\beta_t\int_{I_t}t\cdot w\,d\lambda
&\leq \sum_gp_g\rho_g\\
&=\sum_{t,g}\beta_t t_gA_{tg}\\
&=\sum_t\beta_tU_t.
\end{aligned}
$$
A continuum Pareto improvement would make the left side strictly larger than the last expression: every $\beta_t$ is positive, and a nonnegative integrable utility difference that is positive on a set of positive measure has positive integral. This is impossible. $\square$
The graph has $\tau$ vertices and at most $m\tau^2$ edges. Negative-cycle detection and shortest paths therefore take polynomial time.
For an encoded realization, determining whether $A_{tg}>0$ requires only checking whether some positive-length cell of type $t$ contains kind $g$.
The supporting weights and prices have polynomial binary length. Indeed, each exponent $h_t$ is at most $\tau-1$, and
$$
p_g\in\{a c^j:0\leq j\leq\tau\}.
$$
Hence fPO admits a rational certificate using at most $\tau+1$ geometric price levels.
This characterizes and verifies fPO, but it does not find bundle patterns that simultaneously satisfy EFX and expected EF.
Write
$$
R=\sum_g\rho_g.
$$
Theorem 3. If $R\leq a/b$, the requested construction is deterministically polynomial-time solvable in $m,\tau,L$. It produces one realization with at most $\tau(m+1)$ interval cells, each carrying either the empty bundle or one item.
If $R=0$, assign the empty bundle everywhere. Feasibility forces every nonnegative fractional alternative to be zero almost everywhere, so all required properties hold.
Assume henceforth that $R>0$, and let
$$
G_+=\{g:\rho_g>0\}.
$$
Kinds outside $G_+$ receive zero allocation.
Consider a linear Fisher market with one buyer per supported type:
We use the established algorithmic theorem that a linear Fisher market with positive rational budgets and rational utilities admits an exact rational equilibrium computable in polynomial time. [Orlin’s algorithm](https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol10171/DagSemProc.10171.2/DagSemProc.10171.2.pdf) provides such a computation.
Here the hypotheses hold: budgets are positive, and every buyer values every retained kind positively. To match the unit-supply formulation, replace kind $g$ by one unit whose value to buyer $t$ is $t_g\rho_g$. Clearing denominators of these coefficients and the budgets gives integer data of polynomial binary length. Rescaling the resulting equilibrium recovers prices per physical unit and allocations in the original quantities.
Let $p_g>0$ and $A_{tg}\geq0$ be the resulting prices and allocations. They satisfy
$$
\sum_tA_{tg}=\rho_g,
\qquad
\sum_gp_gA_{tg}=\mu_t.
$$
For
$$
\alpha_t=\max_{g\in G_+}\frac{t_g}{p_g},
$$
equilibrium optimality gives
$$
A_{tg}>0\ \Longrightarrow\ t_g=\alpha_t p_g.
$$
Define the per-person mean bundle
$$
x_t=\frac{A_t}{\mu_t}.
$$
Then
$$
p\cdot x_t=1,
\qquad
t\cdot x_t=\alpha_t.
$$
For every pair of types $t,s$,
$$
t\cdot x_s
\leq\alpha_t p\cdot x_s
=\alpha_t
=t\cdot x_t.
$$
Thus these means satisfy exactly the required type-level EF inequalities.
Let
$$
p_{\min}=\min_{g\in G_+}p_g,
\qquad
p_{\max}=\max_{g\in G_+}p_g.
$$
Choose a kind $h$ with price $p_{\max}$. Since $\rho_h>0$, some type $t$ receives a positive amount of it. For a kind $k$ with price $p_{\min}$, equilibrium optimality implies
$$
\frac{t_h}{p_{\max}}\geq\frac{t_k}{p_{\min}}.
$$
Consequently,
$$
\frac{p_{\max}}{p_{\min}}
\leq\frac{t_h}{t_k}
\leq\frac ba=c.
$$
The budgets sum to one, so
$$
1=\sum_gp_g\rho_g
\leq p_{\max}R
\leq c p_{\min}R.
$$
Therefore
$$
p_{\min}\geq\frac1{cR}.
$$
For every type,
$$
\sum_gx_{tg}
\leq\frac{p\cdot x_t}{p_{\min}}
=\frac1{p_{\min}}
\leq cR
\leq1.
$$
Equivalently,
$$
\sum_gA_{tg}\leq\mu_t.
$$
Inside $I_t$, assign a cell of length $A_{tg}$ the bundle $e_g$, for each positive $A_{tg}$. Assign the empty bundle to the remaining length
$$
\mu_t-\sum_gA_{tg}\geq0.
$$
All endpoints are rational.
The resulting realization has aggregate matrix $A$, so it is feasible and its type-level means are $x_t$. The preceding calculation proves EF.
Every bundle is empty or a singleton. Removing any present item from another person’s bundle leaves the empty bundle. Since utilities are nonnegative, EFX holds.
Finally, set $\beta_t=1/\alpha_t>0$. Then
$$
\beta_t t_g\leq p_g,
$$
with equality on every positive allocation incidence. The weighted-utility argument in Section 2.2 proves continuum fPO.
The construction uses at most $\tau(m+1)$ cells. All rational data have polynomial binary length, and the equilibrium computation and interval construction take polynomial time. A lottery concentrated on this realization is the requested output. $\square$
The numerical condition $R\leq a/b$ is sufficient, but the construction can apply more broadly.
Compute a Fisher equilibrium as above and retain its prices $p$ and values $\alpha_t$. Solve the following rational linear feasibility problem for $Y$:
$$
Y_{tg}\geq0,
\qquad
\sum_tY_{tg}=\rho_g,
$$
$$
\sum_gp_gY_{tg}=\mu_t,
\qquad
\sum_gY_{tg}\leq\mu_t,
$$
and
$$
Y_{tg}=0
\qquad\text{whenever }t_g<\alpha_t p_g.
$$
This system has polynomial size. If it is feasible, implement $Y$ using singleton and empty bundles.
The spending equalities and allocation only on maximum-ratio incidences give
$$
t\cdot\frac{Y_t}{\mu_t}=\alpha_t,
\qquad
t\cdot\frac{Y_s}{\mu_s}\leq\alpha_t.
$$
Hence EF holds. Singleton bundles give EFX, and weights $\beta_t=1/\alpha_t$ give fPO.
Thus this is a polynomial-time sufficient test for a deterministic solution. Its infeasibility is not a certificate that the original construction problem is difficult or infeasible.
Consider
$$
a=1,\qquad b=2,
$$
with two types
$$
t^0=(1,1),\qquad t^1=(2,1),
$$
masses
$$
\mu_{t^0}=\frac14,\qquad \mu_{t^1}=\frac34,
$$
and supplies
$$
\rho_1=\rho_2=\frac38.
$$
Here $R=3/4>a/b$.
Let $p_1,p_2$ be equilibrium prices.
If $p_1<p_2$, both types strictly prefer kind $1$ per unit of money, so kind $2$ cannot clear.
If $p_1=p_2$, type $t^1$ buys only kind $1$. Its budget forces
$$
p_1\frac38=\frac34,
$$
so $p_1=p_2=2$. Clearing kind $2$ would then require expenditure $3/4$ from type $t^0$, whose budget is only $1/4$. This is impossible.
Thus $p_1>p_2$, and type $t^0$ buys only kind $2$.
If $p_1<2p_2$, type $t^1$ buys only kind $1$. Clearing both kinds then gives
$$
p_1=2,\qquad p_2=\frac23,
$$
contradicting $p_1<2p_2$.
If $p_1>2p_2$, both types buy only kind $2$, so kind $1$ cannot clear.
Consequently,
$$
p_1=2p_2.
$$
Total expenditure is one, whence
$$
\frac38(p_1+p_2)=1,
\qquad
p_2=\frac89,\qquad p_1=\frac{16}{9}.
$$
Type $t^0$ must therefore receive
$$
A_{t^0,2}=\frac{1/4}{8/9}=\frac9{32}>\frac14=\mu_{t^0}.
$$
Its mean item count is $9/8$. The linear feasibility test in Section 4 is therefore infeasible at every equilibrium.
Assign the entire type-$t^0$ interval one item of kind $2$ per person. Within the type-$t^1$ interval, use cells of lengths
$$
\frac38,\qquad\frac18,\qquad\frac14
$$
carrying, respectively,
$$
e_1,\qquad e_2,\qquad0.
$$
These cell lengths sum to $3/4$. Kind $1$ has total allocation $3/8$, and kind $2$ has total allocation
$$
\frac14+\frac18=\frac38.
$$
The type-level means are
$$
\bar z_{t^0}=(0,1),
\qquad
\bar z_{t^1}=\left(\frac12,\frac16\right).
$$
The two nontrivial EF inequalities are
$$
1\geq\frac12+\frac16=\frac23
$$
and
$$
2\cdot\frac12+\frac16=\frac76\geq1.
$$
EFX holds because all bundles are empty or singletons.
Prices $(2,1)$ and weights $\beta_{t^0}=\beta_{t^1}=1$ satisfy the supporting inequalities, with equality on all positive allocation incidences. Hence the realization is fPO.
This example identifies the limitation precisely: insisting on the Fisher equilibrium’s equal per-person expenditure can prevent a singleton implementation even when the required deterministic EF, EFX, and fPO realization exists.
The graph characterization removes linear programming from fPO verification and gives explicit rational supporting certificates. The small-supply theorem resolves a regime with unrestricted numbers of kinds and supported types.
Neither result supplies a general method for finding compatible EFX bundle patterns and lottery probabilities when $R>a/b$. No hardness reduction is established here.
⟨structured verdict parsed — rendered above⟩
The output establishes sound partial results, but it does not resolve the general construction problem. The aggregation lemma, graph characterization, small-supply construction, and example withstand verification. I found one minor indexing omission concerning zero-supply kinds, and no false central mathematical step.
The task asks for a polynomial-time construction for arbitrary supplies, including polynomial output size and expected sampling time, or an NP-hardness result.
The prover explicitly disclaims resolving that question. Its algorithm covers the regime
$$
\sum_g\rho_g\leq a/b
$$
and additional instances passing a sufficient feasibility test. Neither supplies a general algorithm or a hardness reduction.
Severity: major relative to completing the assigned task. This is an acknowledged limitation, not an overclaim about the partial results.
Verified.
The forward direction correctly integrates a continuum improvement. Feasibility and nonnegativity imply that every coordinate is integrable. Utilities are consequently integrable as well.
A nonnegative integrable utility difference that is positive on a set of positive measure has strictly positive integral. Since the support is finite, strict aggregate improvement occurs for at least one type.
The converse handles both relevant cases correctly:
The divisions use positive denominators: $U_t>0$ in the first case and $\mu_t>0$ in the second. Null-set exceptions are consistent with the task’s definition.
Verified.
A negative closed walk contains a negative cycle with distinct vertices. Self-loops cannot be negative because their weights are zero.
The recurrence for the transfers exactly balances utility at each cycle vertex other than $t_1$. Rechecking the remaining utility ratio gives
$$
\frac{t_1(g_k)q_k}{t_1(g_1)q_1}
=
\prod_{j=1}^k
\frac{t_{j+1}(g_j)}{t_j(g_j)}
=
c^{-\sum_{j=1}^k d(t_j,t_{j+1};g_j)}>1.
$$
The sign is correct.
Every transfer is a positive finite multiple of $q_1$, and every donating incidence has positive aggregate allocation. The asserted sufficiently small choice therefore exists.
Repeated good labels do not invalidate feasibility: distinct cycle vertices ensure that each type has only one outgoing transfer, and incoming transfers cannot decrease an allocation coordinate. Supplies are preserved. Lemma 1 applies.
Verified.
The added source makes every vertex reachable. Removing nonnegative cycles permits a shortest path with at most $\tau-1$ edges between type vertices. Thus
$$
-(\tau-1)\leq\ell_t\leq0.
$$
The distances are integers, and the shifted exponents satisfy the claimed range.
The shortest-path inequality has the correct orientation:
$$
h_s-h_t\leq\varepsilon_{tg}-\varepsilon_{sg}.
$$
It yields
$$
\beta_s s_g\leq\beta_t t_g
$$
for every edge arising from $A_{tg}>0$. Taking the maximum over $s$ therefore gives equality on every allocated incidence.
The weighted-utility bound correctly excludes every continuum Pareto improvement. Positivity of all $\beta_t$ is essential and is explicitly satisfied.
The argument also covers $\tau=1$ and supplies identically zero.
Verified.
The graph has at most $m\tau^2$ edges. For a rational interval encoding, positivity of an aggregate incidence is determined by the stated positive-length-cell test.
The price-level claim follows from
$$
\beta_s s_g=a c^{h_s+\varepsilon_{sg}},
\qquad
0\leq h_s+\varepsilon_{sg}\leq\tau.
$$
Raising a binary rational to an exponent bounded by $\tau$ has polynomial binary length. The claimed supporting certificates therefore have polynomial size.
This establishes efficient verification of fPO, not efficient construction satisfying all three conditions.
Verified.
The cited source provides an exact polynomial-time algorithm for the integral-data, unit-supply linear Fisher model. Its equilibrium conditions include full spending, market clearing, and allocation only on maximum bang-per-buck incidences. Its rational-solution analysis supports the required encoding bound. [Orlin’s paper, Sections 1.1, 2, and 4](https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol10171/DagSemProc.10171.2/DagSemProc.10171.2.pdf).
The prover’s reduction matches that model:
No theorem-hypothesis failure was found.
Verified.
Full spending gives $p\cdot x_t=1$. Maximum-ratio allocation gives $t\cdot x_t=\alpha_t$, and the coordinatewise upper bound gives
$$
t\cdot x_s\leq\alpha_t p\cdot x_s=\alpha_t.
$$
These are precisely the required type-level EF inequalities.
Verified.
A positive-supply maximum-price kind must be allocated to some buyer. Its maximum-ratio condition against a minimum-price kind implies
$$
p_{\max}/p_{\min}\leq b/a=c.
$$
Total spending then yields
$$
1\leq c p_{\min}R.
$$
Consequently,
$$
\sum_gx_{tg}\leq1/p_{\min}\leq cR\leq1.
$$
The direction of every inequality and the boundary case $R=a/b$ are correct.
Verified, with a minor indexing omission.
The capacity bound permits the stated singleton cells and remaining empty cell. They reproduce $A$, preserve supplies, and retain the EF means.
Removing the only item from a singleton leaves zero utility. Thus EFX holds, including comparisons involving empty bundles.
The supporting-weight argument proves fPO on the retained kinds. However, prices were defined only for $g\in G_+$, whereas the displayed supporting inequality and reference to Section 2.2 do not explicitly restrict their indices.
Severity: minor. Zero-supply kinds cannot have positive allocation under any feasible nonnegative assignment, so this omission does not undermine the conclusion.
Minimum clarification: State explicitly that the supporting inequalities and weighted sums in this application range over $G_+$, and explain the omission of zero-supply kinds.
The zero-supply case is separately handled correctly. Rational endpoints, polynomially many cells, and singleton bundles give the claimed polynomial output size. A deterministic lottery requires no additional sampling argument.
Verified, subject to the same retained-kind indexing clarification.
The constraints form a rational linear feasibility problem with polynomially many variables, constraints, and polynomial-length coefficients. Standard exact rational linear-programming algorithms apply.
Spending and maximum-ratio restrictions reproduce the EF calculation. Capacity constraints permit singleton implementation; EFX and fPO then follow from the arguments already verified.
The output correctly states that infeasibility of this auxiliary system says nothing decisive about feasibility or complexity of the original problem.
Verified.
The price cases exhaust all positive equilibrium price ratios:
Hence $p_1=2p_2$. Total expenditure gives
$$
p_2=\frac89,\qquad p_1=\frac{16}{9}.
$$
The forced allocation
$$
A_{t^0,2}=\frac9{32}>\frac14
$$
indeed violates singleton capacity for every Fisher equilibrium.
The alternative realization’s cell lengths and supplies are correct. Its means are
$$
(0,1),\qquad \left(\frac12,\frac16\right),
$$
and both displayed EF comparisons are correct.
All bundles are empty or singleton. The proposed prices $(2,1)$ and unit weights satisfy the supporting inequalities, with equality at every allocated incidence. Thus fPO also holds.
The example establishes the claimed limitation of the Fisher implementation. It establishes no hardness result.
The mathematical partial results stand with the minor indexing clarification above. No counterexample or false central step was found.
To complete the assigned task, the prover must supply either a construction covering arbitrary supplies with the required output and sampling bounds, or a valid hardness reduction. That requires further mathematics; it is not an expositional repair.
⟨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.