Answer: For explicit terminal-table output, computation is NP-hard under polynomial-time metric reductions and cannot run in polynomial time because the table can be exponentially large. Even deciding whether terminal revenue is below a rational threshold is NP-hard under polynomial-time many-one reductions.
Theorem 3.3 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateOur mechanism can be implemented in polynomial time.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite type set \(T\), rational masses \(\mu_t\), and type-specific values \(v_t\), budgets \(B_t\), and integral caps \(K_t\), together with a rational monotone submodular rank oracle \(F_\mu:2^T\to\mathbb{Q}_+\) whose capacities scale with population mass, compute the terminal mass table \(\pi_{t,k,p}\) produced by an ascending-price clinching auction. Here \(\pi_{t,k,p}\) is the mass of type-\(t\) people receiving \(k\in\{0,\ldots,K_t\}\) indivisible goods and paying \(p\); cohort splits preserve the aggregate polymatroid constraints. Is this outcome computable in time polynomial in \(|T|\), \(\sum_t K_t\), the rational input bit length, and the number of value-oracle calls?
A society is given by its support: an ordered list \(T\) of \(\tau\ge2\) types with positive binary rational masses \(\mu_t\), summing to \(1\); \(\tau\) is the support size. Each type has positive rational per-unit value \(v_t\), positive rational per-person budget \(B_t\), and integral per-person cap \(K_t\ge1\). Put \(m=\sum_tK_t\).
A value oracle supplies a normalized monotone submodular rank \(F_\mu:2^T\to\mathbb Q_+\), with \(F_\mu(T)>0\), \(F_\mu(\{t\})\le\mu_tK_t\), and \(F_\mu(T)=F_\mu(T\setminus\{t\})\) for every type. Capacities measure goods mass and scale linearly under common rescaling of population mass. Let \(L\) include the rational input encoding and a bound on oracle-answer bit lengths.
Use the following cohort interpretation of the ascending-price auction. A cohort \(C=(t,a,k,p,d)\) consists of mass \(a>0\) whose people each have \(k\) goods, have paid \(p\), and have integral demand \(d\ge0\). Initially each type forms one cohort \((t,\mu_t,0,0,K_t+1)\), and the price is \(c=0\); a cohort is active when \(d>0\).
For the current cohorts, write \(x_t=\sum_{C:t(C)=t}a_Ck_C\). Feasible additional aggregate transactions form \(R=\{y\ge0:\sum_{C:t(C)\in S}y_C\le F_\mu(S)-\sum_{t\in S}x_t\ (S\subseteq T),\ y_C\le a_C\min(d_C,K_{t(C)}-k_C)\}\).
A clinching sweep visits the cohorts present at its start in lexicographic order of \((t,k,p,d)\). At each visit recompute \(R\) and choose the largest \(r\ge0\) for which \(\{y_{-C}:y\in R,\ y_C=r\}=\{y_{-C}:y\in R,\ y_C=0\}\).
With \(q=\lfloor r/a_C\rfloor\) and \(\theta=r/a_C-q\), replace the visited cohort by masses \(a_C(1-\theta)\) and \(a_C\theta\) receiving respectively \(q\) and \(q+1\) additional goods; receiving \(j\) goods changes its state to \((k+j,p+cj,d-j)\). Discard zero masses, visit no newly created cohort in that sweep, and merge identical states after the sweep.
While active cohorts remain, advance the price to \(\min_{C:d_C>0}\min\{v_{t(C)},(B_{t(C)}-p_C)/d_C\}\). At that price, first process active valuation-equality cohorts by setting their demand to zero, then process active budget-equality cohorts by decreasing their demand by one; select ties lexicographically and execute a clinching sweep after every individual update, reevaluating pending equalities.
The terminal table \(\pi_{t,k,p}\) records the mass of people of type \(t\) receiving \(k\in\{0,\ldots,K_t\}\) goods and paying total amount \(p\), summing over terminal demands.
Is exact computation of this terminal mass table polynomial in \(m,\tau,L\), with polynomially many value-oracle calls, or is it NP-hard? For hardness, restrict to ranks supplied by polynomial-size descriptions with polynomial-time evaluation.
The finite-buyer integer-polymatroid clinching auction is computable in time polynomial in the numbers of buyers and goods; with the goods count encoded in binary, that bound is pseudo-polynomial. [Hirai–Sato](https://arxiv.org/html/2303.00231v4)
No complexity classification for the exact cohort model specified here was identified in the literature search.
For explicitly listed terminal tables, the problem is NP-hard under polynomial-time metric reductions. More substantively, even the following scalar problem is NP-hard under ordinary polynomial-time many-one reductions:
Given an auction instance and a rational threshold $\rho$, decide whether its terminal revenue is less than $\rho$.
This holds for ranks with polynomial-size descriptions and polynomial-time evaluation. On the constructed instances, terminal revenue is a rational number of polynomial bit length.
I use the explicit-output interpretation of the table: all nonzero entries are listed. Because such tables can be exponentially long, the reduction convention matters. A polynomial-time metric reduction from a function $f$ to a function $g$ consists of polynomial-time functions $A,D$ satisfying
$$
f(z)=D(z,g(A(z))).
$$
The decoding function is polynomial-time in the combined length of its arguments, including the returned table. This is the function-reduction convention used below; it does not assert that an exponentially long table can be scanned in time polynomial in the original instance. See, for example, the [definition of metric reductions](https://drops.dagstuhl.de/storage/00lipics/lipics-vol365-icdt2026/html/LIPIcs.ICDT.2026.12/LIPIcs.ICDT.2026.12.html).
The scalar revenue hardness is independent of this output-length distinction. I prove it first, then derive the table consequence and reprove the exponential output-size obstruction.
Fix an integer $n\ge 2$. Let the ordered types be $0,1,\ldots,n$, all with cap $n$. Thus
$$
\tau=n+1,\qquad m=n(n+1).
$$
Define
$$
\alpha=\frac{n2^n}{2n2^n-1},
\qquad
D_0=\alpha n,
\qquad
D_i=\frac{\alpha(2n-2i+1)}{2^i}
\quad(1\le i\le n),
$$
and set
$$
\mu_0=\alpha,\qquad
\mu_i=\frac{D_{i-1}-D_i}{n}
\quad(1\le i\le n).
$$
These masses are positive, since
$$
D_0-D_1=\frac{\alpha}{2}
$$
and, for $i\ge 2$,
$$
D_{i-1}-D_i
=\frac{\alpha(2n-2i+5)}{2^i}>0.
$$
Also $D_n=\alpha/2^n$, so
$$
\sum_{t=0}^n\mu_t
=\alpha+\frac{D_0-D_n}{n}
=\alpha\left(2-\frac{1}{n2^n}\right)
=1.
$$
Put
$$
G=n(1-\alpha),\qquad
F_\mu(S)=\min\left\{G,\ n\sum_{t\in S}\mu_t\right\}.
$$
Choose strictly increasing positive integer prices
$$
c_1<c_2<\cdots<c_n<V.
$$
Assign
$$
v_0=V,\qquad v_i=c_i\quad(1\le i\le n),
$$
and give every type budget
$$
B=(2n+2)V.
$$
Type $0$ will generate histories; the other types will exit at the specified prices.
Normalization and monotonicity are immediate. For $e\notin S$, the marginal increment is
$$
F_\mu(S\cup\{e\})-F_\mu(S)
=
\min\left\{
n\mu_e,\ \max\{0,G-n\mu(S)\}
\right\},
$$
where $\mu(S)=\sum_{t\in S}\mu_t$. This expression decreases as $S$ increases, proving submodularity.
The singleton bounds follow from the definition:
$$
F_\mu(\{t\})\le n\mu_t=\mu_tK_t.
$$
Every type satisfies $n\mu_t\le D_0$: this is equality for type $0$, and for $i\ge 1$ follows from
$$
n\mu_i=D_{i-1}-D_i\le D_{i-1}\le D_0.
$$
Consequently,
$$
n\sum_{s\ne t}\mu_s
=n-n\mu_t
\ge n-D_0
=G.
$$
Thus
$$
F_\mu(T\setminus\{t\})=F_\mu(T)=G>0.
$$
Finally,
$$
F_\mu(S)
=
n\min\left\{
\sum_{i=1}^n\mu_i,\ \sum_{t\in S}\mu_t
\right\}.
$$
This formula scales linearly under common rescaling of all population masses.
For a current cohort $C$, write
$$
b_C=a_C\min(d_C,n-k_C).
$$
Let
$$
X=\sum_Ca_Ck_C,\qquad
U=\sum_Cb_C,\qquad
s=G-X,\qquad
D=U-s.
$$
For this rank, the transaction region is
$$
R=\left\{
y\ge 0:
y_C\le b_C\text{ for all }C,\quad
\sum_Cy_C\le s
\right\}.
$$
The specified clinching amount is
$$
r_C=\min\{b_C,\max\{0,b_C-D\}\}.
$$
In particular, when $D\ge 0$,
$$
r_C=\max\{0,b_C-D\}.
$$
Proof. The rank constraints require both the total-supply bound and the bounds
$$
x(S)+\sum_{C:t(C)\in S}y_C\le n\mu(S).
$$
The latter follow from the cohort bounds, because for each type $t$,
$$
x_t+\sum_{C:t(C)=t}b_C
\le
\sum_{C:t(C)=t}a_Cn
=n\mu_t.
$$
Conversely, the original constraint for $T$ gives the total-supply bound. This proves the displayed description of $R$.
When $y_C=0$, the other coordinates can attain every total between zero and
$$
\min\{s,U-b_C\}.
$$
Fixing $y_C=r$ preserves their entire feasible projection precisely when
$$
0\le r\le b_C,\qquad
s-r\ge\min\{s,U-b_C\}.
$$
Solving these inequalities gives the claimed formula. $\square$
Every clinch preserves $D=U-s$. When $D\ge 0$, the children of a visited cohort have combined transaction bound
$$
\min\{b_C,D\}.
$$
Proof. A child receiving $j$ goods satisfies
$$
\min(d_C-j,n-k_C-j)
=\min(d_C,n-k_C)-j.
$$
The permitted increments stay within both demand and remaining cap. Weighting this identity by the child masses shows that their combined bound is $b_C-r_C$. Both $U$ and $s$ therefore decrease by $r_C$, preserving $D$.
For $D\ge 0$, Lemma 1 gives
$$
b_C-r_C=\min\{b_C,D\}.
$$
$\square$
Every event price is at most $V$, because every valuation is at most $V$. Hence every person pays at most $nV$, and every demand is at most $n+1$. For every active cohort,
$$
\frac{B-p_C}{d_C}
\ge
\frac{(2n+2)V-nV}{n+1}
=
\frac{n+2}{n+1}V
>V.
$$
Thus budget equality never occurs. The trigger exits occur at $c_1,\ldots,c_n$, followed by type-zero valuation updates at $V$.
Until those final updates, every type-zero cohort satisfies
$$
d_C=n+1-k_C,
$$
so it remains active, even when at cap, and
$$
b_C=a_C(n-k_C).
$$
Initially $U=n$ and $s=G$, so the deficit is $D_0$.
An unallocated trigger type $j$ has bound
$$
A_j=n\mu_j=D_{j-1}-D_j.
$$
At the sweep following trigger exit $i$, every future trigger $j>i$ satisfies
$$
A_j\le D_{j-1}\le D_i.
$$
It therefore clinches zero by Lemma 1. Inductively, all triggers remain unallocated until their valuation exits.
Exit $i$ removes exactly $D_{i-1}-D_i$ from $U$, leaving $s$ unchanged. Subsequent clinches preserve the deficit. Therefore the sweep at $c_i$ has deficit exactly $D_i$, regardless of any merging among type-zero cohorts.
Suppose no type-zero cohorts have merged before stage $i$.
After stage $i-1$, each type-zero cohort has mass
$$
a_{i-1}=\frac{\alpha}{2^{i-1}}
$$
and goods count either $i-2$ or $i-1$.
At the first stage,
$$
\frac{r}{\alpha}
=n-\frac{D_1}{\alpha}
=\frac12.
$$
At stage $i\ge 2$,
$$
\frac{D_i}{a_{i-1}}=n-i+\frac12.
$$
Consequently, the per-person clinch is $3/2$ for a parent with $k=i-2$, and $1/2$ for a parent with $k=i-1$.
Every parent therefore splits into equal halves with goods counts $i-1$ and $i$. The rule prohibiting visits to new children during the same sweep is essential here.
Label a history by bits $z_1,\ldots,z_i$, where
$$
k_i=i-1+z_i.
$$
Its purchase increments are $z_1$ at the first stage and
$$
1+z_h-z_{h-1}
$$
at stage $h\ge 2$. Its payment is therefore
$$
p_i
=
\sum_{h=2}^i c_h
+c_i z_i
-\sum_{h=1}^{i-1}(c_{h+1}-c_h)z_h.
$$
For a fixed $z_i$, two histories have identical payment precisely when their earlier bits give equal subset sums of the price gaps
$$
c_2-c_1,\ldots,c_i-c_{i-1}.
$$
They then also have identical goods count and demand, so they merge. Histories with different $z_i$ have different goods counts.
The following bound handles the auction after merging, without assuming that the original history formula continues to describe it.
Let $P$ be the number of type-zero cohorts present at the start of the sweep at $c_n$, and put
$$
a=\frac{\alpha}{2^n}=D_n.
$$
Immediately after that sweep,
$$
U_0\le Pa,
$$
where $U_0$ is the combined type-zero transaction bound.
If any merge occurred by the end of stage $n-1$, then
$$
P\le 2^{n-1}-1,
$$
and the type-zero allocation $X_{\mathrm{pre}}$ before price $V$ satisfies
$$
X_{\mathrm{pre}}
\ge
\alpha\left(n-\frac12\right)+a.
$$
Proof. By Lemma 2, the children of each parent visited at stage $n$ have combined bound at most $D_n=a$. Summing over the $P$ parents gives $U_0\le Pa$. Merging after the sweep preserves this sum.
Every parent produces at most two children. A merge by stage $n-1$ makes the cohort count strictly smaller than the maximum obtainable by repeated doubling; subsequent stages cannot recover that maximum. Thus $P\le 2^{n-1}-1$.
All triggers have exited without receiving goods. For type zero, demand still exceeds remaining cap by one, so
$$
U_0=\alpha n-X_{\mathrm{pre}}.
$$
It follows that
$$
X_{\mathrm{pre}}
\ge
\alpha n-(2^{n-1}-1)a
=
\alpha\left(n-\frac12\right)+a.
$$
$\square$
The source problem is Equal-Subset-Sum: given positive integers $w_1,\ldots,w_N$, decide whether two disjoint nonempty subsets have equal sums. This problem is NP-complete; see [Woeginger–Yu](https://www.sciencedirect.com/science/article/abs/pii/002001909290226L) and the positive-integer formulation in [Mucha–Nederlof–Pawlewicz–Węgrzycki](https://arxiv.org/html/1905.02424v2).
For positive integers, this is equivalent to asking whether two distinct subsets have equal sums. Indeed, canceling their intersection gives disjoint equal-sum subsets; neither remaining subset can be empty, because all weights are positive.
Let
$$
W=\sum_{h=1}^Nw_h,\qquad n=N+2.
$$
Use the auction family above, with prices determined by
$$
c_1=1,
$$
$$
c_{i+1}-c_i=w_i
\quad(1\le i\le N),
$$
and
$$
c_{N+2}-c_{N+1}=W+1.
$$
Thus $c_n=2W+2$. Choose
$$
V=(n2^n+2)c_n.
$$
Define the rational threshold
$$
\rho
=
\alpha\left(\frac{c_1}{2}+\sum_{i=2}^n c_i\right)
+
V\left(\frac{\alpha}{2}-a\right),
\qquad
a=\frac{\alpha}{2^n}.
$$
Let terminal revenue be
$$
\operatorname{Rev}(\pi)=\sum_{t,k,p}p\,\pi_{t,k,p}.
$$
All triggers pay zero, so this is also type zero’s terminal revenue.
I prove the exact equivalence
$$
\text{Equal-Subset-Sum is a yes-instance}
\quad\Longleftrightarrow\quad
\operatorname{Rev}(\pi)<\rho.
$$
If the original weights have distinct subset sums, adding the gap $W+1$ preserves that property. A sum containing $W+1$ is greater than every sum of the original weights; sums on the same side reduce to original subset sums.
Every prefix of the price-gap list therefore has distinct subset sums. Section 4 proves inductively that no merge occurs and that stage $i$ produces $2^i$ equal-mass cohorts.
The mean goods count after stage $i$ is $i-1/2$. Hence allocation and revenue before $V$ are
$$
X_{\mathrm{pre}}=\alpha\left(n-\frac12\right)
$$
and
$$
R_{\mathrm{pre}}
=
\alpha\left(\frac{c_1}{2}+\sum_{i=2}^n c_i\right).
$$
At that time, half the type-zero population has $n-1$ goods and half has $n$ goods. Each cohort has mass $a$.
At price $V$, lexicographic valuation processing first selects a cohort with $n-1$ goods. Its exit removes bound $a=D_n$, making the deficit zero. The ensuing sweep gives every other uncapped cohort its last good. Later updates remove only zero transaction bounds.
The terminal allocation is consequently
$$
X_{\mathrm{term}}=\alpha n-a.
$$
The definition of $\alpha$ gives
$$
n=\alpha(2n-2^{-n}),
$$
so
$$
G=n(1-\alpha)=\alpha n-a.
$$
Thus purchases at $V$ total
$$
X_{\mathrm{term}}-X_{\mathrm{pre}}
=\frac{\alpha}{2}-a.
$$
Therefore
$$
\operatorname{Rev}(\pi)
=
R_{\mathrm{pre}}
+
V\left(\frac{\alpha}{2}-a\right)
=\rho.
$$
Suppose the original weights have a subset-sum collision. A type-zero merge must occur by stage $N+1=n-1$.
To see this, if a merge has already occurred there is nothing to prove. Otherwise all $2^{N+1}$ histories exist at stage $N+1$. Choose equal-sum subsets of $w_1,\ldots,w_N$ and give the corresponding histories the same last bit. The payment formula in Section 4 makes their states identical, so they merge.
Lemma 3 therefore gives
$$
X_{\mathrm{pre}}
\ge
\alpha\left(n-\frac12\right)+a.
$$
Before $V$, each type-zero person buys at most $n$ goods, each at price at most $c_n$. Thus
$$
R_{\mathrm{pre}}\le \alpha n c_n.
$$
Feasibility always gives $X_{\mathrm{term}}\le G$. All subsequent purchases occur at $V$, so
$$
\operatorname{Rev}(\pi)
=
R_{\mathrm{pre}}+V(X_{\mathrm{term}}-X_{\mathrm{pre}})
\le
\alpha n c_n
+
V\left(\frac{\alpha}{2}-2a\right).
$$
Our choice of $V$ ensures
$$
Va
=
(n2^n+2)c_n\frac{\alpha}{2^n}
=
\alpha n c_n+2ac_n
>
\alpha n c_n.
$$
Consequently,
$$
\operatorname{Rev}(\pi)
<
V\left(\frac{\alpha}{2}-a\right)
\le \rho.
$$
This completes the many-one reduction to the terminal-revenue decision problem.
Put
$$
H=2n2^n-1.
$$
The masses have the explicit representations
$$
\mu_0=\frac{n2^n}{H},\qquad
\mu_1=\frac{2^{n-1}}{H},
$$
and, for $i\ge 2$,
$$
\mu_i=\frac{2^{n-i}(2n-2i+5)}{H}.
$$
Their numerators and denominators have $O(n+\log n)$ bits.
The prices, valuations and budgets have $O(n+\log n+\log W)$ bits. The threshold $\rho$ has polynomial bit length. Therefore the reduction constructs an instance with
$$
m=n(n+1),\qquad \tau=n+1,
$$
and $L$ polynomial in the source encoding length.
The rank description is simply
$$
F_\mu(S)=\min\{G,n\mu(S)\}.
$$
It is evaluated by rational summation and comparison in polynomial time. Every answer has denominator dividing $H$ and numerator at most $nH$, so its bit length is polynomial as required.
Initially every cohort mass is an integer multiple of $1/H$. This property persists.
Indeed, when it holds, $b_C$, $U$, $s$, $D$ and $r_C$ are integer multiples of $1/H$. The two child masses are
$$
r_C-q a_C
\quad\text{and}\quad
a_C-(r_C-q a_C),
$$
so they have the same property. Merging also preserves it.
All event prices are integers, so all per-person payments are integers, bounded by $nV$. Hence terminal revenue has denominator dividing $H$ and numerator at most $nVH$, a polynomial-bit quantity.
The execution also terminates: each valuation update removes at least $1/H$ of active population mass, and sweeps never reactivate inactive people.
Thus exact terminal-revenue computation is NP-hard even when its output is polynomially short.
Let $A$ be the auction-instance map above. Given the original weights and the explicitly returned table $Y$, let the decoder:
The decoder is polynomial-time in the combined encoding length of the weights and table. Exact rational summation has polynomial bit complexity in that length. Section 5 proves its correctness.
This is a polynomial-time metric reduction from the characteristic function of Equal-Subset-Sum to the explicit terminal-table function. Since Equal-Subset-Sum is NP-complete, the latter function is NP-hard under the stated convention.
For completeness, the output-size obstruction from the notes follows from the same family and can be proved independently of the hardness reduction.
Take
$$
c_i=2^i-1,\qquad V=2^n.
$$
The price gaps are $2,4,\ldots,2^{n-1}$, whose subset sums are distinct. Thus stage $n$ produces exactly $2^n$ type-zero cohorts of mass
$$
a=\frac{\alpha}{2^n}.
$$
Write
$$
A=\sum_{h=2}^n c_h,\qquad
S(z)=\sum_{h=1}^{n-1}2^h z_h.
$$
The pre-final payment formula is
$$
p_n=A+c_nz_n-S(z).
$$
As proved in the no-instance analysis, one cohort with $z_n=0$ exits first at $V$ and keeps $n-1$ goods. Every other such cohort buys one last good; cohorts with $z_n=1$ are already capped.
The terminal payments of capped cohorts are therefore
$$
A+V-S(z)
$$
for the former family, and
$$
A+V-1-S(z)
$$
for the latter.
Within each family, payments are distinct by uniqueness of binary expansion. Between the families, payments have opposite parity because every $S(z)$ is even. The first exiting cohort has a different goods count from every capped cohort.
Hence type zero contributes exactly $2^n$ nonzero terminal-table entries. In this family,
$$
m=n(n+1),\qquad \tau=n+1,\qquad L=O(n^2).
$$
Explicitly writing the table therefore cannot take time polynomial in $m,\tau,L$, regardless of the efficiency of oracle access.
The explicit terminal-table function is NP-hard under the stated polynomial-time metric reductions, and its output can be exponentially large. The terminal-revenue decision problem has conventional many-one NP-hardness even though the relevant revenue is a single polynomial-bit rational.
The proof does not classify access models that return only one specified table entry, or arbitrary succinct representations of the table. It also does not establish a separate lower bound on the number of value-oracle calls.
⟨structured verdict parsed — rendered above⟩
The claimed hardness result is correct under the explicitly stated output convention. The reduction establishes conventional many-one NP-hardness for the terminal-revenue decision problem and metric-reduction NP-hardness for the explicitly listed terminal table. The separate exponential-output construction also checks out.
I found no major or minor mathematical issues requiring repair.
The prover explicitly interprets the terminal table as a list of all nonzero entries. This is a natural interpretation of the requested exact table, and the limitation is stated clearly.
The metric reduction permits decoding time polynomial in the combined length of the source instance and returned table. This agrees with the [cited definition of metric reductions](https://drops.dagstuhl.de/storage/00lipics/lipics-vol365-icdt2026/html/LIPIcs.ICDT.2026.12/LIPIcs.ICDT.2026.12.html). Consequently, the table-hardness claim does not imply that its decoder runs in polynomial time in the original instance when the table is exponentially long. The prover correctly acknowledges this distinction.
The scalar revenue decision problem avoids that output-length qualification.
All required auction hypotheses are satisfied.
For the rank
$$
F_\mu(S)=\min\{G,n\mu(S)\},
$$
the stated marginal formula is exact. Its decrease as $S$ increases establishes diminishing returns and hence submodularity. Normalization, monotonicity, and the singleton cap bounds also follow directly.
The redundancy condition is correctly checked: $n\mu_t\le D_0$ implies
$$
n\sum_{s\ne t}\mu_s\ge n-D_0=G.
$$
Therefore removing any one type leaves the full rank unchanged.
The final expression for the rank in terms of population masses also verifies linear scaling under common population rescaling.
Finding: The construction is admissible for the precise model in USER_TASK.
The simplification of the transaction region is valid.
The cohort bounds imply every type-set capacity bound involving $n\mu(S)$, because allocated goods plus available additional transactions for each person never exceed cap $n$. The total constraint provides the remaining supply bound $s=G-X$. Conversely, these bounds imply every original truncated-rank constraint.
Thus the region is exactly the stated box intersected with a total-supply constraint.
The projection argument is also correct. At $y_C=0$, the other coordinates have their original coordinate bounds and total bound $\min\{s,U-b_C\}$. At $y_C=r$, only the total bound changes, to $s-r$. Equality of the entire projections is therefore characterized by the inequalities written in the proof.
Solving them gives
$$
r_C=\min\{b_C,\max\{0,b_C-D\}\}.
$$
For $D\ge0$, this reduces correctly to $\max\{0,b_C-D\}$.
Finding: Both the region description and maximal clinching formula are proved.
The identity
$$
\min(d_C-j,n-k_C-j)=\min(d_C,n-k_C)-j
$$
is valid for every permitted child increment. The floor-and-ceiling split respects demand and cap because their minimum is integral and bounds the average increment.
Weighting over the children gives a reduction of exactly $r_C$ in $U$. Allocation increases by $r_C$, so $s$ also decreases by $r_C$. Hence $D$ is preserved.
For $D\ge0$, the combined child bound is indeed $\min\{b_C,D\}$.
The budget argument is sound. Every event price is at most $V$, each person receives at most $n$ goods, and demand never exceeds $n+1$. The displayed lower bound on the budget breakpoint is strictly greater than $V$. Consequently, no budget-equality update occurs.
Until valuation exit, type-zero demand remains $n+1-k_C$, including for capped people, whose demand remains positive but whose transaction bound is zero.
Finding: The invariant and event simplification are valid.
The induction that trigger types remain unallocated is correct. At each earlier sweep, a future trigger has bound
$$
A_j=D_{j-1}-D_j\le D_i,
$$
so its clinch is zero. Its eventual valuation exit therefore removes exactly $A_j$ from $U$, with no allocation change.
The deficit after trigger exit $i$ is consequently $D_i$, including when type-zero cohorts have merged.
Under the no-prior-merge hypothesis, the stage calculations check out:
These calculations respect the rule that newly created children are not visited during the same sweep.
The payment formula correctly follows from the stated purchase increments. With the last bit fixed, payment equality is exactly equality of subset sums of the price gaps. Such histories also have identical goods counts and demands, so the prescribed merge occurs. Different last bits have different goods counts and cannot merge.
Finding: The history analysis correctly identifies the source of merging.
This lemma correctly avoids assuming that the unmerged history formula survives a merge.
At stage $n$, each visited type-zero parent leaves children with combined bound at most $D_n=a$. Summing over the $P$ original parents and subsequently merging gives $U_0\le Pa$.
Every parent produces at most two children. Once a merge reduces the cohort count below the doubling maximum, later stages cannot restore that maximum. Thus a merge by stage $n-1$ implies
$$
P\le2^{n-1}-1.
$$
Because all triggers are unallocated and type-zero demand exceeds remaining cap by one,
$$
U_0=\alpha n-X_{\mathrm{pre}}.
$$
The resulting allocation lower bound, including its additive term $a$, is arithmetically correct.
Finding: The required quantitative consequence of an earlier merge is established.
The source problem is appropriate. The [cited Equal-Subset-Sum paper](https://arxiv.org/html/1905.02424v2) states NP-completeness and provides the positive-integer formulation. Positivity also justifies the prover’s equivalence between distinct equal-sum subsets and disjoint nonempty equal-sum subsets.
The price construction gives exactly $c_n=2W+2$. Appending gap $W+1$ preserves uniqueness of subset sums in a no-instance.
Every prefix has distinct subset sums, so no merge occurs. The cohort counts, equal masses, mean goods counts, and pre-final revenue follow correctly from the history calculation.
At price $V$, lexicographic valuation processing first removes a type-zero cohort with $n-1$ goods. Its transaction bound is $a=D_n$, so the deficit becomes zero. The ensuing sweep gives every other uncapped cohort its remaining good. Later valuation updates remove only zero transaction bounds.
The resulting terminal allocation is $\alpha n-a$. The identity
$$
G=\alpha n-a
$$
is correct, as is the final purchase quantity $\alpha/2-a$. Hence terminal revenue equals $\rho$.
A collision among the original weights forces a merge by stage $N+1=n-1$, unless a merge has already occurred. This uses the payment formula only up to the first merge, where it remains valid.
Lemma 3 then supplies the required larger pre-final allocation. The bounds
$$
R_{\mathrm{pre}}\le\alpha n c_n,
\qquad
X_{\mathrm{term}}\le G
$$
are valid independently of the subsequent merging pattern or final valuation order.
The decisive constant check is correct:
$$
Va=\alpha n c_n+2ac_n>\alpha n c_n.
$$
It yields terminal revenue strictly below $\rho$.
Finding: The stated equivalence is proved, establishing many-one NP-hardness of the terminal-revenue decision problem.
The explicit mass representations are correct. Their bit lengths, and those of prices, valuations, budgets, and $\rho$, are polynomial in the source encoding length.
The rank has a polynomial-size description and polynomial-time evaluation. Its answers have denominator dividing $H$ and the claimed polynomial bit-length bound.
The mass-lattice argument is valid. The displayed child-mass formulas preserve integer multiples of $1/H$, as do merging and all transaction calculations. Integer event prices imply integer per-person payments bounded by $nV$. Terminal revenue therefore has polynomial bit length.
Termination follows as stated: each valuation update removes at least $1/H$ of active mass, and sweeps never reactivate inactive people.
Computing revenue from an explicit terminal table requires polynomial time in that table’s encoding length. The decoder consequently satisfies the stated metric-reduction convention.
Finding: The encoding requirements and function reduction are established.
For $c_i=2^i-1$, the price gaps have unique subset sums, so the unmerged construction produces $2^n$ histories.
The final payment expressions are correct. Payments are distinct within each capped family, and the two families have opposite parity. The single cohort retaining $n-1$ goods is distinguished by its goods count. Hence there are exactly $2^n$ nonzero type-zero terminal entries.
The bounds $m=n(n+1)$, $\tau=n+1$, and $L=O(n^2)$ establish a superpolynomial explicit-output requirement.
The prover correctly limits its conclusions: it does not classify individual-entry queries, arbitrary succinct representations, or oracle-call complexity separately.
Repair feedback: None required. The argument resolves the exact explicit-table problem under its stated reduction convention.
⟨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.