← back to the atlas

A Polynomial-Time Algorithm for Fair and Efficient Allocation with a Fixed Number of Agents (d4-conf-wine-2025-0039)

Answer: —

The anchor (named result in the paper)

Theorem 1.1 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateWhen each agent has an additive valuation function and the number of agents is fixed, an EF1 and fPO allocation can be computed in polynomial time.

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

The continuous mirror question, as graded

Given fixed \(\tau\), rational type masses \(\mu_\theta\), additive values \(v_{\theta g}\), and rational per-capita supplies \(\sigma_g\) for indivisible good kinds, compute masses \(x_{\theta,b}\) over integral bundles \(b\in\mathbb{Z}_{\ge 0}^{m}\) satisfying \(\sum_b x_{\theta,b}=\mu_\theta\) and \(\sum_{\theta,b}b_gx_{\theta,b}\le\sigma_g\), such that every pair of supported cells satisfies \(v_\theta(b)\ge v_\theta(b')-\max(\{v_{\theta g}:b'_g>0\}\cup\{0\})\), and no feasible fractional reassignment weakly improves every positive-mass cell while strictly improving one.

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

A society is given by its support: the list of the \(\tau\) types with positive mass, each mass \(\mu_\theta\) a binary rational, with \(\sum_\theta\mu_\theta=1\). Here \(\tau\) is the support size, not the number of possible types, and is fixed.
There are \(m\ge1\) good kinds with positive binary-rational per-capita supplies \(\sigma_g\). Values \(v_{\theta g}\) are nonnegative binary rationals; every type values some kind positively, and every kind is valued positively by some type. Let \(L\) be the total input bit length.
An allocation is a finite list of positive binary-rational masses \(x_{\theta,b}\), with integral bundles \(b\in\mathbb Z_{\ge0}^{m}\) encoded in binary, satisfying \(\sum_bx_{\theta,b}=\mu_\theta\) and \(\sum_{\theta,b}b_gx_{\theta,b}\le\sigma_g\). Write \(v_\theta(z)=\sum_gv_{\theta g}z_g\).
Require EF1 between every ordered pair of supported cells: \(v_\theta(b)\ge v_\theta(b')-\max(\{v_{\theta g}:b'_g>0\}\cup\{0\})\) whenever \(x_{\theta,b}>0\) and \(x_{\theta',b'}>0\).
Require fractional Pareto optimality: there are no vectors \(y_{\theta,b}\in\mathbb R_{\ge0}^{m}\) for the supported cells satisfying \(\sum_{\theta,b}x_{\theta,b}y_{\theta,b,g}\le\sigma_g\), with \(v_\theta(y_{\theta,b})\ge v_\theta(b)\) for every cell and strict inequality for at least one. Reassignments need not satisfy EF1.

For each fixed \(\tau\), can such an allocation be computed in polynomial time in \(m\) and \(L\), with the polynomial allowed to depend on \(\tau\), or is this search problem NP-hard for some fixed \(\tau\)?

