Answer: —
Theorem 4.4 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateThe problem of computing an optimal execution is NP-hard.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite catalogue of good categories \(M\), a finite support \(\mathcal T\) of initial agent types \(t=(S_t,D_t)\), and rational masses \(\mu_t\) summing to \(1\), what is the maximum total number of exchanges per unit mass achievable by a finite schedule of legal dynamic cycle actions? Each agent holds and demands integral sets of categories; copies are interchangeable, and a cycle action of mass \(\lambda\) uses disjoint cohorts of each participating type, updates their states by the paper’s cycle rule, and cannot use more mass of a type than is available.
Let \(M\) be a set of \(m\) item classes. A society is given by its support: the list of the \(\tau\) types with positive mass, each mass \(\mu_t\) a binary rational, with \(\sum_t\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types.
Each type has a binary-encoded initial bundle \(b_t\in\mathbb Z_{\geq0}^{M}\) of class copies and a demand set \(D_t\subseteq M\), with \(b_t(j)=0\) for every \(j\in D_t\). Every class has positive aggregate initial supply; copies have individual owners.
A current agent state is \(s=(b,D)\). Receiving a class removes it permanently from that agent's demand set; received copies may subsequently be traded. Agents accept any currently demanded class in exchange for one currently owned copy.
A mass-cycle step selects \(k\geq2\) pairwise disjoint cohorts of equal real mass \(\delta>0\), in states \((b_i,D_i)\), and classes \(j_i\in D_i\), with indices cyclic and \(b_i(j_{i-1})\geq1\).
Cohort \(i\) receives one copy of \(j_i\) per agent from cohort \(i+1\), gives one copy of \(j_{i-1}\), and moves simultaneously to \((b_i-e_{j_{i-1}}+e_{j_i},D_i\setminus\{j_i\})\), where \(e_j\) is the unit vector for class \(j\).
States and class labels may repeat around a cycle, but participating agents and transferred copies are distinct. All cohorts must be available before the step; repeated use of a state consumes the sum of its selected cohort masses. Cohorts may split across later steps.
An execution is a finite sequence of such steps, possibly empty, with value \(\sum_C k_C\delta_C\), the total exchanges per unit population. The input also contains a binary rational threshold \(Q\geq0\); let \(L\) be the total input bit length. State running times in \(m,\tau,L\).
Is deciding whether an execution has value at least \(Q\) solvable in polynomial time in \(m,\tau,L\), or is it NP-hard?
For finite agents and individually identified items, maximizing exchanges over dynamic cycle executions is NP-hard; optimal static executions, which transfer each item at most once, are computable in polynomial time. [Discrete results](https://arxiv.org/pdf/2110.14271).
No result settling this precise continuous mass-cycle problem was located.
The general polynomial-time versus NP-hard classification remains unresolved here. I prove:
$$
\tau^{O(m)}2^{O(m^2)}\operatorname{poly}(L).
$$
In particular, the problem is polynomial-time solvable for every fixed $m$.
Throughout, agents may split into arbitrarily small cohorts. None of the arguments imposes indivisibility on population mass.
Construct the initial trading graph $G$ with vertex set consisting of the types and classes. Its arcs are
$$ j\longrightarrow t \quad\text{if }b_t(j)>0, \qquad t\longrightarrow j \quad\text{if }j\in D_t. $$
Write $C(v)$ for the strongly connected component containing vertex $v$, and define
$$ A_t=\{j\in D_t:C(j)=C(t)\}, \qquad d_t=|A_t|. $$
Thus $A_t$ consists of the demands of type $t$ lying in its initial strongly connected component.
A positive mass of type-$t$ agents can receive class $j\in D_t$ in some execution if and only if $j\in A_t$. Moreover, every such demand can receive positive mass in a single step from the initial society.
Keep an agent’s initial type as a permanent auxiliary label.
First, an agent never owns a currently demanded class. This holds initially by hypothesis. Receiving a class removes it from the demand set, and giving a copy cannot violate the property.
Suppose inductively that every previous transfer has occurred within one strongly connected component of $G$. Collapse each current state to its initial type. Every current demand arc is an initial demand arc. Every current ownership arc is either:
In the second case, the inductive hypothesis gives $C(j)=C(t)$. Consequently, all newly created arcs lie within initial strongly connected components.
A current trading cycle becomes a directed closed walk in this collapsed graph. Its projection onto the condensation graph of $G$ cannot use an arc between distinct components: the condensation graph is acyclic, and such an arc would belong to a nontrivial directed closed walk. Hence every transfer in the current step also stays within an initial component. Induction proves necessity.
Conversely, suppose $C(t)=C(j)$ and $j\in D_t$. The arc $t\longrightarrow j$ lies on a simple directed cycle of $G$: append a shortest directed path from $j$ to $t$. This cycle alternates between types and classes. It contains at least two types, since an initial type cannot both own and demand the same class.
Select a cohort of mass
$$ 0<\delta\leq \min\{\mu_u:u\text{ is a type on this cycle}\} $$
from each participating type. Every required giving class is initially owned, and every receiving class is initially demanded. Executing this cycle gives a positive mass of type-$t$ agents class $j$. $\square$
The sets $A_t$ are computable in time polynomial in $m,\tau,L$. In particular, every execution has value at most
$$ H=\sum_t\mu_t d_t. $$
I use “static” in the sense of the question: each individually owned copy is transferred at most once.
For every initially owned class, introduce a variable $a_{tj}$ representing the mass of copies of $j$ given by type $t$. For every demanded class, introduce $z_{tj}$ representing the mass received by type $t$. Missing variables are interpreted as zero.
Consider the linear program
$$ \begin{aligned} \text{maximize}\quad &\sum_t\sum_{j\in D_t}z_{tj},\\ 0\leq a_{tj}&\leq \mu_t b_t(j),\\ 0\leq z_{tj}&\leq \mu_t,\\ \sum_j a_{tj}&=\sum_j z_{tj} &&\text{for every }t,\\ \sum_t a_{tj}&=\sum_t z_{tj} &&\text{for every }j. \end{aligned} $$
Let its optimum be $S$.
$S$ is exactly the maximum value of a static execution. It is attained and computable in polynomial time in $m,\tau,L$.
Every static execution satisfies the displayed constraints. A copy given in a static execution must be given by its initial owner: a different owner could possess it only after an earlier transfer. Demand permanence gives the bounds $z_{tj}\leq\mu_t$. Conservation gives both sets of balance equations.
It remains to prove that the LP optimum is attainable. The feasible region is bounded and rational, so it has a rational optimum.
Fix a rational feasible solution. For a type $t$, put
$$ r_t=\sum_j a_{tj}=\sum_j z_{tj}. $$
If $r_t=0$, assign no exchanges to this type. Otherwise, for initially owned classes $p$ and demanded classes $q$, define
$$ g_{pq}=\frac{a_{tp}z_{tq}}{\mu_t r_t}. $$
Then
$$ \sum_q g_{pq}=\frac{a_{tp}}{\mu_t}\leq b_t(p), \qquad \sum_p g_{pq}=\frac{z_{tq}}{\mu_t}\leq 1. $$
The polytope of nonnegative matrices satisfying these row and column bounds has integral vertices. Indeed, its constraint matrix is the vertex-edge incidence matrix of a bipartite graph; changing signs on one part gives a directed incidence matrix, which is totally unimodular. Adding slack variables preserves total unimodularity, and the bounds are integers.
Therefore $g$ is a convex combination of integral matrices satisfying the same bounds. The coefficients can be chosen rational: the equations defining a convex decomposition form a feasible rational linear system.
Each integral matrix specifies an individual agent’s planned static exchanges. Each demanded class occurs at most once, and at most $b_t(p)$ copies of initial class $p$ are selected. Its number of selected giving slots equals its number of receiving slots.
Do this for every type and choose a common denominator $N$ for all resulting cohort masses. We obtain a finite population of $N$ agents with integer numbers of planned slots.
Form a directed bipartite multigraph whose vertices are these agents and the classes. For each selected original copy of class $j$, add an arc from $j$ to its owner. For each planned receipt of $j$, add an arc from the receiving agent to $j$. Every vertex is balanced:
A finite balanced directed multigraph decomposes into simple directed cycles. Execute these cycles. Every giving edge names an original copy still owned until that edge is used. Every receiving edge names a distinct planned demand of its agent, so that demand remains available until used. Thus every cycle is valid, and no received copy is subsequently given.
Finally, replace each finite agent by a cohort of mass $1/N$. This realizes the same static execution in the continuous society, with value $\sum_{t,j}z_{tj}$.
The LP has $O(\tau m)$ variables and constraints and polynomial encoding length. Polynomial-time rational linear programming therefore computes $S$. $\square$
Define
$$ I_t=\{j:b_t(j)>0,\ C(j)=C(t)\}. $$
Introduce variables:
Consider the LP
$$ \begin{aligned} \text{maximize}\quad &\sum_t d_t c_t,\\ 0\leq c_t&\leq\mu_t,\\ 0\leq a_{tj}&\leq b_t(j)c_t &&(j\in I_t),\\ 0\leq z_{tj}&\leq c_t &&(j\in A_t),\\ \sum_j a_{tj}&=\sum_j z_{tj}\geq c_t &&\text{for every }t,\\ \sum_t a_{tj}&=\sum_t z_{tj} &&\text{for every }j. \end{aligned} $$
Let its optimum be $U$.
Every dynamic execution has value at most $U$, and
$$ U\leq H. $$
The bound $U$ is computable in polynomial time in $m,\tau,L$.
Consider an individual agent that participates.
Its first exchange gives an original copy. Also, it can never receive any class present in its initial bundle, because none of those classes belongs to its initial demand set.
Let $r$ be the number of original copies it gives during the execution. Every other copy it receives belongs to its initial demand set, and it receives each such class at most once. Since every exchange preserves its bundle size, it retains exactly $r$ received copies at the end. In particular, $r\geq1$.
Aggregating over participating agents gives
$$ a_{tj}\leq b_t(j)c_t,\qquad z_{tj}\leq c_t,\qquad \sum_j a_{tj}=\sum_j z_{tj}\geq c_t. $$
Proposition 1 restricts these classes to $I_t$ and $A_t$.
For each class, the number of original copies that leave their initial owners equals the number held as received copies at the end. This proves the class balance equation.
Finally, each participating type-$t$ agent receives at most $d_t$ classes. Hence the execution’s value is at most $\sum_t d_t c_t$, which is at most $U$. The inequality $U\leq H$ follows from $c_t\leq\mu_t$.
This LP also has $O(\tau m)$ variables and constraints with polynomial encoding length. $\square$
Consequently:
Equality with $U$ requires additional reasoning, as the next example shows.
Take five classes $x,y,z,v,w$ and four types:
| Type | Mass | Initial bundle | Demand set |
|---|---:|---|---|
| $P$ | $3/8$ | one $x$, one $v$ | $\{y,w\}$ |
| $A$ | $1/4$ | one $w$ | $\{x,z,v\}$ |
| $B$ | $1/4$ | one $v$ | $\{x,y,z\}$ |
| $C$ | $1/8$ | one $y$, one $z$ | $\{x,w\}$ |
Every class has positive aggregate initial supply.
All vertices lie in one initial strongly connected component. For example,
$$ x\longrightarrow P\longrightarrow w\longrightarrow A \longrightarrow v\longrightarrow B\longrightarrow y \longrightarrow C\longrightarrow x $$
is a directed cycle, and the additional path $A\longrightarrow z\longrightarrow C$ incorporates $z$. Thus
$$ H=\frac38\cdot2+\frac14\cdot3+\frac14\cdot3+\frac18\cdot2 =\frac52. $$
A static execution activates the entire population:
$$ P:\ x\mapsto w,\qquad A:\ w\mapsto v,\qquad B:\ v\mapsto x. $$
Every agent participates once. Its associated variables are feasible for the upper-bound LP with $c_t=\mu_t$. Therefore $U=H=5/2$.
No execution in this society has value $5/2$.
Suppose an execution attained $H$. Since $H$ counts every initial demand and no agent can receive a demanded class twice, all demands would have to be satisfied, except possibly on sets of mass zero.
In particular, all $P$ agents participate. Each participating agent retains at least one received copy, by the argument in Proposition 3. Hence $P$ agents hold at least $3/8$ copies of classes $y,w$ at the end.
The total supply of these two classes is exactly
$$ \operatorname{supply}(y)+\operatorname{supply}(w) =\frac18+\frac14=\frac38. $$
Thus every copy of $y$ and $w$ is held by $P$ at the end.
Let $a_{Cy}$ and $a_{Cz}$ denote the masses of original copies given by $C$. Every initial $y$ copy has left $C$, so $a_{Cy}=1/8$. No $C$ agent retains a received $w$, since every $w$ copy is held by $P$.
The only other class $C$ can receive is $x$, once per agent. Consequently, the total mass of received copies retained by $C$ is at most $1/8$. Bundle-size conservation gives
$$ \frac18+a_{Cz} =a_{Cy}+a_{Cz} =\text{mass of received copies retained by }C \leq\frac18. $$
Therefore $a_{Cz}=0$.
All initial $z$ copies belong to $C$. If none leaves its initial owner, no other agent can ever receive $z$. This contradicts satisfaction of the $z$ demands of types $A$ and $B$. $\square$
This example disproves the inference that activating agents through static exchanges suffices to satisfy all their accessible demands dynamically. It does not establish whether the supremum of execution values in this example equals $5/2$.
If $d_t\leq1$ for every type, then the dynamic optimum equals $S$. The threshold problem is therefore polynomial-time solvable.
By Proposition 1, each agent can receive at most one class during the entire execution. An agent that receives a copy consequently cannot participate in a later exchange. Thus no received copy can be transferred again.
Every dynamic execution is therefore static. Proposition 2 computes and attains the optimum. $\square$
This includes all instances with $m=2$. Writing the classes as $x,y$, define
$$ \alpha=\sum_{\substack{t:\ b_t(x)>0\\ y\in D_t}}\mu_t, \qquad \beta=\sum_{\substack{t:\ b_t(y)>0\\ x\in D_t}}\mu_t. $$
The optimum is
$$ 2\min\{\alpha,\beta\}. $$
Indeed, agents with no copies cannot participate, agents owning both classes have no demands, and every remaining participating agent belongs to one of these two groups and can exchange only once. Matching equal masses of the groups attains the bound. For $m\leq1$, the optimum is zero.
The following argument handles finite executions and the exact comparison with $Q$, including equality.
Fix an initial type $t$ and write $d=|D_t|$.
Every state descended from this type can be represented by:
The current state satisfies
$$ D=D_t\setminus R, $$
and
$$ b(j)= \begin{cases} b_t(j)-a_j,&j\notin D_t,\\ 1,&j\in F,\\ 0,&j\in D_t\setminus F. \end{cases} $$
Furthermore,
$$ 0\leq a_j\leq b_t(j), \qquad \sum_{j\notin D_t}a_j=|F|. $$
These identities follow because initial classes cannot be received, demanded classes are received at most once, and bundle size is conserved.
There are $3^d$ choices for the status of the initially demanded classes. There are at most
$$ \binom{(m-d)+d}{d}=\binom md $$
nonnegative vectors $a$ whose coordinate sum is at most $d$. Thus the number of candidate states for this initial type is at most
$$ 3^d\binom md\leq4^m. $$
Some candidates may be unreachable; retaining them causes no difficulty because their initial mass is zero.
Keeping initial-type labels, the total number of candidate states is therefore at most
$$ N\leq\tau4^m. $$
Each state has an encoding length polynomial in $L$: every original coordinate decreases by at most $m$, regardless of its binary-encoded initial magnitude.
Keeping initial-type labels is legitimate. A cohort containing several initial types can be partitioned by those types. Taking a common refinement of these finite partitions around a cycle decomposes the step into finitely many steps with constant initial-type labels and the same resulting state masses.
Represent a participant that gives class $p$ and receives class $q$ by an edge
$$ p\longrightarrow q $$
labelled with its current state. We have $p\neq q$, since a currently demanded class is not owned.
A mass-cycle is a directed closed walk in this class graph. Every closed walk decomposes into simple directed cycles while preserving its individual labelled edges. Each resulting cycle has between two and $m$ edges.
Execute these cycles using the originally selected cohorts, reserving those cohorts until their corresponding cycle is executed. They remain available because the original cohorts were disjoint. Each participant gives and receives the same classes as in the original step. Redirecting copies of the same class is permitted.
Hence the resulting states and total value are preserved, and it suffices to use cycles with at most $m$ participants.
Importantly, a state label may occur several times within one such cycle. Its required mass is the sum over those occurrences.
Make one place for each candidate labelled state and one additional place recording accumulated value.
For every state $s=(b,D)$ and classes $p,q$ with $b(p)>0$ and $q\in D$, create the primitive labelled edge $p\longrightarrow q$. There are at most
$$ E\leq Nm^2 $$
such edges.
Enumerate all simple class cycles among these edges. There are at most
$$ \sum_{k=2}^{m}E^k\leq mE^m $$
when $E\geq1$.
A cycle of length $k$ becomes one Petri-net transition:
Firing this transition by amount $\delta$ requires, before firing, mass $\delta$ times each input multiplicity. It therefore enforces exactly the question’s availability rule for repeated states. Its value contribution is $k\delta$.
Initialize the state places with the given masses and the value place with zero. The target marking has zero in every state place and $Q$ in the value place. Covering this marking is precisely achieving value at least $Q$.
For an explicitly given finite Petri net with nonnegative integer input and output matrices and binary-rational markings, continuous coverability using rational firing amounts is polynomial-time decidable. This is the Fraca–Haddad theorem, stated as Proposition 2.4 in [*The Logical View on Continuous Petri Nets*](https://lsv.ens-paris-saclay.fr/Publis/PAPERS/PDF/BFHH-tocl17.pdf). Its semantics uses finite firing sequences. The constructed net satisfies its hypotheses: all multiplicities are nonnegative integers, and both markings are binary rational.
Allowing real firing amounts does not change this decision. For any fixed finite transition sequence, the availability inequalities and value requirement are rational linear constraints in its firing amounts. If positive real amounts satisfy them, choose a positive rational number smaller than every amount and impose it as a common lower bound. The resulting feasible rational linear system has a rational solution. Thus a real witness implies a rational witness with the same transition sequence.
The net construction is therefore exact for the problem as stated.
The threshold problem is decidable in time
$$ (\tau4^m m^2)^{O(m)}\operatorname{poly}(L) = \tau^{O(m)}2^{O(m^2)}\operatorname{poly}(L). $$
The candidate-state set has size at most $\tau4^m$, and the number of cycle transitions is at most $m(\tau4^m m^2)^m$. Their encodings have polynomial length per transition. Apply polynomial-time continuous coverability to this explicit net. $\square$
The state expansion gives a polynomial algorithm for fixed $m$, but its size is exponential when $m$ varies. The compact LP bounds avoid that expansion, but Proposition 4 proves that the upper bound is not always attainable.
A general polynomial algorithm would need an exact formulation that captures the additional execution constraints. A hardness proof would need a reduction whose choices remain hard despite arbitrary cohort splitting. Neither is established above.
⟨structured verdict parsed — rendered above⟩
The output establishes substantial partial results, but it does not resolve the general polynomial-time versus NP-hard classification requested in USER_TASK. Its stated partial status is accurate. I found no false step or substantive gap in Propositions 1–6.
The sole major issue is incomplete coverage of the assigned target: neither a polynomial-time algorithm for variable $m$ nor an NP-hardness proof is established.
The ownership invariant is correct. Initially, an agent owns no demanded class; receiving removes the received class permanently from its demand set, and giving cannot violate this invariant.
The strongly connected component induction is valid. Current demand arcs remain initial demand arcs. Any ownership arc introduced by a previous receipt lies within an initial component by the induction hypothesis. Consequently, a current trading cycle projects to a directed closed walk in the initial condensation graph. A directed acyclic graph cannot contain a closed walk traversing an intercomponent arc. This proves necessity without assuming that states or initial types occur only once in a cycle.
For sufficiency, a shortest path from $j$ to $t$, together with the arc $t\longrightarrow j$, produces a simple directed cycle. The graph is bipartite, and a cycle with only one type would require that type initially to own and demand the same class, which is excluded. Thus the constructed cycle meets the requirement of at least two participating cohorts. All selected types have positive mass, so the displayed choice of $\delta$ is available.
The quantifiers established are: for each eligible pair $(t,j)$, there exists an initial single-step execution giving class $j$ to positive mass of type $t$. The proof does not require one common execution for all eligible pairs.
The upper bound
$$
H=\sum_t\mu_t d_t
$$
follows because each accessible demand can be satisfied at most once per agent. The graph and its strongly connected components have polynomial input size.
Finding: correct.
The LP constraints are necessary. In a static execution, a transferred copy must leave its initial owner, because possession by another owner would require a previous transfer. Each demand can be satisfied at most once, and the type and class balance equations express exchange and copy conservation.
The attainment argument is also valid. For $r_t>0$, the proposed matrix has row sums $a_{tp}/\mu_t$ and column sums $z_{tq}/\mu_t$. Its bounds are integers, and the stated bipartite incidence argument establishes total unimodularity. The bounded matrix polytope therefore has integral vertices. Its rational point admits a finite rational convex decomposition.
An integral matrix specifies a permissible exchange plan: original giving slots respect bundle capacities, demanded receiving slots occur at most once, and the total numbers of giving and receiving slots agree. Passing to a common denominator produces a finite population representing the prescribed type and plan masses.
The resulting directed multigraph is balanced at agents and classes. Its simple-cycle decomposition is executable: an unused original-copy edge still refers to a copy held by its original owner, and an unused receipt edge still refers to an unsatisfied demand. Initially owned and demanded classes are disjoint, so no prohibited cycle with only one agent occurs. Replacing the finite agents by equal-mass cohorts is legitimate.
The denominator need not be polynomially bounded for this existence argument. The polynomial-time claim concerns solving the compact LP, whose dimensions and coefficient lengths are polynomial in the input.
Finding: correct, including attainment.
The bookkeeping of original and received copies is sound. An agent cannot receive any initially owned class, since such a class was not initially demanded. Its first exchange therefore gives an original copy, and any original copy it gives cannot subsequently return to it.
Bundle-size conservation consequently makes the number of retained received copies equal to the number of original copies given. For a participating agent, this number is at least one. Aggregating gives the stated capacity, retention, and participation constraints.
The class balance equation is valid with individually identified copies: each original copy that leaves its initial owner ends with another owner as a received copy. Transfers between later owners do not change this accounting.
Proposition 1 supplies the restrictions to $I_t$ and $A_t$. The objective bounds total receipts because each participating type-$t$ agent satisfies at most $d_t$ demands. Finally, $c_t\leq\mu_t$ gives $U\leq H$.
Finding: correct. This establishes an upper bound, without asserting its attainability.
The displayed cycle contains every type and every class except $z$; the additional path places $z$ in the same strongly connected component. The calculation is correct:
$$
H=\frac34+\frac34+\frac34+\frac14=\frac52.
$$
Both proposed static steps satisfy initial ownership, demand, and cohort availability. They use disjoint portions of $P$, activate the entire population, and yield feasible upper-bound LP variables with $c_t=\mu_t$. Thus $U=H$ follows.
The contradiction argument is valid. Attainment of $H$ would satisfy all initial demands up to sets of mass zero. Participating $P$ agents retain at least $3/8$ received copies in total, all of classes $y,w$. This exhausts the combined supply of those classes.
Therefore all original $y$ copies leave $C$, while $C$ retains no received $w$. Its retained receipts can only be $x$, with total mass at most $1/8$. Conservation then forces $a_{Cz}=0$. Since all original $z$ copies belong to $C$, the positive-mass $z$ demands of $A$ and $B$ cannot be satisfied.
The proof establishes nonattainment of $5/2$. It does not establish a strict gap between the supremum and $5/2$, and the prover correctly acknowledges that distinction.
Finding: correct.
If $d_t\leq1$, Proposition 1 limits every agent to one receipt over the execution. A subsequent participation would require another receipt, so a received copy cannot be transferred again. Every dynamic execution is consequently static.
For $m=2$, agents that can participate belong to the two displayed groups. Each can exchange only once, and balancing the exchanged classes requires equal participating masses from the groups. The value $2\min\{\alpha,\beta\}$ and its attainment are correct. The zero optimum for $m\leq1$ also respects the ownership-demand invariant.
Finding: correct.
The state representation respects demand permanence, initial-copy identities, and bundle conservation. Initially demanded classes can be received only once, so their current multiplicities are zero or one. Initially owned classes cannot be received. The equation
$$
\sum_{j\notin D_t}a_j=|F|
$$
is the correct conservation identity.
The candidate count is valid: the demanded-class statuses contribute $3^d$, and the original-copy decrement vectors contribute at most $\binom md$. The bound $3^d\binom md\leq4^m$ holds. Binary bundle magnitudes do not cause additional states, since at most $m$ receipts are possible. Keeping unreachable candidates at zero initial mass is harmless because transitions still implement valid exchanges.
Refining cohorts by initial type is legitimate. The closed-walk decomposition into simple class cycles preserves each participant’s giving and receiving classes. Reserving the originally selected disjoint cohorts makes sequential execution valid. Thus restricting cycles to at most $m$ participants preserves finite executions and their values.
The Petri-net inputs correctly count repeated occurrences of a state. Its enabling condition uses mass available before firing, so successor mass cannot improperly supply the same simultaneous step. The value place records exactly $k\delta$, and its target implements the non-strict threshold comparison.
The cited theorem checks out. Proposition 2.4 concerns polynomial-time continuous coverability for explicitly encoded nets with binary-rational markings; the accompanying definitions use finite rational firing sequences and the required input-availability semantics. The construction satisfies these hypotheses. [*The Logical View on Continuous Petri Nets*, Definitions 2.1–2.3 and Proposition 2.4](https://lsv.ens-paris-saclay.fr/Publis/PAPERS/PDF/BFHH-tocl17.pdf).
The real-to-rational witness argument is valid, including threshold equality. For a fixed finite positive real firing sequence, imposing a sufficiently small positive rational lower bound leaves a feasible rational linear system, which has a rational solution. The empty execution is allowed and handles $Q=0$.
The state and transition counts support
$$
\tau^{O(m)}2^{O(m^2)}\operatorname{poly}(L).
$$
This is polynomial for fixed $m$, but does not give polynomial time in the full variable input.
Finding: correct.
The minimum additional work needed to complete the assignment is a general polynomial-time algorithm with a polynomial bound in $m,\tau,L$, or a valid NP-hardness reduction for the stated continuous model. This requires a new result; an expositional clarification cannot close the remaining classification question.
⟨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.