Answer: —
Theorem B.1 — class: algorithmic
Given finite good classes \(H\), rational per-capita supplies \(\rho_h\), a finite catalogue \(T\) of complete XOS valuation types with finite rational descriptions and distribution \(\mu\), a finite-description periodic priority schedule including a tagged position, and a threshold \(R\), run the paper’s mechanism on sufficiently divisible \(N\)-copy instances with \(N\mu_t\) agents of type \(t\) and \(N\rho_h\) goods of class \(h\). Decide whether \(\limsup_{N\to\infty} U_{t\to w}^{(N)}/U_t^{(N)}\le R\) for every type \(t\) and finite-description XOS report \(w\), using \(+\infty\) when truthful utility is zero and deviating utility is positive; otherwise output a violating \(t,w\).
A society is given by its support: the list of the \(\tau\) types with positive mass, each mass a binary rational. Here \(T\) is that support, \(\sum_{t\in T}\mu_t=1\), and \(\tau=|T|\) is the support size, not the number of possible types.
Let \(H\) be an ordered set of \(m\ge1\) good classes, with binary-rational supplies \(\rho_h>0\) satisfying \(\sum_h\rho_h\ge1\). Each type has an explicit nonempty list of nonnegative rational XOS clauses: on a bundle with count vector \(x\in\mathbb Z_{\ge0}^{H}\), its value is \(v_t(x)=\max_{k\le K_t}\sum_h a_{t,k,h}x_h\). Every copy of a class has the same clause coefficients; valuations are normalized and monotone.
The priority schedule is an explicit word \(p\in T^q\), with \(|\{j:p_j=t\}|=q\mu_t\), and a designated position \(j_t\) satisfying \(p_{j_t}=t\) for each supported type. For every sufficiently large \(N\) with \(q\mid N\) and all \(N\rho_h\) integral, create \(N\) distinct agents in the order obtained by repeating \(p\), and \(N\rho_h\) goods of class \(h\). The tagged agent of type \(t\) is at position \(j_t\) in the first repetition.
Start every bundle empty. Repeatedly traverse this fixed agent order, giving each agent one remaining good maximizing its reported marginal value relative to its own current bundle. Break ties by class order and then copy index; allocate even zero-marginal goods, and stop immediately when no goods remain.
A deviation changes only the tagged agent's report to an arbitrary finite explicit list of nonnegative rational XOS clauses over the same classes, fixed independently of \(N\). All other agents report truthfully. Let \(U_t^{(N)}\) and \(U_{t\to w}^{(N)}\) be that agent's final utilities evaluated using \(v_t\), respectively under truthful reporting and report \(w\). Interpret a positive numerator over zero as \(+\infty\), and \(0/0\) as \(1\); take limits only over the admissible \(N\).
Given a binary-rational threshold \(R\ge1\), the limiting incentive-ratio threshold problem asks whether \(\limsup_{N\to\infty}U_{t\to w}^{(N)}/U_t^{(N)}\le R\) for every \(t\in T\) and every such report \(w\); a violation is a pair \(t,w\) for which this inequality fails.
Is this limiting incentive-ratio threshold problem in \(\mathrm P\), or is it \(\mathrm{NP}\)-hard? State running times in \(m,\tau,q,K,L\), where \(K=\max_t K_t\) and \(L\) is the total binary input length.
For discrete societies with \(n\ge2\) agents and \(M\ge n\) goods, marginal-value Round-Robin has sharp worst-case incentive ratio \(\lceil M/n\rceil\) for XOS valuations. [Verified discrete result](https://arxiv.org/html/2306.15920v2#A2)
No result settling the exact replicated-society threshold problem defined above was located.
The unrestricted $\mathrm P$ versus $\mathrm{NP}$-hard classification remains unresolved here.
I prove three additional structural and algorithmic results:
$$
\tau\,m^B B^{2m+1}q^{2m+1}2^{O(m^3)}
\operatorname{poly}(m,q,K,L).
$$
Consequently, the problem is polynomial-time solvable when both $m$ and $B$ are fixed constants.
The finite search preserves exact exhaustion positions and finite residual stocks; it does not replace the mechanism by a continuum approximation.
Put
$$
S=\sum_{h\in H}\rho_h,\qquad B=\lceil S\rceil,\qquad
\lambda=S-B+1.
$$
The hypotheses imply $0<\lambda\le1$.
There are exactly $NS$ allocations: every remaining good is allocated, including goods with zero marginal value. Thus there are $B-1$ complete traversals followed by a prefix of length
$$
E(N)=N\lambda.
$$
When $S$ is integral, this last prefix is a complete traversal.
Because $j_t\le q$ is fixed and $\lambda>0$, every tagged agent receives exactly $B$ goods for all sufficiently large admissible $N$. This conclusion is independent of the report.
For a supported type $t$, define
$$
A_t=\max_{k,h}a_{t,k,h}=\max_h v_t(e_h).
$$
For sufficiently large $N$, all classes remain available at its first turn: fewer than $q$ preceding allocations cannot exhaust a stock $N\rho_h$ tending to infinity. Truthful reporting therefore obtains a first good worth $A_t$. By monotonicity,
$$
U_t^{(N)}\ge A_t.
$$
Every bundle $x$ with $B$ goods satisfies
$$
v_t(x)
=\max_k\sum_h a_{t,k,h}x_h
\le A_t\sum_hx_h
=BA_t.
$$
Consequently, if $A_t>0$, every eventual ratio is at most $B$. If $A_t=0$, nonnegativity implies that every true coefficient is zero, so the ratio is always $1$ under the prescribed convention.
This proves the universal bound
$$
\sup_{t,w}\limsup_{N\to\infty}
\frac{U_{t\to w}^{(N)}}{U_t^{(N)}}\le B.
$$
In particular, $R\ge B$ is a sufficient YES-condition, checkable in $O(L+mL^2)$ bit operations using schoolbook rational arithmetic.
For later use, define the finite set
$$
\mathcal X_B=
\left\{x\in\mathbb Z_{\ge0}^{H}:\sum_hx_h=B\right\}.
$$
For fixed $t$, every sufficiently large truthful or deviating utility belongs to
$$
\{v_t(x):x\in\mathcal X_B\}.
$$
Thus every fixed report produces a ratio sequence taking values in a finite set, after finitely many initial terms. Its limit superior is a value occurring infinitely often. This observation does not assert eventual constancy.
Lemma 1. Suppose an agent starts empty with every class available. Under any allowed XOS report, it keeps selecting its first chosen class for as long as that class remains available.
Proof. Write the report as
$$
w(x)=\max_\ell b_\ell\cdot x,
\qquad
A=\max_{\ell,h}b_{\ell,h}.
$$
Let $c$ be the first chosen class. Then $w(e_c)=A$, and some clause has coefficient $A$ on $c$. Hence
$$
w(ne_c)=nA
$$
for every nonnegative integer $n$.
For every class $h$,
$$
w(ne_c+e_h)\le(n+1)A=w((n+1)e_c).
$$
Thus $c$ is a marginal maximizer.
Suppose an earlier class $h$ tied with $c$. For $n>0$, equality would require a clause with coefficient $A$ on both $c$ and $h$, because all coefficients are at most $A$. Consequently $w(e_h)=A$. For $n=0$, the same conclusion follows directly from the tie. In either case, the initial tie rule would have chosen $h$ before $c$, a contradiction. Therefore $c$ continues to be chosen. $\square$
The next result shows that, once this first class disappears, there is no analogous restriction on a finite prescribed sequence of choices.
Lemma 2. Fix a class $c$, an integer $d\ge1$, and a word
$$
h_1,\ldots,h_\ell\in H\setminus\{c\}.
$$
There is a nonnegative rational XOS report with $\ell+1$ clauses having the following behavior:
Every coefficient lies in $[0,1]$ and has
$$
O(\log(d+\ell+1))
$$
bits.
Proof. If $\ell=0$, use $w(x)=x_c$. Assume $\ell\ge1$, and set
$$
\eta=\frac{1}{16(\ell+1)^2},
\qquad
\varepsilon=\frac{\eta}{8(\ell+1)},
\qquad
C=d-\frac14.
$$
Include the clause $x_c$. For each $r\in\{1,\ldots,\ell\}$, include the clause with coefficients
$$
b_{r,c}=\frac{C-\eta r^2/2}{d},
$$
and, for $h\ne c$,
$$
b_{r,h}=\frac12+\eta r+\varepsilon\mathbf1_{\{h=h_r\}}.
$$
These coefficients are nonnegative and strictly less than $1$. Indeed,
$$
0<\frac{d-\frac14-\frac1{32}}{d}
<b_{r,c}<1,
$$
while
$$
b_{r,h}\le\frac12+\frac1{16}+\frac1{128}<1.
$$
Their numerators and denominators have the asserted bit length.
At a bundle $ne_c$, the clause $x_c$ gives value $n$. At a candidate bundle $(n+1)e_c$, it gives $n+1$, whereas every other candidate $ne_c+e_h$, with $h\ne c$, has value strictly below $n+1$. Thus $c$ is selected whenever it remains available during this initial phase.
Now suppose $c$ is unavailable and the bundle contains exactly $d$ copies of $c$ and $u-1$ other goods, where $1\le u\le\ell$. For any candidate next good, let $y$ be the resulting bundle. Its total count outside $c$ is $u$. The value of clause $r$ at $y$ is
$$
C+\frac u2+\eta\left(ru-\frac{r^2}{2}\right)
+\varepsilon y_{h_r}.
$$
The difference between the terms excluding $\varepsilon$, for clauses $u$ and $r$, is
$$
\frac{\eta}{2}(u-r)^2.
$$
For $r\ne u$, this is at least $\eta/2$. The perturbation can reduce the difference by at most
$$
\varepsilon u\le\varepsilon\ell<\frac{\eta}{8}.
$$
Hence clause $u$ strictly dominates all the other scripted clauses at every candidate bundle.
It also dominates the original clause $x_c$: its value is at least
$$
C+\frac u2+\frac{\eta u^2}{2}
\ge d+\frac14>d.
$$
Therefore clause $u$ determines the value of every candidate next bundle. Among available classes, its coefficient on $h_u$ is uniquely largest. If $h_u$ is available, it is selected. $\square$
Notice that the proof works for every distribution of the previously acquired goods outside $c$. The report uses the number of subsequent turns as a clock.
For a word
$$
s=(s_1,\ldots,s_B)\in H^B,
$$
let $c=s_1$ and let $d$ be the length of its initial run of $c$. Retain only words in which $c$ never appears after that initial run. Associate to each retained word the report from Lemma 2, using the suffix
$$
s_{d+1},\ldots,s_B.
$$
Call this its *canonical report*. There are at most $m^B$ such reports.
Theorem 3. A limiting violation exists if and only if one exists using a canonical report. Moreover, the supremum of all limiting incentive ratios is a finite rational number attained by a canonical report for some supported type.
Proof. Canonical reports are allowed reports, so one implication is immediate.
Fix a type $t$ and an arbitrary report $w$. For sufficiently large $N$, record both the tagged agent’s deviating word and its truthful word, each of length $B$. There are only finitely many pairs of words.
By Section 1, the limiting ratio is a value recurring infinitely often. Choose an infinite subsequence on which a fixed pair of words attains this value. Let the deviating word begin with $d$ copies of class $c$.
Lemma 1 implies that $c$ cannot occur after this initial run: the first different choice is possible only after $c$ has exhausted, and exhausted classes never return. Thus the word has a canonical report.
On each sufficiently large $N$ in the chosen subsequence, replacing $w$ by that canonical report reproduces the entire allocation. To verify this, induct on chronological allocation turns. Untagged agents have unchanged reports. At tagged turns, the canonical report selects $c$ while it remains available, and subsequently selects the prescribed suffix class by Lemma 2. Therefore the stocks and all previous bundles agree at every turn.
The canonical report consequently attains the original limiting ratio on an infinite subsequence, so its own limit superior is at least that ratio.
The canonical family is finite. Taking its maximum therefore gives an attained upper bound on every allowed report, and this maximum is itself attained by an allowed report. Finiteness and rationality follow from Section 1. $\square$
Since $\ell=B-d$, each witnessing report has
$$
\ell+1=B-d+1\le B
$$
clauses and coefficient bit length $O(\log(B+1))$. Its explicit description has length
$$
O\!\left(mB\log(B+1)\right).
$$
This removes the unbounded report quantifier, but $B$ can be exponentially large in $L$.
The following result is independent of the canonical-report construction.
Lemma 4. Fix a nonempty available set $A$ and an XOS valuation with $k$ clauses. Along consecutive turns during which $A$ remains unchanged, the agent changes its chosen class at most $k-1$ times.
Proof. For each clause $\ell$, define
$$
b_\ell=\max_{h\in A}a_{\ell,h},
$$
and let $c_\ell$ be the earliest class attaining this maximum. At bundle $x$, put
$$
s_\ell(x)=a_\ell\cdot x+b_\ell.
$$
Maximizing marginal value is equivalent to maximizing $v(x+e_h)$, because $v(x)$ is independent of $h$. Consequently, the chosen class is the earliest $c_\ell$ among clauses maximizing $s_\ell(x)$.
Suppose the current chosen class is $c$. Among maximizing clauses with $c_\ell=c$, select one, denoted $k_0$, with largest $b_\ell$. Write $b=b_{k_0}$ and $M=s_{k_0}(x)$.
After selecting $c$, for any clause $\ell$ with $b_\ell\le b$,
$$
s_\ell(x+e_c)
=s_\ell(x)+a_{\ell,c}
\le M+b_\ell
\le M+b
=s_{k_0}(x+e_c).
$$
Equality requires
$$
s_\ell(x)=M,\qquad a_{\ell,c}=b_\ell=b.
$$
Then $c$ maximizes clause $\ell$’s coefficients on $A$, so $c_\ell\le c$. Since clause $\ell$ was already maximizing at $x$ and the mechanism selected $c$, the tie rule also gives $c_\ell\ge c$. Thus $c_\ell=c$.
It follows that the selected clause coefficient $b$ can never decrease from one turn to the next, and must strictly increase whenever the chosen class changes. There are at most $k$ possible values $b_\ell$. Hence at most $k-1$ class changes occur. $\square$
An execution has at most $m$ nonempty availability phases. There are at most $m-1$ transitions between phases. Applying Lemma 4 within each phase gives the total bound
$$
m(K_t-1)+(m-1)=mK_t-1
$$
on class changes for a truthful agent. Equivalently, its allocation word has at most $mK_t$ maximal constant runs.
This bound does not yet yield a polynomial algorithm for the threshold problem, because arbitrary deviations can use the much larger canonical family.
I now give a finite decision procedure that retains all exhaustion-boundary effects.
Let $D$ be the least common multiple of $q$ and the reduced denominators of the supplies. The admissible population sizes are exactly
$$
N=Dn,\qquad n\in\mathbb Z_{\ge1}.
$$
Both $D$ and $B$ have $O(L)$ bits.
Fix a tagged type $t$ and a canonical word. Encode two executions at the same $N$: the truthful execution and the execution with its canonical report.
For each execution and each class $h$, introduce:
The allocation at $(r_h,b_h)$ is the last allocation of class $h$.
An ordinary turn $(r,i)$ therefore has class $h$ available precisely when
$$
r<r_h
\quad\text{or}\quad
(r=r_h\text{ and }i\le b_h).
$$
It is an active allocation turn precisely when
$$
r<B
\quad\text{or}\quad
(r=B\text{ and }i\le E),
\qquad E=N\lambda.
$$
We enumerate the finite choices of exhaustion traversals. Within each execution, we also enumerate a weak ordering of the named positions
$$
b_1,\ldots,b_m,E,j_t,
$$
including possible equalities, and their residues modulo $q$. The residue of $E$ is shared between the two executions.
Write
$$
b_h=qz_h+s_h,\qquad E=qz_E+s_E,
\qquad 0\le s_h,s_E<q.
$$
Once residues have been enumerated, the integer variables are
$$
n,\quad z_E,\quad
z_1^{\mathrm{truth}},\ldots,z_m^{\mathrm{truth}},
\quad
z_1^{\mathrm{dev}},\ldots,z_m^{\mathrm{dev}}.
$$
There are $2m+2$ variables.
Ordering conditions, position bounds, and $E=D\lambda n$ are integer linear constraints.
We additionally impose
$$
Dn\ge q,\qquad D\rho_h n\ge q+1\ \text{for every }h,
\qquad E\ge q.
$$
These conditions hold for every sufficiently large admissible $N$. They ensure that all tagged agents receive $B$ goods and have every class available at their first turn.
In either execution, split the agent positions into:
There are at most $m+2$ singletons and $m+3$ intervals.
Within an interval, agents with the same residue modulo $q$ have the same type and the same availability pattern at every traversal. Their bundle histories are therefore identical. The tagged agent is isolated at its singleton $j_t$.
For example, the number of positions of residue $a$, where $1\le a\le q$, in an interval $(u,v)$ is
$$
\left\lfloor\frac{v-1-a}{q}\right\rfloor
-
\left\lfloor\frac{u-a}{q}\right\rfloor.
$$
Because endpoint residues have been fixed, this is an affine integer expression in the variables. The final interval uses
$$
\left\lfloor\frac{N-a}{q}\right\rfloor
-
\left\lfloor\frac{u-a}{q}\right\rfloor.
$$
For every interval-residue cohort and every singleton, simulate its bundle through the $B$ traversals using the branch’s availability pattern. Truthful choices are computed directly from the input clauses. The deviating tagged agent follows its prescribed word; a branch is rejected if the requested class is unavailable or the word violates its initial commitment.
If an interval-residue cohort has an active turn with no available class, impose that its population count is zero. Such a cohort then contributes nothing. A singleton with this defect rejects the branch.
Thus every nonempty cohort has a completely determined, constant final count vector.
For each execution and class $h$, impose
$$
\sum_C \operatorname{count}(C)\,x_{C,h}=D\rho_h n,
$$
where $C$ ranges over its cohorts and $x_C$ is the final bundle computed for that cohort.
These are linear equations: each $x_{C,h}$ is constant within the branch, and every cohort population is affine in the integer variables.
Finally, require that the singleton turn $(r_h,b_h)$ is active and actually selects class $h$. Distinct classes cannot exhaust at the same allocation turn.
Lemma 5. Integer solutions of these constraints correspond exactly to executions having the branch’s stated exhaustion data and tagged behavior.
Proof. Every actual execution with these branch data satisfies the constraints, by counting its allocations.
Conversely, consider an integer solution and the simulated allocation sequence. No simulated allocation of class $h$ occurs after $(r_h,b_h)$, and that designated turn allocates $h$. The supply equality says that the total simulated number of $h$-allocations is exactly its stock.
Before its designated exhaustion allocation, therefore, fewer than all copies of $h$ have been consumed: the designated allocation itself is still to come. After that allocation, exactly all copies have been consumed. Thus the stipulated availability pattern is correct at every chronological turn.
Induction over turns now establishes that every simulated truthful choice is the actual marginal-maximizing choice. Lemma 2 establishes the same correspondence for the canonical report. The active turns number
$$
(B-1)N+E=NS,
$$
so the mechanism stops exactly where stipulated. $\square$
In particular, constant residual stocks are preserved by the affine counting equations.
Within a combined branch, the tagged truthful and deviating bundles are fixed vectors. Let their true utilities be $V$ and $W$.
A branch can witness a violation precisely when
$$
W>RV
$$
and its integer solutions have unbounded $n$. This comparison respects the prescribed zero conventions: if $V=W=0$, it is false, as required for $R\ge1$.
Write the branch constraints as a rational polyhedron
$$
P=\{x:Ax\le b\},
$$
with integer variables $x$ and distinguished coordinate $n$.
Lemma 6. The integer solutions in $P$ have unbounded $n$ if and only if both systems below have integer solutions:
$$
Ax\le b
$$
and
$$
A\delta\le0,\qquad \delta_n\ge1.
$$
Proof. If both have integer solutions $x_0$ and $\delta$, then
$$
x_0+k\delta\in P
$$
for every nonnegative integer $k$, and its $n$ coordinate tends to infinity.
For the converse, take integer solutions $x_j$ with $n_j\to\infty$. Every remaining variable is a quotient of a position between $1$ and $Dn_j$, so its ratio to $n_j$ is bounded. Pass to a convergent subsequence of $x_j/n_j$, with limit $\gamma$. Dividing the inequalities by $n_j$ gives
$$
A\gamma\le0,\qquad \gamma_n=1.
$$
A nonempty system of rational linear inequalities has a rational solution; this follows, for example, by Fourier–Motzkin elimination and choosing rational values between the resulting rational bounds. Hence the homogeneous system with distinguished coordinate $1$ has a rational solution. Clearing denominators gives an integer $\delta$ with $A\delta\le0$ and $\delta_n\ge1$. $\square$
We use the standard fixed-dimension integer-programming theorem: integer feasibility with $d$ variables and encoding length $\ell$ is decidable in
$$
2^{O(d^3)}\operatorname{poly}(\ell)
$$
time. The theorem applies to general linear inequality systems, including unbounded feasible regions. See [Lenstra’s original paper](https://pub.math.leidenuniv.nl/~lenstrahw/PUBLICATIONS/1983i/art.pdf) and the running-time statement in [Kannan’s paper](https://doi.org/10.1145/800061.808749).
Here $d=2m+2$. All constraints have integer coefficients after clearing denominators, and polynomial encoding length in $m,q,L$. Thus Lemma 6 is tested by two such integer-feasibility calls.
The algorithm enumerates supported types, canonical words, and the combined execution branches above. It returns NO exactly when a branch with $W>RV$ has unbounded integer solutions.
If it returns NO, Lemmas 5 and 6 provide arbitrarily large admissible $N$ with the same canonical report and ratio exceeding $R$. This is a limiting violation.
Conversely, suppose a limiting violation exists. Theorem 3 supplies a canonical witnessing report. There are finitely many pairs of tagged words and finitely many exhaustion branches. On an infinite subsequence, the words, exhaustion traversals, position orderings, and residues are all fixed. The corresponding branch has $W>RV$ and unbounded integer solutions, so the algorithm finds it.
An upper bound on the number of branches is
$$
\tau\,m^B B^{2m}
q^{2m+1}(m+2)^{2m+4}.
$$
The factors respectively account for the type, canonical word, exhaustion traversals, residues, and two weak orderings.
A branch has $O(qm)$ cohorts. Direct simulation costs
$$
O\!\left(B(q+1)(m+3)KmL^2\right)
$$
bit operations: at each turn, all candidate marginal maximizers can be evaluated in $O(Km)$ arithmetic operations. Bundle counts and all resulting coefficients have $O(L+\log B)=O(L)$ bits.
Including the two integer-feasibility tests yields the valid overall bound
$$
\tau\,m^B B^{2m+1}q^{2m+1}2^{O(m^3)}
\operatorname{poly}(m,q,K,L).
$$
Since $B\le2^{O(L)}$, this is at most
$$
2^{\,2^{O(L)}}.
$$
For fixed $m$ and fixed $B$, the displayed bound is polynomial in $\tau,q,K,L$. This proves an exact polynomial-time special case extending to any fixed number of classes when total supply is also bounded.
The canonical-report theorem resolves one obstacle identified in the notes: arbitrary finite reports can be replaced by a finite, explicitly bounded family. The exhaustion encoding resolves another: finite residual stocks can be handled exactly.
The remaining obstacle is computational. Enumerating allocation words costs $m^B$, and the exhaustion encoding also branches exponentially with the number of classes. I have not proved that these searches can be replaced by a polynomial algorithm, nor constructed a hardness reduction for the specified threshold problem.
⟨structured verdict parsed — rendered above⟩
The output establishes substantial partial results, but it does not resolve the requested unrestricted $\mathrm P$ versus $\mathrm{NP}$-hard classification. I found no false central step in its structural lemmas or exact decision procedure. The main unresolved issue is the original complexity question, which the prover explicitly acknowledges.
With $S=\sum_h\rho_h$, $B=\lceil S\rceil$, and $\lambda=S-B+1$, the identity
$$
NS=(B-1)N+N\lambda
$$
correctly describes the complete traversals and final prefix. Admissibility makes $N\lambda$ integral. The integral case $S=B$ is handled correctly by $\lambda=1$.
Since $j_t\le q$ is fixed and $\lambda>0$, every tagged agent eventually receives exactly $B$ goods. Positive supplies ensure that every class is available at its first turn for sufficiently large admissible $N$.
The bounds
$$
A_t\le U_t^{(N)},\qquad U_{t\to w}^{(N)}\le BA_t
$$
follow from the first truthful allocation, monotonicity, and nonnegative clause coefficients. If $A_t=0$, every true coefficient is zero, so both utilities are zero and the ratio convention gives $1$. Thus the universal bound $B$ and the sufficient YES-condition $R\ge B$ are valid.
Every eventual tagged bundle has $B$ goods, so its true utility belongs to a finite rational set. For types with $A_t>0$, truthful denominators are positive; for types with $A_t=0$, ratios are identically $1$. Consequently, each fixed report has a finite ratio alphabet, and its limit superior is a value recurring infinitely often.
This establishes the subsequence property used later. It does not require eventual constancy.
If $c$ is chosen first, some clause has coefficient $A$ on $c$, and all coefficients are at most $A$. Hence
$$
w(ne_c)=nA,\qquad w(ne_c+e_h)\le(n+1)A.
$$
The equality analysis correctly excludes an earlier class tying with $c$: such an equality would imply that the earlier class also had singleton value $A$, contradicting the first-turn tie rule.
The argument also covers $A=0$. Once $c$ exhausts, it cannot subsequently reappear in the allocation word.
The coefficient bounds and bit-length estimate are valid. In particular,
$$
\frac{\eta r^2}{2}<\frac1{32}
$$
for $r\le\ell$, so the coefficient on $c$ remains positive and below $1$.
At a candidate bundle containing $d$ copies of $c$ and $u$ other goods, the unperturbed advantage of clause $u$ over clause $r$ is exactly
$$
\frac{\eta}{2}(u-r)^2.
$$
The perturbation can reduce this advantage by at most $\varepsilon u<\eta/8$, so clause $u$ strictly dominates every other scripted clause. Its value also exceeds $d$, excluding the original clause $x_c$.
Therefore the requested class $h_u$ is uniquely optimal whenever available. The dependence on previously acquired goods is bounded exactly as claimed. The separate case $\ell=0$ is handled.
The finite pair-of-words argument produces an infinite subsequence with fixed truthful and deviating words attaining the original limit superior.
Lemma 1 makes the deviating word eligible for the canonical construction. On that subsequence, the chronological induction is valid: unchanged preceding allocations preserve stocks and bundles, and Lemma 2 reproduces each prescribed tagged choice.
The canonical report need only have limit superior at least that of the original report. The proof uses this inequality correctly; it does not assume identical behavior outside the selected subsequence.
Taking the maximum over the finite canonical family therefore establishes an attained finite rational supremum. The bounds of at most $B$ clauses and coefficient length $O(\log(B+1))$ follow.
Maximizing the marginal is equivalent to maximizing the candidate next-bundle value. The clause scores $s_\ell(x)$ and earliest maximizing classes $c_\ell$ correctly incorporate the class tie rule.
The displayed inequality shows that a clause with $b_\ell\le b$ cannot displace the selected clause after acquiring $c$, except through an equality that retains the same chosen class. Consequently, the selected coefficient cannot decrease, and a class change requires a strict increase.
There are at most $k$ distinct coefficient values within a fixed availability phase, giving at most $k-1$ changes. There are at most $m$ nonempty phases and $m-1$ intervening transitions, yielding
$$
m(K_t-1)+(m-1)=mK_t-1.
$$
Counting phases in which the agent has no turn only overestimates this bound.
The admissible population sizes are exactly the positive multiples of the stated least common multiple $D$. Both $D$ and $B$ have $O(L)$ bits.
The availability condition correctly includes the exhaustion allocation itself. The active-turn condition also correctly handles the final prefix.
Splitting positions at all exhaustion positions, $E$, and $j_t$ makes availability and activity constant within each interval at every traversal. Agents of the same residue have the same type, and the tagged agent is isolated. Identical histories within a cohort then follow inductively.
Both population-count formulas are correct. Fixing endpoint residues makes them affine integer expressions. The large-population restrictions exclude only finitely many admissible sizes and therefore preserve the limiting question.
The stipulated rejection of words violating initial commitment is necessary: following a scripted suffix is justified only once $c$ is unavailable. That condition is included in the write-up.
The supply equalities and designated final allocation jointly establish the claimed availability pattern. Before a designated exhaustion allocation, a future allocation of that class remains, so its stock cannot already be exhausted. After it, no further allocation of that class occurs, and the total equals its supply.
This validates the chronological induction identifying simulated choices with actual choices. Requiring designated exhaustion turns to be active and to select their named classes excludes inconsistent exhaustion data.
Thus the encoding preserves finite residual stocks and exact exhaustion positions.
Within a branch, the tagged utilities are fixed. The condition
$$
W>RV
$$
correctly characterizes a ratio exceeding $R$, including the prescribed zero conventions.
An integer feasible point and an integer recession direction with positive $n$ coordinate generate arbitrarily large feasible population sizes.
Conversely, the branch position bounds ensure that all other coordinates divided by $n$ remain bounded. The normalized subsequence therefore yields a real recession vector with $n$ coordinate $1$. Rational feasibility of this rational linear system, followed by clearing denominators, supplies the integer direction asserted in the proof.
The bounded-coordinate argument is specific to these branch constraints; its hypotheses are satisfied here.
The cited integer-feasibility theorem has the appropriate form: integer variables, rational linear constraints converted to integer coefficients, and no boundedness requirement. Lenstra’s paper explicitly addresses reducing unbounded feasibility instances, and the cited Kannan publication confirms the stated dimension-dependent bound. See [Lenstra’s paper](https://pub.math.leidenuniv.nl/~lenstrahw/PUBLICATIONS/1983i/art.pdf) and [Kannan’s publication](https://doi.org/10.1145/800061.808749).
The variable count $2m+2$ is correct. Cohort populations and accumulated class counts have polynomial binary descriptions, even though simulation can take $B$ traversals.
The branch factors correctly account for canonical words, exhaustion traversals, residues, and weak orderings. Clause scores permit class selection in $O(Km)$ arithmetic operations per simulated turn. The resulting overall bound
$$
\tau\,m^B B^{2m+1}q^{2m+1}2^{O(m^3)}
\operatorname{poly}(m,q,K,L)
$$
is consistent with the procedure described. Its double-exponential upper bound in $L$ follows from $B\le2^{O(L)}$.
For fixed $m$ and fixed $B$, the algorithm is polynomial in the remaining input parameters.
The unrestricted classification is not established. Exact decidability, bounded canonical witnesses, and polynomial solvability for fixed $m$ and $B$ do not imply either unrestricted polynomial-time solvability or hardness.
The minimum additional requirement is a proof settling the unrestricted problem: either an algorithm with polynomial running time in the requested input parameters or a valid hardness reduction for the exact limiting threshold problem. This requires new 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.