Answer: —
Theorem 3.1 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateThere exists a constant $\varepsilon > 0$ such that finding an $\varepsilon$-approximate consensus halving for $n$ agents with monotonic utilities that uses at most $n$ cuts is PPAD-hard, even if all agents have symmetric-threshold utilities.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given \(m\) items, a rational distribution \(\mu\) over \(\tau\) positive-mass symmetric-threshold utility types with values \(u_t(j)\) and caps \(c_{tj}\), and the fixed constant \(\varepsilon\), find \(x\in[0,1]^m\) with \(\kappa(x)=|\{j:0<x_j<1\}|\leq\tau\) such that every type \(t\) satisfies \(\left|\sum_j f_{tj}(x_j)u_t(j)-\sum_j f_{tj}(1-x_j)u_t(j)\right|\leq\varepsilon\sum_j u_t(j)\).
A society is given by its support: a list of \(\tau\geq1\) distinct utility types with positive binary-rational masses \(\mu_t\), summing to \(1\). Here \(\tau\) is the support size, not the number of possible types.
There are \(m\geq1\) unordered, divisible items. Type \(t\) has binary-rational values \(u_t(j)\geq0\) and caps \(0\leq c_{tj}<1/2\). Define \(f_{tj}(z)=\max\{0,\min\{1,(z-c_{tj})/(1-2c_{tj})\}\}\) and \(U_t(x)=\sum_{j=1}^{m}u_t(j)f_{tj}(x_j)\).
Fix a sufficiently small positive rational constant \(\varepsilon\) in the finite-agent hardness regime. The search problem asks for a rational vector \(x\in[0,1]^m\) such that \(\kappa(x)=|\{j:0<x_j<1\}|\leq\tau\) and \(|U_t(x)-U_t(\mathbf{1}-x)|\leq\varepsilon\sum_{j=1}^{m}u_t(j)\) for every support type \(t\), independently of its mass. Let \(L\) be the total binary input length.
Is this search problem solvable in time polynomial in \(m,\tau,L\), or is it NP-hard?
For a sufficiently small fixed positive error, the finite-agent version is PPAD-hard even with symmetric-threshold utilities, and belongs to PPA. [Verified source](https://pubsonline.informs.org/doi/full/10.1287/moor.2021.1249).
The support formulation is computationally equivalent to the version with one agent per distinct type, so these bounds apply here as well; they do not establish NP-hardness or a polynomial-time algorithm.
I do not settle the classification for unrestricted $\tau$. I prove the stronger algorithmic bound
$$
2^{O(\tau\log(2+\tau/\varepsilon))}
\operatorname{poly}(m,\tau,L).
$$
For fixed $\varepsilon$, this improves the verified bound in the notes from $2^{O(\tau^2)}$ to $2^{O(\tau\log(\tau+1))}$.
The improvement replaces exhaustive endpoint assignments with a dynamic program that retains one assignment per rounded vector of utility totals. I also give a polynomial-time exact algorithm when each item’s cap is independent of the type.
Throughout, values and caps have rational binary encodings. The masses play no role because every support type has its own requirement.
Write
$$
W_t=\sum_{j=1}^m u_t(j).
$$
If $W_t=0$, nonnegativity implies that every $u_t(j)$ is zero, so this type imposes no restriction. Define
$$
w_{tj}=
\begin{cases}
u_t(j)/W_t,&W_t>0,\\
0,&W_t=0.
\end{cases}
$$
Thus each row of $w$ sums to either $1$ or $0$.
Let
$$
d_{tj}(z)=2f_{tj}(z)-1.
$$
The two unclipped affine expressions defining $f_{tj}(z)$ and $f_{tj}(1-z)$ sum to $1$. Clipping to $[0,1]$ preserves this complementary identity, so
$$
f_{tj}(1-z)=1-f_{tj}(z).
$$
Consequently, with
$$
A_t(x)=\sum_{j=1}^m w_{tj}d_{tj}(x_j),
$$
the required utility condition for a positive-value type is exactly
$$
|A_t(x)|\leq\varepsilon.
$$
Moreover,
$$
d_{tj}(0)=-1,\qquad d_{tj}(1)=1,\qquad
d_{tj}(1-z)=-d_{tj}(z).
$$
If $\tau\geq m$, setting every coordinate to $1/2$ is an exact solution. The algorithm below therefore only needs to address $\tau<m$.
Every instance has a real vector $x$ satisfying
$$
A_t(x)=0\quad\text{for all }t,
\qquad
\kappa(x)\leq\tau.
$$
Proof. Use the following form of the Borsuk–Ulam theorem: every continuous odd map from $S^\tau$ to $\mathbb R^\tau$ has a zero.
For $a=(a_0,\ldots,a_\tau)\in S^\tau$, define
$$
p_a(s)=\sum_{i=0}^{\tau}a_i s^i,
\qquad
x_j(a)=\lambda\{s\in[j-1,j]:p_a(s)\geq0\},
$$
where $\lambda$ denotes length. Since $a$ is a unit vector, $p_a$ is a nonzero polynomial.
Each coordinate $x_j(a)$ depends continuously on $a$. Indeed, if $a^{(n)}\to a$, then the sign indicators converge pointwise wherever $p_a(s)\neq0$. The exceptional set is finite, and the indicators are bounded by $1$. Dominated convergence on the item interval proves continuity.
The zero set of $p_a$ has length zero. Since $p_{-a}=-p_a$,
$$
x(-a)=\mathbf1-x(a).
$$
Therefore
$$
F(a)=\bigl(A_1(x(a)),\ldots,A_\tau(x(a))\bigr)
$$
is continuous and odd. Borsuk–Ulam supplies $a^*$ with $F(a^*)=0$.
If $0<x_j(a^*)<1$, the polynomial takes both positive and negative values in the interior of that item interval. The intermediate value theorem gives a root in its interior. Distinct split items give distinct roots, while a nonzero polynomial of degree at most $\tau$ has at most $\tau$ roots. Hence $\kappa(x(a^*))\leq\tau$. $\square$
An exact solution from Lemma 1 can be replaced by a rational exact solution of polynomial encoding length without increasing its number of split items.
Proof. Let $S$ be the split coordinates of a real exact solution, with $r=|S|\leq\tau$. Freeze all coordinates outside $S$ at their endpoint values.
For each $j\in S$, sort the distinct breakpoints
$$
\{0,1\}\cup\{c_{tj},1-c_{tj}:t\in[\tau]\}.
$$
Choose a closed interval between consecutive breakpoints containing the real coordinate. Every $d_{tj}$ is affine on that interval; adjacent formulas agree at the breakpoints.
The exact balance equations and these interval bounds define a nonempty bounded rational polytope in $r$ variables. It has a vertex. At a vertex, the active constraints have rank $r$: otherwise a nonzero direction preserving every active constraint would permit sufficiently small feasible perturbations in both directions, contradicting extremality.
Choose $r$ independent active constraints. Their rational coefficients have polynomial bit length. This follows because they are formed from the input rationals by sums, products, and division by the nonzero rationals $1-2c_{tj}$. Clearing denominators gives an integer system with polynomial-bit entries. Cramer’s rule and the determinant bound
$$
|\det B|\leq r!M^r
$$
for an $r$ by $r$ matrix with entries of absolute value at most $M$ show that its solution has polynomial bit length.
Every point in this polytope satisfies exact balance and can split only coordinates in $S$. The case $r=0$ already has a rational endpoint solution. $\square$
For fixed rational $0<\varepsilon<1$, the required allocation can be found deterministically in time
$$
2^{O(\tau\log(2+\tau/\varepsilon))}
\operatorname{poly}(m,\tau,L).
$$
Set
$$
\delta=\frac{\varepsilon}{2\tau}.
$$
Call an item heavy if $w_{tj}>\delta$ for at least one type. Let $H$ be the heavy-item set, let $K=[m]\setminus H$, and write $h=|H|$.
For a fixed positive-value type, fewer than $1/\delta$ items can have weight greater than $\delta$, because its weights sum to $1$. Taking a union over types gives
$$
h<\frac{\tau}{\delta}
=\frac{2\tau^2}{\varepsilon}.
$$
Every light item satisfies
$$
w_{tj}\leq\delta
\quad\text{for every }t.
$$
For the existence argument, replace all light-item caps by zero. The resulting normalized balance functions are
$$
A_t^H(x)=
\sum_{j\in H}w_{tj}d_{tj}(x_j)
+\sum_{j\in K}w_{tj}(2x_j-1).
$$
This modified system is still a system of symmetric-threshold utilities. Lemma 1 therefore gives an exact allocation $x^*$ with
$$
A_t^H(x^*)=0,\qquad \kappa(x^*)\leq\tau.
$$
The algorithm does not need to compute $x^*$.
Enumerate every set $S\subseteq H$ with $|S|\leq\tau$. These are the heavy items allowed to remain fractional.
For each $j\in S$, enumerate one interval between consecutive breakpoints from
$$
\{0,1\}\cup\{c_{tj},1-c_{tj}:t\in[\tau]\}.
$$
There are at most $2\tau+1$ choices per coordinate. On a chosen interval, write the rational affine formula for $d_{tj}$ as
$$
d_{tj}(z_j)=a_{tj}z_j+b_{tj}.
$$
It remains to handle endpoint assignments on $T=H\setminus S$ without enumerating all of them.
Define
$$
\eta=\frac{\varepsilon}{4\max\{1,h\}},
\qquad
q_{tj}=\left\lfloor\frac{w_{tj}}{\eta}\right\rfloor.
$$
An endpoint assignment on $T$ is specified by the subset $B\subseteq T$ assigned endpoint $1$; all other items in $T$ receive endpoint $0$.
Associate with $B$ the integer vector
$$
v(B)=\left(\sum_{j\in B}q_{tj}\right)_{t=1}^{\tau}.
$$
A standard subset-sum dynamic program retains one representative subset for each reachable vector. Initially, the zero vector has representative $\varnothing$. When processing item $j$, each existing state has an exclusion transition and an inclusion transition adding $(q_{tj})_t$. If transitions collide, retain either representative.
Induction over processed items proves that every reachable vector remains represented.
For every coordinate,
$$
\sum_{j\in B}q_{tj}
\leq \frac{1}{\eta}\sum_{j\in B}w_{tj}
\leq\frac1\eta.
$$
Thus the number of states is at most
$$
N=\left(1+\left\lfloor\frac1\eta\right\rfloor\right)^\tau.
$$
The compression has a controlled error. Write
$$
w_{tj}=\eta q_{tj}+r_{tj},
\qquad 0\leq r_{tj}<\eta.
$$
If $v(B)=v(B')$, their integer contributions cancel, and each remainder sum lies between $0$ and $h\eta$. Hence
$$
\left|
\sum_{j\in B}w_{tj}-\sum_{j\in B'}w_{tj}
\right|
\leq h\eta.
$$
Their signed endpoint contributions therefore differ by at most
$$
\left|
\sum_{j\in T}w_{tj}(2\mathbf1_B(j)-1)
-
\sum_{j\in T}w_{tj}(2\mathbf1_{B'}(j)-1)
\right|
\leq2h\eta
\leq\frac{\varepsilon}{2}.
$$
For every enumerated $S$, interval choice, and retained representative $B$, introduce variables $z_j$ for $j\in S$ and $y_j$ for $j\in K$. Define
$$
E_t(z,y)=
\sum_{j\in T}w_{tj}(2\mathbf1_B(j)-1)
+\sum_{j\in S}w_{tj}(a_{tj}z_j+b_{tj})
+\sum_{j\in K}w_{tj}(2y_j-1).
$$
Solve the rational linear feasibility problem consisting of the chosen interval bounds,
$$
0\leq y_j\leq1\quad(j\in K),
$$
and
$$
|E_t(z,y)|\leq\frac{\varepsilon}{2}
\quad(t\in[\tau]).
$$
At least one branch is feasible. Choose $S$ to be the fractional heavy coordinates of the sparse exact allocation $x^*$ for the modified system. Its size is at most $\tau$. Choose intervals containing its coordinates, and let $B^*\subseteq T$ describe its heavy endpoint assignments.
The dynamic program retains a representative $B$ with $v(B)=v(B^*)$. At $z_j=x_j^*$ and $y_j=x_j^*$, the expression using $B^*$ would equal $A_t^H(x^*)=0$. Replacing $B^*$ by $B$ changes it by at most $\varepsilon/2$, by the preceding calculation. Thus this branch is feasible.
Obtain a vertex $(z,y)$ of any feasible branch.
At most $\tau$ light coordinates can be fractional. To prove this, suppose more than $\tau$ coordinates $y_j$ lie strictly between $0$ and $1$. Their columns $(w_{tj})_{t=1}^{\tau}$ are linearly dependent. Therefore there is a nonzero vector $v$, supported on those coordinates, such that
$$
\sum_{j\in K}w_{tj}v_j=0
\quad\text{for every }t.
$$
Holding $z$ fixed, both $y+\alpha v$ and $y-\alpha v$ satisfy the coordinate bounds for sufficiently small $\alpha>0$. Every $E_t$ remains unchanged. Both points are feasible, contradicting extremality.
Round each light coordinate to a nearest endpoint $\widehat y_j\in\{0,1\}$. Each changed coordinate contributes an error bounded by
$$
|2w_{tj}(\widehat y_j-y_j)|
\leq w_{tj}\leq\delta.
$$
At most $\tau$ coordinates change, so
$$
|E_t(z,\widehat y)-E_t(z,y)|
\leq\tau\delta
=\frac{\varepsilon}{2}.
$$
Define the final allocation by keeping the heavy coordinates from this branch and using $\widehat y$ on the light items. At endpoints, original threshold utilities and linear utilities agree. Consequently its original normalized imbalance is exactly $E_t(z,\widehat y)$, and
$$
|A_t(\widehat x)|
\leq |E_t(z,y)|
+|E_t(z,\widehat y)-E_t(z,y)|
\leq\varepsilon.
$$
All light items and all heavy items outside $S$ are endpoints. Thus
$$
\kappa(\widehat x)\leq|S|\leq\tau.
$$
The number of sets $S$ is at most $(h+1)^\tau$. This bound follows by encoding each subset of size at most $\tau$ as a sorted list padded to length $\tau$ with a sentinel.
There are at most $(2\tau+1)^\tau$ interval choices per set, and at most $N$ retained endpoint assignments. Since
$$
h=O(\tau^2/\varepsilon),
\qquad
\frac1\eta
=O(\tau^2/\varepsilon^2),
$$
the total number of linear programs is bounded by
$$
(h+1)^\tau(2\tau+1)^\tau
\left(1+\left\lfloor\frac1\eta\right\rfloor\right)^\tau
=
2^{O(\tau\log(2+\tau/\varepsilon))}.
$$
The dynamic programs have the same bound up to polynomial factors.
All linear programs have polynomially many variables and constraints and polynomial-bit rational coefficients. Exact rational linear programming decides feasibility and optimizes rational linear objectives in polynomial time.
A vertex can be obtained by minimizing coordinates successively, fixing each optimum before minimizing the next coordinate. Each optimization selects a nonempty face of the preceding polytope. After all coordinates are fixed, the remaining face is a singleton, hence a vertex of the original polytope. Its encoding length is polynomial by the determinant argument in Lemma 2.
All rounding and reconstruction operations use exact rational arithmetic. This completes the proof of the theorem.
Suppose that for each item there is a common cap $c_j$ such that
$$
c_{tj}=c_j\quad\text{for every type }t.
$$
Then an exact solution is computable in polynomial time.
Let $f_j$ be the common threshold function, and introduce variables $y_j\in[0,1]$. Solve
$$
\sum_{j=1}^m u_t(j)y_j=\frac{W_t}{2}
\quad(t\in[\tau]).
$$
This bounded rational polytope is nonempty because $y_j=1/2$ satisfies every equation.
At a vertex, at most $\tau$ coordinates are fractional: if there were more, linear dependence among their value columns would give two feasible perturbations, exactly as in Section 3.5.
Recover an allocation by setting
$$
x_j=
\begin{cases}
0,&y_j=0,\\
1,&y_j=1,\\
c_j+(1-2c_j)y_j,&0<y_j<1.
\end{cases}
$$
Then $f_j(x_j)=y_j$. The complementary identity gives
$$
U_t(x)-U_t(\mathbf1-x)
=
\sum_j u_t(j)(2y_j-1)=0.
$$
Furthermore, $x_j$ is fractional exactly when $y_j$ is fractional. Hence $\kappa(x)\leq\tau$. Rational linear programming and the displayed reconstruction both take polynomial time.
This settles a substantial restricted case, including caps arbitrarily close to $1/2$.
The supplied constant-error $\mathrm{PPAD}$-hardness theorem applies to precisely the symmetric-threshold utility class and relative error used here. The cited paper also states $\mathrm{PPA}$ membership. These bounds imply that an unrestricted polynomial-time algorithm would solve every $\mathrm{PPAD}$ search problem in polynomial time, but they do not establish $\mathrm{NP}$-hardness. [Goldberg et al., *Consensus Halving for Sets of Items*, Theorem 4 and conclusion](https://pubsonline.informs.org/doi/full/10.1287/moor.2021.1249).
There is also a total-search obstruction to conventional $\mathrm{NP}$-hardness, which can be proved directly here.
By Lemma 2, every instance has a valid allocation of polynomial encoding length. Such an allocation is verifiable in polynomial time: check the coordinate bounds, count split items, and evaluate the rational utility differences. Restricting outputs to a sufficiently large polynomial length bound therefore gives a total, polynomially verifiable search relation.
Now suppose a deterministic polynomial-time oracle reduction decides satisfiability using this search relation, correctly for every valid oracle. An unsatisfiability certificate can consist of a complete rejecting oracle transcript:
The transcript has polynomial length, and all checks take polynomial time. For an unsatisfiable formula, totality supplies a valid oracle and hence such a rejecting transcript. For a satisfiable formula, any verified consistent transcript extends to a valid oracle: assign its recorded replies on queried inputs and choose valid replies elsewhere. Correctness excludes rejection for that oracle.
Thus unsatisfiability belongs to $\mathrm{NP}$, implying
$$
\mathrm{NP}=\mathrm{coNP}.
$$
This is a conditional consequence of the specified reduction notion, not an unconditional exclusion of $\mathrm{NP}$-hardness.
The improved algorithm remains superpolynomial when $\tau$ is unrestricted. No general polynomial-time algorithm or $\mathrm{NP}$-hardness reduction is established here.
⟨structured verdict parsed — rendered above⟩
The output establishes valid partial results, including the claimed parameter-dependent algorithm and the polynomial-time algorithm for common item caps. I found no substantive mathematical error in these arguments. It does not resolve the unrestricted classification requested by USER_TASK, and it explicitly acknowledges this limitation.
The normalization is correct. If $W_t=0$, nonnegative values imply $u_t(j)=0$ for every item, so that type’s requirement is automatic. Otherwise, dividing by $W_t$ preserves exactly the required relative-error inequality.
The complementary identity is also correct: the two unclipped affine expressions sum to $1$, and clipping satisfies the same identity. Consequently,
$$ U_t(x)-U_t(\mathbf 1-x)=W_tA_t(x). $$
The endpoint values and oddness of $d_{tj}$ follow. Setting every coordinate to $1/2$ gives exact balance, and satisfies the split bound whenever $\tau\geq m$. Masses correctly play no role.
Finding: Correct, including the zero-value and large-support cases.
The stated Borsuk–Ulam theorem has the correct dimensions and hypotheses.
The construction satisfies them:
The split-count argument is valid. A split interval has positive-length positive and negative regions; hence it contains an interior root. Interiors of distinct item intervals are disjoint, so distinct split items require distinct roots. The polynomial has at most $\tau$ roots.
Finding: Correct. The theorem’s hypotheses and the sparsity conclusion are verified.
Freezing the nonsplit coordinates preserves their rational endpoint values. The listed breakpoints partition each remaining coordinate domain into closed intervals on which all relevant functions are affine. Continuity ensures that the formulas remain valid at interval boundaries.
The resulting polytope is rational, bounded, and nonempty. Its vertex argument works even when the polytope is lower-dimensional: deficient rank among all active constraints would permit feasible perturbations in both directions.
The bit-length argument is sound. Normalization, affine coefficients, and equation formation involve polynomially many rational arithmetic operations with polynomial-bit inputs. Clearing denominators preserves polynomial bit length. The determinant bound then gives polynomial-length rational vertex coordinates.
The separate treatment of $r=0$ covers the endpoint-only case.
Finding: Correct. This establishes existence of polynomial-length exact certificates, without claiming an efficient method to find the appropriate polytope.
The heavy-item estimate is valid. Each positive-value row has fewer than $1/\delta$ entries strictly exceeding $\delta$, and taking their union gives
$$ h<\frac{2\tau^2}{\varepsilon}. $$
Every light-item weight is at most $\delta$. Replacing light caps by zero produces functions to which Lemma 1 applies. Distinctness of the modified utility rows is unnecessary for that lemma’s proof.
Finding: Correct.
Every possible set of fractional heavy coordinates of the modified sparse solution is enumerated. Every such coordinate belongs to one of the enumerated closed breakpoint intervals, including when it equals a breakpoint.
The bounds on the number of sets and interval choices are valid.
Finding: Correct and exhaustive for the existence argument.
The subset-sum recurrence preserves every reachable integer vector, while retaining one representative per vector.
Each coordinate of a state is bounded by $1/\eta$. Thus the stated state-count bound is valid, including zero-value rows and zero rounded weights.
For colliding states, their rounded contributions agree. Each residual sum lies between $0$ and $h\eta$, so the difference of residual sums is at most $h\eta$, rather than requiring twice that amount. Passing to signed endpoint contributions introduces the stated factor of $2$:
$$ 2h\eta\leq\frac{\varepsilon}{2}. $$
This remains valid when $h=0$, because the definition of $\eta$ avoids division by zero.
Finding: Correct. The compression does not lose the feasibility guarantee.
The modified exact solution supplies an enumerated set, interval choice, and endpoint state. Replacing its endpoint subset by the retained representative changes every normalized balance by at most $\varepsilon/2$. Therefore the specified linear feasibility problem has a feasible branch.
Finding: Correct. No computation of the existential allocation is assumed.
The vertex argument correctly bounds the number of fractional light coordinates by $\tau$. A dependence among their columns preserves every $E_t$, while sufficiently small perturbations preserve their coordinate bounds and leave the heavy variables fixed.
Nearest-endpoint rounding changes each affected row contribution by at most $w_{tj}\leq\delta$. Therefore,
$$ |E_t(z,\widehat y)-E_t(z,y)| \leq\tau\delta=\frac{\varepsilon}{2}. $$
After rounding, all light coordinates are endpoints, where their original and modified utilities agree. Heavy utilities are represented exactly on the chosen intervals. Combining the feasibility tolerance with the rounding error gives the required error $\varepsilon$.
Only coordinates in $S$ can remain split, so the final split count is at most $\tau$.
Finding: Correct. No bound on the combined number of fractional coordinates before rounding is needed.
The product of enumeration and state-count bounds has the claimed form:
$$ 2^{O(\tau\log(2+\tau/\varepsilon))}. $$
The rational linear programs have polynomial dimensions and polynomial-bit coefficients. The invoked polynomial-time rational linear-programming result applies.
Successive coordinate minimization produces nested nonempty faces. Once all coordinates are fixed, the face is a singleton and therefore an original-polytope vertex. Intermediate optimal values also have polynomial bit length because each is attained at an original-polytope vertex; thus successive optimization does not invalidate the complexity claim.
Finding: The stated algorithmic bound and rational-output guarantee are established.
The linear feasibility system is nonempty at $y_j=1/2$. The same dependence argument bounds the number of fractional coordinates at a vertex by $\tau$.
The reconstruction satisfies $f_j(x_j)=y_j$. For fractional $y_j$, the assumption $c_j<1/2$ ensures the reconstructed coordinate is strictly between $0$ and $1$. The endpoint cases are handled explicitly.
The displayed utility calculation proves exact balance, and rational reconstruction preserves polynomial encoding length.
Finding: Correct, including caps arbitrarily close to $1/2$. This is a restricted case, not a classification of unrestricted inputs.
The cited theorem matches the symmetric-threshold class, relative-error convention, and agent-dependent split bound. The cited conclusion also states membership in $\mathrm{PPA}$. The transfer to support types is expressly supplied by USER_TASK. [Goldberg et al., *Consensus Halving for Sets of Items*, Theorem 4 and conclusion](https://pubsonline.informs.org/doi/full/10.1287/moor.2021.1249)
The conditional oracle-hardness argument is valid under its expressly stated reduction notion and polynomially bounded search relation:
Thus the conditional conclusion $\mathrm{NP}=\mathrm{coNP}$ follows. The output correctly avoids presenting it as an unconditional exclusion of $\mathrm{NP}$-hardness.
Finding: Correct as a conditional statement. It does not answer the unrestricted classification.
Where: Sections 1 and 5.
The parameter-dependent running time is not a polynomial bound in unrestricted $\tau$. The common-cap result concerns an additional hypothesis absent from USER_TASK. No $\mathrm{NP}$-hardness reduction is supplied.
Minimum feedback: Retain the explicit partial-status statement. Resolving the assigned target requires an additional unrestricted complexity result; clarification alone cannot supply it.
Where: Section 1, the reference to “the verified bound in the notes.”
Neither USER_TASK nor the supplied materials identify those notes or establish the earlier bound $2^{O(\tau^2)}$. The new bound is independently proved, but the comparison cannot be audited from the supplied record.
Minimum feedback: Identify the earlier result and its assumptions, or remove the comparison.
The direction is promising because its principal algorithmic and structural claims survive verification. The appropriate overall status is partial.
⟨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.