Answer: Polynomial-time solvable in $m,\tau,L$; every valid instance is feasible.
Corollary 1 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateAn allocation that is EF1 w.r.t. the subjective utilities and SD-EF1 w.r.t. the market valuation always ex- ists, and can be computed in polynomial time.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given rational masses \(\mu\) over complete additive subjective valuation types on finitely many recurring good classes \(G\), a common additive market valuation \(v\), and per-capita copy supplies \(b_g\), find a finite-support distribution \(\lambda_{t,B}\) over integral bundles \(B\) satisfying type-mass and supply constraints, such that every occupied source-target pair satisfies subjective EF1 and market SD-EF1.
A society is given by its support: the list of the \(\tau\) types with positive masses \(\mu_t\), each a binary rational, with \(\sum_t\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types.
Let \(G\) contain \(m\geq1\) recurring good classes, with nonnegative rational subjective values \(u_t(g)\), common nonnegative rational market values \(v(g)\), and positive rational per-capita supplies \(b_g\). All input numbers are binary encoded; \(L\) is the total input bit length.
A bundle is \(B\in\mathbb Z_{\geq0}^{G}\), allowing repeated copies, with additive utility \(u_t(B)\). Seek finitely supported nonnegative rational masses \(\lambda_{t,B}\) satisfying \(\sum_B\lambda_{t,B}=\mu_t\) and \(\sum_{t,B}\lambda_{t,B}B_g=b_g\) for every \(g\in G\).
For every ordered pair \((t,B),(s,C)\) with positive allocation mass, including pairs of the same type, require subjective EF1 under \(u_t\), where removing a good means removing one copy from \(C\).
Also require market SD-EF1: either \(C=0\), or there is a class \(h\) with \(C_h>0\) such that \(\sum_{g:v(g)\geq a}B_g\geq\sum_{g:v(g)\geq a}(C_g-\mathbf1_{g=h})\) for every \(a\in\{v(g):g\in G\}\). Ties use weak thresholds, including zero; the subjective and market removal witnesses may differ.
Is finding such an allocation, or reporting infeasibility, polynomial-time solvable in \(m,\tau,L\), or is it NP-hard?
For finitely many agents and individually listed indivisible goods, an allocation satisfying subjective EF1 and market SD-EF1 always exists and is computable in polynomial time. [Barman, Ebadian, Latifian, and Shah](https://www.cs.toronto.edu/~nisarg/papers/market-values.pdf)
No result settling this exact distribution-over-types problem was identified in the search.
The problem is polynomial-time solvable in $m,\tau,L$. Every valid instance is feasible, and an allocation with at most $\tau+2m+1$ positive masses can be constructed in polynomial time.
The construction uses market-ranked blocks of total supply one. Its main ingredient is a transportation linear program that removes all directed envy cycles while preserving subjective EF1. Support reduction keeps the number of allocated type-bundle pairs polynomial throughout.
The market-block idea is also used in the finite-agent reduction underlying Corollary 1 of [Barman, Ebadian, Latifian, and Shah](https://www.cs.toronto.edu/~nisarg/papers/market-values.pdf). The proof below establishes the required construction directly for rational population masses, without expanding the population into individual agents.
For any nonnegative additive valuation $u$, define
$$
M_u(C)=
\begin{cases}
\max_{g:C_g>0}u(g),&C\ne0,\\
0,&C=0.
\end{cases}
$$
Subjective EF1 from $B$ to $C$ is equivalent to
$$
u(B)\ge u(C)-M_u(C).
$$
For nonempty $C$, removing a copy of maximum value minimizes the remaining utility. For empty $C$, the displayed inequality holds automatically because utilities are nonnegative.
For a market threshold $a$, write
$$
P_a(B)=\sum_{g:v(g)\ge a}B_g.
$$
Lemma 1. Market SD-EF1 from $B$ to $C$ is equivalent to
$$
P_a(B)\ge P_a(C)-1
\qquad\text{for every }a\in\{v(g):g\in G\}.
$$
Proof. Removing one copy reduces any threshold count by at most one, proving necessity.
For sufficiency, if $C=0$, the required exception applies. Otherwise choose a class $h$ of maximum market value present in $C$. At thresholds above $v(h)$, the envied bundle has count zero. At every other threshold, removing one copy of $h$ reduces its count by exactly one. Thus this single copy witnesses every required inequality. Ties and zero market values cause no exception. $\square$
In particular, market SD-EF1 in both directions follows whenever every supported pair satisfies
$$
|P_a(B)-P_a(C)|\le1
$$
at every market threshold.
Set
$$
q_g=\lfloor b_g\rfloor,
\qquad
r_g=b_g-q_g.
$$
Thus $q$ is an integer bundle and $0\le r_g<1$.
It suffices to construct an allocation for supplies $r_g$ and then add $q$ to every allocated bundle. Indeed, total population mass is one, so this addition gives exactly the original supplies. Market prefix differences are unchanged. For subjective EF1, note that
$$
M_{u_t}(q+C)\ge M_{u_t}(C).
$$
Consequently,
$$
\begin{aligned}
u_t(q+B)-u_t(q+C)+M_{u_t}(q+C)
&=u_t(B)-u_t(C)+M_{u_t}(q+C)\\
&\ge u_t(B)-u_t(C)+M_{u_t}(C)\\
&\ge0.
\end{aligned}
$$
This includes empty $C$.
Let
$$
R=\sum_g r_g<m.
$$
If $R=0$, assign $q$ to every type, with mass $\mu_t$, and finish.
Otherwise set
$$
k=\lceil R\rceil\le m.
$$
Add a dummy class of supply $k-R$ if this quantity is positive. Its subjective utilities are all zero.
Order the real classes by nonincreasing market value, breaking ties arbitrarily, and place the dummy last. Lay out consecutive intervals of the corresponding residual supply lengths on $[0,k)$.
Split each class interval at integer boundaries. Call each positive-length piece a token class $h$. It has:
Write $H$ for the token classes and $p=|H|$. Each real-class interval has length less than one, so it produces at most two token classes. The dummy interval, when present, ends at the integer $k$ and produces only one. Hence
$$
p\le2m+1.
$$
For every block $j$,
$$
\sum_{h:j(h)=j}a_h=1.
$$
Define token utilities by
$$
\widetilde u_t(h)=
\begin{cases}
u_t(g(h)),&h\text{ has a real label},\\
0,&h\text{ is dummy}.
\end{cases}
$$
A token bundle is an integer vector $Z\in\mathbb Z_{\ge0}^{H}$. Mapping it to a real bundle means merging equal real labels and deleting dummy labels. Repeated real copies are therefore allowed.
The algorithm will allocate blocks successively. After processing block $j$, every supported token bundle will contain exactly one token from each block $1,\ldots,j$, and no tokens from later blocks.
We first prove a general operation on a finitely supported allocation.
Suppose its positive type-bundle pairs are indexed by $i=1,\ldots,N$:
$$
(t_i,Z_i,w_i),
\qquad w_i>0.
$$
Assume this allocation satisfies subjective EF1 for every ordered pair.
Let $C_1,\ldots,C_K$ be its distinct supported bundles, and let their aggregate masses be
$$
W_\ell=\sum_{i:Z_i=C_\ell}w_i.
$$
Introduce a variable $x_{i\ell}$ only when
$$
\widetilde u_{t_i}(C_\ell)\ge\widetilde u_{t_i}(Z_i).
$$
Solve
$$
\begin{aligned}
\text{maximize}\quad&
\sum_{i,\ell}x_{i\ell}\widetilde u_{t_i}(C_\ell),\\
\text{subject to}\quad&
\sum_\ell x_{i\ell}=w_i
&&\text{for every }i,\\
&
\sum_i x_{i\ell}=W_\ell
&&\text{for every }\ell,\\
&
x_{i\ell}\ge0.
\end{aligned}
$$
The original assignment is feasible. The polytope is bounded, since every variable is at most one, so an optimum exists.
Interpret a positive $x_{i\ell}$ as assigning mass $x_{i\ell}$ of type $t_i$ bundle $C_\ell$. Aggregate identical resulting type-bundle pairs.
Lemma 2. This operation preserves type masses, token supplies, and subjective EF1. At an optimum, the directed envy graph on the resulting positive type-bundle pairs is acyclic.
Here the graph has an edge
$$
(t,B)\longrightarrow(s,C)
\quad\text{exactly when}\quad
\widetilde u_t(C)>\widetilde u_t(B).
$$
Proof. The row equations preserve each original cohort’s mass and hence every type mass. The column equations preserve the aggregate mass of every bundle, and therefore preserve all token supplies.
For subjective EF1, take a positive $x_{i\ell}$. The assigned bundle satisfies
$$
\widetilde u_{t_i}(C_\ell)\ge\widetilde u_{t_i}(Z_i).
$$
Every resulting supported bundle $D$ was supported originally. Original EF1 therefore gives
$$
\widetilde u_{t_i}(Z_i)
\ge
\widetilde u_{t_i}(D)-M_{\widetilde u_{t_i}}(D).
$$
Combining these inequalities proves every required resulting comparison.
For acyclicity, suppose an optimum has a directed cycle
$$
(t_1,B_1)\longrightarrow\cdots
\longrightarrow(t_\ell,B_\ell)
\longrightarrow(t_1,B_1).
$$
Use indices modulo $\ell$. For each cycle vertex, select a positive transportation cell supplying that type-bundle pair; call its row $i_r$. Thus
$$
t_{i_r}=t_r,
\qquad
\widetilde u_{t_r}(B_r)\ge
\widetilde u_{t_r}(Z_{i_r}).
$$
The cycle inequalities imply
$$
\widetilde u_{t_r}(B_{r+1})
>
\widetilde u_{t_r}(B_r)
\ge
\widetilde u_{t_r}(Z_{i_r}).
$$
Hence assigning bundle $B_{r+1}$ to row $i_r$ is an allowed transportation cell.
Choose a positive $\varepsilon$ no larger than the selected cells’ masses. For every $r$, move mass $\varepsilon$ in row $i_r$ from $B_r$ to $B_{r+1}$. The selected cells are distinct because the cycle vertices are distinct.
Every row total is preserved. Every bundle-column total is preserved because the receiving and relinquished bundles form the same cyclic list. The objective increases by
$$
\varepsilon\sum_{r=1}^{\ell}
\left(
\widetilde u_{t_r}(B_{r+1})
-
\widetilde u_{t_r}(B_r)
\right)>0,
$$
contradicting optimality. Thus the graph is acyclic. $\square$
This lemma applies to comparisons within a type as well as across types.
For a fixed stage, suppose the required token supplies are $c_h$. They equal $a_h$ for processed blocks and zero for unprocessed blocks.
Given a feasible allocation, retain its available type-bundle pairs and solve
$$
\sum_{Z}\lambda_{t,Z}=\mu_t,
\qquad
\sum_{t,Z}\lambda_{t,Z}Z_h=c_h,
\qquad
\lambda_{t,Z}\ge0
$$
for a basic feasible solution.
This linear program is feasible because the current allocation is a feasible point. It is bounded because the masses sum to one.
Associate to a variable its column
$$
A_{t,Z}=(e_t,Z)\in\mathbb Z^{\tau+p}.
$$
A basic feasible solution has at most
$$
d:=\tau+p
$$
positive variables. To see the relevant support bound directly, if the active columns were dependent, there would be a nonzero vector $z$ supported on those columns with
$$
\sum_i z_iA_i=0.
$$
The type rows imply $\sum_i z_i=0$, so $z$ has both positive and negative entries. Sufficiently small perturbations in both directions along $z$ preserve feasibility, contradicting extremality.
The resulting support is a subset of the available support. Therefore:
In particular, the one-token-per-processed-block property is preserved. We use this support reduction repeatedly.
Suppose blocks $1,\ldots,j-1$ have been allocated. Assume the current allocation:
Take a topological order of the envy graph: every directed edge goes from an earlier vertex to a later one.
Serve the cohorts in that order. While serving cohort $i$, choose, among token classes of block $j$ with positive remaining supply, a token $h$ maximizing $\widetilde u_{t_i}(h)$. If the cohort has remaining mass $w$ and that token has remaining supply $a$, assign bundle
$$
Z_i+e_h
$$
to mass
$$
\alpha=\min\{w,a\}.
$$
Subtract $\alpha$ from both remaining quantities and continue.
The block supply and total cohort mass both equal one. Every step reduces both totals by the same amount. Thus available supply remains whenever unserved mass remains. Every step exhausts a cohort or a token class, so there are at most $N+p_j$ steps, where $p_j$ is the number of token classes in block $j$.
The operation preserves type masses, uses exactly the block’s supplies, and gives each resulting bundle exactly one new token.
Lemma 3. This greedy block allocation preserves subjective EF1.
Proof. Consider an ordered pair of resulting positive assignments
$$
(t_i,Z_i+e_h),
\qquad
(t_\ell,Z_\ell+e_f).
$$
All utility comparisons below use the first recipient’s valuation $\widetilde u_{t_i}$.
There are three cases.
Case 1: $i$ precedes $\ell$ in the topological order.
Token $f$ was available when token $h$ was chosen: its supply is positive at the later assignment and only decreases over time. Greedy choice therefore gives
$$
\widetilde u_{t_i}(h)\ge\widetilde u_{t_i}(f).
$$
If $Z_\ell\ne0$, old EF1 supplies a token copy $z$ in $Z_\ell$ such that
$$
\widetilde u_{t_i}(Z_i)
\ge
\widetilde u_{t_i}(Z_\ell-e_z).
$$
Consequently,
$$
\begin{aligned}
\widetilde u_{t_i}(Z_i+e_h)
&\ge
\widetilde u_{t_i}(Z_\ell-e_z)
+\widetilde u_{t_i}(f)\\
&=
\widetilde u_{t_i}(Z_\ell+e_f-e_z).
\end{aligned}
$$
The old witness remains present in the augmented envied bundle.
If $Z_\ell=0$, remove its new token $f$. Its remaining bundle is empty, and nonnegative utility suffices.
Case 2: $\ell$ precedes $i$.
There cannot be an envy edge from vertex $i$ to vertex $\ell$, because that would contradict the topological order. Thus
$$
\widetilde u_{t_i}(Z_i)\ge\widetilde u_{t_i}(Z_\ell).
$$
Removing the envied bundle’s new token $f$ yields
$$
\widetilde u_{t_i}(Z_i+e_h)
\ge
\widetilde u_{t_i}(Z_i)
\ge
\widetilde u_{t_i}(Z_\ell).
$$
Case 3: $i=\ell$.
The two recipients originated from the same type-bundle cohort. Again remove the envied bundle’s new token:
$$
\widetilde u_{t_i}(Z_i+e_h)
\ge
\widetilde u_{t_i}(Z_i)
=
\widetilde u_{t_i}(Z_\ell).
$$
These cases cover every ordered pair, including pairs of the same type and pairs created by splitting one cohort. $\square$
Initialize each type with the empty token bundle and mass $\mu_t$.
For each block $j=1,\ldots,k$:
Induction using Lemmas 2 and 3 proves that every stage satisfies subjective EF1 and all mass and processed-supply equations. At the end, every supported token bundle contains exactly one token from every block.
We now prove market fairness after merging real labels and deleting dummy labels.
Fix an original market threshold $a$. In the interval layout, the real classes satisfying $v(g)\ge a$ occupy precisely a prefix
$$
[0,\gamma_a),
\qquad
\gamma_a=\sum_{g:v(g)\ge a}r_g.
$$
This holds for ties because the entire tied group belongs to the threshold prefix. It also holds at threshold zero: the prefix contains all real classes and ends before the dummy.
A supported token bundle chooses exactly one token from each unit block. Every block entirely before $\gamma_a$ contributes one threshold copy. Every block entirely after $\gamma_a$ contributes zero. If $\gamma_a$ lies strictly inside a block, that block contributes either zero or one.
Hence every resulting real residual bundle $B$ satisfies
$$
P_a(B)\in
\{\lfloor\gamma_a\rfloor,\lceil\gamma_a\rceil\}.
$$
Any two such bundles therefore have threshold counts differing by at most one. Lemma 1 proves market SD-EF1 for every ordered pair.
Subjective EF1 also survives the mapping to real bundles. Utilities are unchanged by merging labels and deleting dummy tokens. Moreover, since dummy utilities are zero and real utilities are nonnegative,
$$
M_{\widetilde u_t}(Z)=M_{u_t}(B)
$$
for a token bundle $Z$ and its real image $B$, including when $B$ is empty. Thus the subjective EF1 characterization from Section 1 is unchanged.
The mapped allocation has residual supplies $r_g$. Finally add $q$ to every bundle as justified in Section 2. This produces the required original allocation.
It remains to verify that the construction is polynomial in the binary input size, rather than merely in the number of mathematical operations.
We use the standard rational linear-programming theorem: feasibility and linear optimization over an explicitly encoded rational polytope can be performed in polynomial time, and an optimal basic feasible solution can be obtained when the polytope is nonempty and bounded. All linear programs above satisfy these hypotheses.
There are
$$
k\le m,
\qquad
p\le2m+1,
\qquad
d=\tau+p
$$
blocks, token classes, and support-bound rows, respectively.
Before each transportation optimization, support reduction has left at most $d$ pairs. There are therefore at most $d$ distinct bundles, at most $d^2$ transportation variables, and at most $2d$ equality constraints.
A basic transportation solution has at most $2d$ positive cells. After aggregation, the next support-reduction problem thus has at most $2d$ variables.
The greedy block operation starts with at most $d$ cohorts and creates at most $d+p_j$ positive assignments. Its subsequent support-reduction problem also has polynomial size.
Topological sorting and choosing highest-utility available tokens require polynomially many exact rational comparisons. There are at most $m$ iterations.
Choose an integer $D$ clearing the denominators of the input type masses and supplies. Taking the product of their input denominators gives
$$
\log D=O(L).
$$
Every residual supply, dummy supply, and token-piece length has denominator dividing $D$: these numbers are obtained from input supplies by sums, subtraction, and integer boundaries.
In a support-reduction problem, the right-hand side consists of type masses, processed token supplies, and zeros. Its coordinates lie in $[0,1]$ and have denominators dividing $D$.
Every supported token bundle has exactly one token per processed block. Since each token class belongs to a single block, every token coordinate is zero or one. The support-reduction matrix therefore has entries in $\{0,1\}$.
If a basic solution has $s\le d$ positive variables, their independent columns admit a nonsingular $s$-row restriction $M$. Cramer’s rule gives
$$
\lambda_i=
\frac{\det M_i(Dy)}{D\det M},
$$
where $y$ is the restricted right-hand side. Determinant expansion yields
$$
1\le|\det M|\le s!,
\qquad
|\det M_i(Dy)|\le D\,s!.
$$
Thus every compressed mass has bit length
$$
O\!\left(L+d\log(d+1)\right).
$$
Crucially, this bound depends on the fixed input right-hand sides, not on the number of preceding iterations.
Transportation right-hand sides are compressed masses and sums of at most $d$ such masses. Their bit lengths are polynomial. Objective coefficients are utilities of bundles of size at most $m$, so their bit lengths are polynomial as well. Exact transportation solutions consequently have polynomial encoding length.
The greedy operation uses only comparisons and subtraction of rational masses and token supplies. Within one block, all resulting denominators divide the product of the denominators present at the start of that operation. There are polynomially many such numbers, each of polynomial bit length, so intermediate rational bit lengths remain polynomial. The following support reduction restores the uniform bound above.
Finally, adding $q$ produces bundle coordinates of polynomial bit length. The final allocation has at most
$$
d\le\tau+2m+1
$$
positive masses; merging identical mapped type-bundle pairs can only decrease this number.
Therefore the entire construction, including its output, has polynomial bit complexity in $m,\tau,L$.
Every valid instance admits the requested allocation, and the algorithm above constructs one in polynomial time. Thus reporting infeasibility is unnecessary on inputs satisfying the stated hypotheses.
⟨structured verdict parsed — rendered above⟩
The prover’s claim is proved. The construction addresses the exact distribution-over-types problem, including binary-encoded supplies, repeated copies, comparisons within a type, weak market thresholds, and zero valuations. I found no major or minor issues requiring repair.
For a nonempty bundle $C$, removing a copy with maximum subjective value minimizes the remaining additive utility. Thus
$$
u(B)\ge u(C)-M_u(C)
$$
is exactly subjective EF1. The convention $M_u(0)=0$ correctly handles empty envied bundles because utilities are nonnegative.
Lemma 1 also correctly establishes market SD-EF1. Necessity follows because removing one copy decreases each threshold count by at most one. For sufficiency, a maximum-market-value copy in $C$ supplies a single witness for all thresholds: above its value, $C$ has no qualifying copies; at or below its value, removing it decreases the count by exactly one.
This argument respects weak thresholds, ties, zero market values, and repeated copies. Consequently, pairwise threshold-count differences of at most one suffice for all ordered comparisons.
The decomposition
$$
b_g=q_g+r_g,\qquad q_g=\lfloor b_g\rfloor,\qquad 0\le r_g<1
$$
is correct. Adding $q$ to every allocated bundle contributes exactly $q_g$ to aggregate supply because total population mass is one.
Market prefix differences remain unchanged. The displayed subjective calculation is correct: common additive utility cancels, while
$$
M_{u_t}(q+C)\ge M_{u_t}(C).
$$
When $C$ is empty, this inequality follows from nonnegativity and the stated empty-bundle convention. Therefore residual subjective EF1 implies subjective EF1 after adding $q$.
The case $R=0$ is completely handled: identical bundles $q$ satisfy both fairness requirements and all supply equations.
Since each residual supply is strictly less than one,
$$
R=\sum_g r_g<m.
$$
For $R>0$, this gives
$$
1\le k=\lceil R\rceil\le m.
$$
Padding by the dummy supply makes the total interval length exactly $k$.
Each real interval has length less than one and therefore intersects at most two unit blocks in positive length. If the dummy interval is present, its length is less than one and it ends at $k$, so it lies entirely in the last block. Hence
$$
p\le 2m+1.
$$
Zero residual supplies produce no token classes, consistent with the definition requiring positive-length pieces. Splitting at integer boundaries ensures every token belongs to exactly one block, and every block has total token supply one.
The contextual attribution to market-ranked blocks is consistent with the reduction preceding Corollary 1 in the [cited paper](https://www.cs.toronto.edu/~nisarg/papers/market-values.pdf). The distributional construction is proved independently in the submitted argument; it does not rely on expanding rational masses into individually listed agents.
The original assignment is feasible because each original bundle is an allowed destination for its own row. Row equations preserve original cohort masses and therefore type masses. Column equations preserve aggregate bundle masses and therefore every token supply.
Every variable is bounded by its row mass, which is at most one. Thus the feasible polytope is nonempty and bounded.
The EF1 preservation argument is valid for every ordered resulting pair. A recipient receives a bundle worth at least its original bundle under its own valuation, while every resulting envied bundle belonged to the original support. The original EF1 inequality therefore applies to that envied bundle and combines with the recipient’s utility improvement.
Aggregation of identical type-bundle pairs does not introduce any new comparison requiring a different argument.
For every selected cycle vertex, the proof selects a positive transportation cell supplying that vertex. The strict envy inequality makes the successor bundle an allowed destination for the selected row.
Distinct cycle vertices give distinct selected cells. Thus choosing $\varepsilon$ no larger than every selected cell’s mass ensures that all decremented cells remain nonnegative.
Cycle vertices may share a type, a bundle column, or even an original transportation row. None of these possibilities invalidates the exchange:
The stated objective change is exactly the sum of the strictly positive envy improvements, multiplied by $\varepsilon$. It contradicts optimality. Therefore the resulting envy graph is acyclic, including edges between different bundles assigned to the same type.
The support-reduction LP uses only currently available type-bundle pairs and has the current allocation as a feasible point. Type equations imply total mass one, establishing boundedness.
The active-column argument correctly proves that an extreme point has at most
$$
d=\tau+p
$$
positive variables. A dependence among active columns gives a nonzero perturbation preserving all equations. The type rows force its coefficients to sum to zero, so the perturbation has both signs and permits sufficiently small feasible changes in both directions.
Since support reduction only removes pairs, it preserves subjective EF1 and any existing acyclicity. It also preserves the one-token-per-processed-block property. The equality constraints preserve type masses and processed supplies.
Supply and cohort mass both total one. Each assignment subtracts the same mass from these two totals, and each step exhausts a cohort or a token class. The claimed bound of at most $N+p_j$ steps is valid.
All three cases in Lemma 3 are correct:
The empty old envied bundle is expressly handled. These cases cover every ordered pair, including different assignments of the same type and assignments created by splitting one cohort.
Initialization with empty bundles satisfies subjective EF1 and all initial mass equations.
Before each greedy block operation, transportation optimization establishes acyclicity, and support reduction preserves it. Greedy allocation then preserves subjective EF1 and allocates precisely the current block supply. The subsequent support reduction preserves those properties.
The proof does not incorrectly assume that greedy allocation preserves acyclicity: the next iteration establishes it again before it is needed.
Transportation only redistributes existing bundles, while greedy allocation adds exactly one token from the new block. Therefore the final token bundles have exactly one token from every block.
At each original market threshold $a$, the qualifying real intervals form the prefix
$$
[0,\gamma_a),\qquad
\gamma_a=\sum_{g:v(g)\ge a}r_g.
$$
Arbitrary ordering within tied market values causes no problem because a weak threshold includes the entire tied group. The dummy is last, so the zero threshold also has the stated prefix structure.
Each complete block before the prefix endpoint contributes one qualifying copy; each block after it contributes none. Only a block containing the endpoint can vary. Thus
$$
P_a(B)\in\{\lfloor\gamma_a\rfloor,\lceil\gamma_a\rceil\}.
$$
This includes integer endpoints, where the two values coincide. Lemma 1 consequently supplies market SD-EF1 for every ordered pair.
Merging real labels preserves additive utilities and supply totals. Deleting dummy tokens preserves utilities because their values are zero. Nonnegativity ensures that deleting those tokens also preserves the maximum-copy value, including when the real image is empty. Therefore subjective EF1 survives the mapping.
Adding $q$ then gives the original supplies and preserves both fairness conditions as already established.
The stated rational LP theorem supplies exact optimization and a basic optimal solution for explicitly encoded nonempty bounded rational polytopes. Both LP families meet these hypotheses.
Before transportation, support has size at most $d$, giving at most $d^2$ variables and $2d$ equality constraints. A basic transportation solution has at most $2d$ positive cells. Greedy allocation creates at most $d+p_j$ assignments. There are at most $m$ iterations, so all LP dimensions and discrete operations are polynomially bounded.
The denominator argument correctly prevents uncontrolled growth across iterations. A common input denominator $D$ satisfies
$$
\log D=O(L).
$$
Residual supplies, dummy supply, and token lengths retain denominators dividing $D$.
The support-reduction matrix has entries in $\{0,1\}$ because every supported bundle contains at most one token of each token class. Its right-hand side has coordinates in $[0,1]$ with denominators dividing $D$. For an independent positive support of size $s\le d$, the stated Cramer bounds
$$
1\le|\det M|\le s!,
\qquad
|\det M_i(Dy)|\le D\,s!
$$
are correct. They yield compressed mass bit lengths
$$
O\!\left(L+d\log(d+1)\right).
$$
Transportation inputs therefore have polynomial encoding length, and exact basic solutions do as well. Within a greedy operation, subtraction introduces no denominator factors outside the product of the starting denominators. That product has polynomial bit length. The following support reduction restores the uniform bound.
Finally, the integer parts $q_g$ have polynomial bit length even when numerically large. Adding them does not expand repeated copies individually. The final support bound
$$
\tau+2m+1
$$
is valid, and aggregating identical mapped pairs can only reduce it.
No additional lemma, clarification, or repair is needed to make the submitted argument verifiable.
⟨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.