For finitely many agents with nonnegative additive valuations, an EF1 and fractionally Pareto-optimal allocation is computable in polynomial time when the number of agents is fixed ([Mahara](https://arxiv.org/html/2411.01810v1)).
No result settling this exact mass-society search problem was located in the literature search.

Modeling choices made when packaging the task

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

Status and proved progress

The general complexity question remains unresolved. I prove a polynomial-time algorithm for a further class with arbitrary overlapping valuation supports:

Theorem. Suppose that, for every type $\theta$, there is a positive rational $c_\theta$ such that
$$ v_{\theta g}\in\{0,c_\theta\}\qquad\text{for every kind }g. $$
Then an EF1 and fractionally Pareto-optimal allocation can be computed in polynomial time in the input length, even when $\tau$ is not fixed. The output has at most $\tau(m+1)$ supported cells.

Thus this result allows different types to like different, overlapping sets of kinds. It does not require proportional valuation vectors or disjoint positive supports.

The proof is self-contained. In particular, the rounding construction used below is established explicitly rather than imported from the notes.

1. Normalization and the efficiency certificate

Define the liked set of type $\theta$ by
$$ G_\theta=\{g:v_{\theta g}=c_\theta\}. $$
The assumptions of the question imply that every $G_\theta$ is nonempty and every kind belongs to at least one such set.

Dividing each type’s valuations by $c_\theta$ preserves both EF1 and fractional Pareto optimality: every utility comparison concerning that type is multiplied by a positive constant. The normalized valuations are therefore
$$ \widehat v_{\theta g}= \begin{cases} 1,&g\in G_\theta,\\ 0,&g\notin G_\theta. \end{cases} $$

We will allocate every kind completely and give each supported cell only kinds liked by its type. These two properties already certify fractional Pareto optimality.

Indeed, for such an allocation,
$$ \sum_{\theta,b}\frac{x_{\theta,b}}{c_\theta}v_\theta(b) = \sum_{\theta,b}x_{\theta,b}\sum_g b_g = \sum_g\sigma_g. $$
For any feasible fractional reassignment $y$,
$$ \begin{aligned} \sum_{\theta,b}\frac{x_{\theta,b}}{c_\theta}v_\theta(y_{\theta,b}) &= \sum_{\theta,b}x_{\theta,b} \sum_{g\in G_\theta}y_{\theta,b,g}\\ &\le \sum_g\sum_{\theta,b}x_{\theta,b}y_{\theta,b,g}\\ &\le \sum_g\sigma_g. \end{aligned} $$
A weak improvement in every supported cell, with a strict improvement in at least one, would strictly increase the first weighted utility sum because all its weights $x_{\theta,b}/c_\theta$ are positive. This contradicts the bound.

It remains to construct liked-only bundles that exhaust supplies and satisfy EF1.

2. A rounding lemma controlling bundle cardinality

Lemma. Given nonnegative rational coordinates $a_1,\ldots,a_k$, one can compute a rational probability distribution on at most $k+1$ integral bundles $b\in\mathbb Z_{\ge0}^k$ such that
$$ \mathbb E[b_j]=a_j $$
for every coordinate, and every supported bundle satisfies
$$ \sum_jb_j\in \left\{ \left\lfloor\sum_ja_j\right\rfloor, \left\lceil\sum_ja_j\right\rceil \right\}. $$
A coordinate with $a_j=0$ is zero in every supported bundle. The construction has polynomial running time and output bit length.

Proof. Set
$$ A_0=0,\qquad A_j=\sum_{i=1}^ja_i. $$
For $s\in[0,1)$, define
$$ b_j(s)=\lfloor A_j+s\rfloor-\lfloor A_{j-1}+s\rfloor. $$
Because $A_j\ge A_{j-1}$, every coordinate is a nonnegative integer. If $a_j=0$, the two floors coincide.

For every nonnegative real $A$, writing $A=n+r$ with $n$ integral and $0\le r<1$ gives
$$ \int_0^1\lfloor A+s\rfloor\,ds=n(1-r)+(n+1)r=A. $$
Subtracting consecutive identities yields
$$ \int_0^1b_j(s)\,ds=a_j. $$
The coordinates telescope:
$$ \sum_{j=1}^kb_j(s)=\lfloor A_k+s\rfloor, $$
which has the asserted two possible values.

Each function $\lfloor A_j+s\rfloor$ has at most one breakpoint inside $[0,1)$. Their combined breakpoints partition the interval into at most $k+1$ positive-length, half-open intervals on which the whole bundle is constant. Use those interval lengths as probabilities, merging repeated bundles.

All breakpoints are rational. Computing cumulative sums, sorting breakpoints, and evaluating the floors uses polynomially many exact rational operations. Every resulting number has polynomial bit length. $\square$

3. Bottleneck groups and their expected item counts

We next construct an aggregate liked-only allocation whose types have suitably ordered expected item counts.

At a stage of the construction, let $T$ be the remaining types and $R$ the remaining kinds. For $B\subseteq T$, define
$$ \mu(B)=\sum_{\theta\in B}\mu_\theta, \qquad N_R(B)=R\cap\bigcup_{\theta\in B}G_\theta, \qquad f_R(B)=\sum_{g\in N_R(B)}\sigma_g. $$
For nonempty $T$, set
$$ t=\min_{\varnothing\ne B\subseteq T}\frac{f_R(B)}{\mu(B)}. $$

3.1 The maximal minimizing group

There is a unique inclusion-wise maximal subset attaining this minimum.

To prove this, first observe that $f_R$ is submodular:
$$ f_R(B\cup C)+f_R(B\cap C)\le f_R(B)+f_R(C). $$
Indeed,
$$ N_R(B\cup C)=N_R(B)\cup N_R(C), \qquad N_R(B\cap C)\subseteq N_R(B)\cap N_R(C), $$
and every supply is positive.

By the definition of $t$,
$$ f_R(E)\ge t\mu(E) $$
for every $E\subseteq T$, including the empty set. If $B$ and $C$ attain the minimum, then
$$ \begin{aligned} f_R(B\cup C)+f_R(B\cap C) &\le t\mu(B)+t\mu(C)\\ &=t\mu(B\cup C)+t\mu(B\cap C). \end{aligned} $$
The reverse inequality holds termwise. Consequently, $B\cup C$ also attains the minimum.

The union of all minimizing subsets is therefore itself minimizing. Denote it by $A$, and put
$$ H=N_R(A). $$
In particular,
$$ \sum_{g\in H}\sigma_g=t\mu(A). $$

3.2 Allocating the group’s goods

There are rational quantities $q_{\theta g}\ge0$, for $\theta\in A$ and $g\in H$, such that
$$ q_{\theta g}=0\quad\text{if }g\notin G_\theta, $$
$$ \sum_{g\in H}q_{\theta g}=\mu_\theta t, \qquad \sum_{\theta\in A}q_{\theta g}=\sigma_g. $$

Here is the flow justification. Use a network with source-to-type capacities $\mu_\theta t$, type-to-liked-kind edges of sufficiently large capacity, and kind-to-sink capacities $\sigma_g$.

For every $B\subseteq A$, the total demand of $B$ is at most the available supply in its neighborhood:
$$ t\mu(B)\le f_R(B). $$
All those neighboring kinds belong to $H$. By the max-flow/min-cut theorem, these inequalities imply that all source-to-type edges can be saturated.

For completeness, a cut containing types $B$ on its source side must also contain their neighboring kinds if it crosses no large-capacity edge. Its minimum possible capacity is
$$ t\mu(A\setminus B)+f_R(B)\ge t\mu(A). $$
Choosing each large capacity greater than the total source capacity ensures that a minimum cut never crosses such an edge. Thus the maximum flow has value $t\mu(A)$.

The total kind-to-sink capacity is also $t\mu(A)$, so every supply in $H$ is exhausted. The flows on type-to-kind edges give the required $q_{\theta g}$.

Remove $A$ and $H$ and repeat.

3.3 The levels strictly increase

Let $B$ be any nonempty subset of the next remaining type set $T\setminus A$. Its next-stage neighborhood supply satisfies
$$ f_{R\setminus H}(B)=f_R(A\cup B)-f_R(A). $$
Therefore,
$$ f_{R\setminus H}(B)\ge t\mu(B). $$
Equality would make $A\cup B$ a minimizing subset at the current stage, contradicting the maximality of $A$. Hence
$$ \frac{f_{R\setminus H}(B)}{\mu(B)}>t. $$
Every subsequent level is strictly larger.

Initially, every nonempty type subset has a nonempty neighborhood, so the first level is positive. The displayed inequality also ensures that every remaining type continues to have a nonempty neighborhood.

Every remaining kind continues to be liked by a remaining type: if all its remaining likers were in $A$, it would belong to $H$ and would have been removed. Consequently, when all types have been removed, all kinds have also been removed and allocated.

Write $t_\theta$ for the level of the group containing $\theta$. We have proved
$$ \sum_gq_{\theta g}=\mu_\theta t_\theta. $$
We have also obtained the crucial separation property:
$$ t_\theta<t_\eta,\ q_{\eta g}>0 \quad\Longrightarrow\quad g\notin G_\theta. $$
Indeed, all then-remaining kinds liked by $\theta$ were removed when its group was processed. Later groups use only kinds still remaining.

4. Computing the groups in polynomial time

Enumerating all type subsets suffices when $\tau$ is fixed. To establish the stronger theorem for variable $\tau$, we give a polynomial-time procedure.

At each stage solve the rational linear program
$$ \begin{aligned} \text{maximize}\quad &t\\ \text{subject to}\quad &q_{\theta g}\ge0,\quad t\ge0,\\ &q_{\theta g}=0\quad\text{if }g\notin G_\theta,\\ &\sum_{\theta\in T}q_{\theta g}\le\sigma_g &&\text{for }g\in R,\\ &\sum_{g\in R}q_{\theta g}\ge\mu_\theta t &&\text{for }\theta\in T. \end{aligned} $$
This program is feasible at zero and has a finite optimum: summing the last constraints bounds $t$ by the total remaining supply divided by $\mu(T)>0$.

Its optimum equals the minimum ratio in Section 3. Necessity follows by summing the demands of any subset $B$; sufficiency follows from the same flow-cut calculation as above, now with type set $T$.

It remains to recover the maximal minimizing subset $A$ without enumerating subsets.

Choose an integer $D$ clearing the denominators of all input masses and supplies. For example, their denominator product suffices and has polynomial bit length. Every nonempty-subset ratio has the form
$$ \frac{f_R(B)}{\mu(B)}=\frac{S_B}{M_B}, \qquad S_B,M_B\in\mathbb Z,\qquad 1\le M_B\le D. $$
The last bound uses $\mu(B)\le1$. Consequently, two distinct ratios differ by at least
$$ \frac1{D^2}. $$

Let $t$ be the LP optimum and define
$$ \varepsilon=\frac1{2D^2}, \qquad t'=t+\varepsilon. $$
Construct the type-to-kind flow network using source-to-type capacities $t'\mu_\theta$. Give each type-to-liked-kind edge capacity
$$ C=1+t'\mu(T)+\sum_{g\in R}\sigma_g. $$
This exceeds the capacity of the cut containing only the source, so a minimum cut crosses no such edge.

If $B$ is its source-side type set, positive supplies imply that its source-side kinds are exactly $N_R(B)$: any extra kind could be moved to the sink side and strictly decrease the cut capacity. Hence minimizing the cut is equivalent to maximizing
$$ t'\mu(B)-f_R(B). $$

For a minimizing subset of the original ratio, this expression is $\varepsilon\mu(B)>0$. For every other nonempty subset, it is negative, because its ratio is at least $t+1/D^2$. The empty subset gives zero. Among minimizing subsets, the unique maximal one $A$ has strictly greatest mass, since masses are positive and every minimizing subset is contained in $A$.

Thus this minimum cut recovers precisely $A$.

There are at most $\tau$ stages. Each uses one rational LP and a polynomial-size flow computation to identify the group, followed by a flow computation to allocate its goods. Polynomial-time rational LP and maximum-flow algorithms apply to these finite, rationally encoded problems. Their coefficients, capacities, and rational outputs have polynomial bit length; notably, $D$ is used through its binary encoding rather than by expanding a population of size $D$.

5. Rounding and proving every EF1 comparison

For each type, define its conditional expected bundle by
$$ a_{\theta g}=\frac{q_{\theta g}}{\mu_\theta}. $$
Its expected total item count is $t_\theta$. Apply the rounding lemma to obtain a distribution $(\ell_{\theta k},b^{\theta k})$, and set
$$ x_{\theta,b^{\theta k}}=\mu_\theta\ell_{\theta k}, $$
merging repeated bundles.

The construction gives the required type masses and exact supply totals:
$$ \sum_kx_{\theta,b^{\theta k}}=\mu_\theta, \qquad \sum_{\theta,k}x_{\theta,b^{\theta k}}b^{\theta k}_g =\sum_\theta q_{\theta g} =\sigma_g. $$
Every supported bundle contains only liked kinds. Moreover,
$$ |b^{\theta k}|:=\sum_gb^{\theta k}_g \in\{\lfloor t_\theta\rfloor,\lceil t_\theta\rceil\}. $$

Consider any ordered pair of supported cells, with comparing type $\theta$ and other type $\eta$, and write their bundles as $b,b'$.

If $t_\theta<t_\eta$, the separation property implies that $\theta$ likes none of the kinds in $b'$. Thus $\theta$ values $b'$ at zero, and EF1 holds.

Suppose instead that $t_\theta\ge t_\eta$. Let
$$ h=\sum_{g\in G_\theta}b'_g $$
be the number of items in $b'$ liked by $\theta$. Since every item in $b$ is liked by $\theta$,
$$ \widehat v_\theta(b)=|b|\ge\lfloor t_\theta\rfloor. $$
If $h=0$, EF1 holds immediately. If $h>0$, removing any liked item from $b'$ reduces its normalized value to $h-1$, and
$$ \begin{aligned} h-1 &\le |b'|-1\\ &\le \lceil t_\eta\rceil-1\\ &\le \lfloor t_\eta\rfloor\\ &\le \lfloor t_\theta\rfloor\\ &\le |b|. \end{aligned} $$
Multiplying by $c_\theta$ proves the original EF1 inequality.

These cases cover every ordered pair, including pairs within one type. Fractional Pareto optimality follows from Section 1.

The rounding lemma produces at most $m+1$ cells per type. Its inputs $q_{\theta g}/\mu_\theta$ have polynomial bit length, as do the resulting masses and binary-encoded bundles. This completes the theorem.

6. An overlapping example

Take two types of mass $1/2$, with normalized valuations
$$ v_1=(1,1,0),\qquad v_2=(0,1,1), $$
and supplies
$$ \sigma=\left(\frac14,1,\frac14\right). $$
The individual neighborhood ratios are $5/2$, while the ratio for both types together is $3/2$. They therefore form one bottleneck group.

An aggregate allocation is
$$ q_1=\left(\frac14,\frac12,0\right), \qquad q_2=\left(0,\frac12,\frac14\right). $$
The rounding construction yields these four cells:

| Type | Bundle | Mass |
|---|---|---|
| $1$ | $(0,1,0)$ | $1/4$ |
| $1$ | $(1,1,0)$ | $1/4$ |
| $2$ | $(0,1,0)$ | $1/4$ |
| $2$ | $(0,1,1)$ | $1/4$ |

Every bundle has one or two liked items, so the preceding EF1 proof applies. All supplies are exhausted using liked assignments, which certifies fractional Pareto optimality.

7. What remains open

This theorem settles the mass-society problem when each valuation row has a single positive value, with arbitrary zeros and overlaps. It does not settle the question for arbitrary fixed $\tau$.

The argument relies on two properties specific to this class: utility is proportional to liked-item count, and assigning every kind to a liker automatically maximizes a positive weighted utility sum. With several distinct positive values in a type’s row, neither property supports the same construction.

The remaining target is a polynomial-time algorithm for arbitrary overlapping, nonproportional valuations at every fixed support size, or a hardness proof for some fixed support size. Neither is established here.

⟨structured verdict parsed — rendered above⟩

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

Verification report

The restricted theorem is correct under the standard interpretation that “binary rational” means a rational number encoded by binary integers. The general task remains unresolved, as the prover explicitly acknowledges. No substantive gap or false step was found in the restricted theorem.

The proved result applies only when each type’s positive valuations are all equal. It does not establish either a polynomial-time algorithm for arbitrary valuations at every fixed support size or hardness for some fixed support size.

1. Normalization and fractional Pareto optimality

The normalization is valid. Since $c_\theta>0$, dividing type $\theta$’s utility by $c_\theta$ preserves its EF1 comparisons and its weak and strict utility improvements.

The proposed efficiency certificate is also valid:

The weights $x_{\theta,b}/c_\theta$ are strictly positive for every supported cell. Thus an improvement that is weak everywhere and strict in at least one cell would strictly increase this sum, contradicting the upper bound.

This argument correctly handles arbitrary real-valued fractional reassignments and does not impose EF1 on those reassignments.

2. Rounding lemma

All claims in the lemma check out.

The floor differences are nonnegative integers because the cumulative sums are nondecreasing. A zero coordinate produces identical consecutive cumulative sums, hence a zero bundle coordinate throughout.

The integral identity
$$ \int_0^1\lfloor A+s\rfloor\,ds=A $$
is correct, including when $A$ is integral. Subtracting consecutive identities gives the required coordinate expectations.

The telescoping identity is correct because $\lfloor s\rfloor=0$ throughout $[0,1)$. It establishes the asserted cardinality bound.

Each cumulative sum contributes at most one interior breakpoint. Therefore there are at most $k+1$ positive-length intervals. The half-open convention assigns breakpoint values consistently; endpoints do not affect expectations. Merging repeated bundles preserves expectations and cannot increase support size.

The polynomial bit-length claim is justified: cumulative sums, breakpoints, interval lengths, and floor values all have polynomial-size rational or integer representations. Large coordinate magnitudes are handled through binary encoding.

3. Bottleneck groups

Maximal minimizing subset

The neighborhood identities and the submodularity inequality are correct.

The lower bound
$$ f_R(E)\ge t\mu(E) $$
also holds for the empty set, where both sides are zero. Applying it to the union and intersection gives the reverse inequality needed in the displayed argument. Hence the union of two minimizing subsets is minimizing.

There are finitely many subsets, so their repeated union yields the unique inclusion-wise maximal minimizing subset $A$. Positive masses ensure that every nonempty subset has a positive denominator.

Allocation within a group

The max-flow/min-cut application is justified as written. The network is finite and has nonnegative rational capacities. Choosing each type-to-kind capacity greater than the total source capacity excludes those edges from a minimum cut.

The displayed cut calculation verifies that every cut has capacity at least $t\mu(A)$. Thus all source-to-type capacities can be saturated. Since the total kind-to-sink capacity equals that same quantity, every supply in $H$ is exhausted.

The resulting flows satisfy all claimed row sums, column sums, and liked-only restrictions.

Increasing levels and separation

The identity
$$ f_{R\setminus H}(B)=f_R(A\cup B)-f_R(A) $$
is correct: the removed neighborhood is precisely $H=N_R(A)$.

Equality in the ensuing lower bound would make $A\cup B$ another minimizing subset, contradicting maximality. Thus subsequent levels strictly increase.

The positivity and termination assertions are valid. Initially every nonempty type subset has positive neighborhood supply. The strict inequality preserves that property at subsequent stages. Every remaining kind retains a remaining liker, so no kinds remain after all types have been processed.

The separation property follows from removing all currently remaining kinds liked by a processed type. Later allocations use only remaining kinds.

4. Polynomial-time construction

The LP is feasible and bounded. Its optimum equals the minimum neighborhood ratio:

The denominator argument is correct. A common denominator $D$ can be represented with polynomially many bits, and
$$ 1\le M_B\le D $$
follows from positive masses and $\mu(B)\le1$. Distinct ratios consequently differ by at least $1/D^2$.

The perturbation
$$ \varepsilon=\frac1{2D^2} $$
correctly separates minimizing from nonminimizing subsets. Original minimizers have positive perturbed surplus; all other nonempty subsets have negative surplus; the empty subset has zero surplus.

The minimum-cut recovery argument is valid. Its large capacity excludes type-to-kind cut edges, and positive supplies exclude unnecessary source-side kinds. Among original minimizers, $A$ uniquely maximizes mass because every other minimizer is a proper subset of $A$ and all type masses are positive.

The complexity claim is supported. There are at most $\tau$ stages, each using polynomial-size rational LP and flow instances. The relevant exact polynomial-time results apply to these rationally encoded instances. The construction does not enumerate a population of size $D$.

5. Final allocation and EF1

The conditional expectations are well-defined because $\mu_\theta>0$. Multiplying the rounding probabilities by $\mu_\theta$ produces positive rational cell masses, with the correct total mass for each type.

The expectation identities give exact supply exhaustion. Coordinates with zero aggregate allocation remain zero after rounding, so all supported bundles remain liked-only.

Every ordered EF1 comparison is covered:

In particular,
$$ \lceil t_\eta\rceil-1\le\lfloor t_\eta\rfloor $$
holds both for integral and nonintegral levels. The argument includes comparisons within one type and comparisons involving empty bundles.

Scaling back by $c_\theta$ gives precisely the required original EF1 inequality. Section 1 then certifies fractional Pareto optimality.

The support bound $\tau(m+1)$ and polynomial output bit length follow from the rounding lemma.

6. Example

The numerical example is consistent.

Each individual neighborhood has supply $5/4$ and mass $1/2$, giving ratio $5/2$. The combined neighborhood has supply $3/2$ and mass $1$, giving ratio $3/2$.

The aggregate allocations have the required row and column sums. The four listed cells reproduce those allocations, have the stated type masses, and satisfy the proved EF1 and efficiency conditions.

7. Scope and actionable feedback

The output establishes genuine polynomial-time progress for the equal-positive-value restriction, including variable support size. It does not resolve the general complexity question in USER_TASK.

No repair of the restricted proof is required under the binary-encoded-rational interpretation. To complete the original assignment, the prover must provide either the requested algorithm for arbitrary valuations at every fixed $\tau$ or a hardness result for some fixed $\tau$. That requires additional mathematics, not an expositional clarification.

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