Next-reaction method by internal Poisson clocks

Inputs. A finite state set $E\subseteq {\mathbb{Z}}^d$, a finite-channel time-homogeneous system from Finite-channel reaction propensity systems and their generator, initial state $x_0\in E$, horizon $T>0$, and optional reaction-event budget $B\in {\mathbb{N}}_0\cup \{\mathrm{\infty }\}$, defaulting to $\mathrm{\infty }$, where ${\mathbb{N}}_0:=\{0,1,2,\dots \}$. Supply independent unit exponential increments $E_{j,k}\sim \mathrm{Exp}(1)$ for $1\le j\le R$ and $k\ge 1$. The countable product construction uses Countable Choice and Dependent Choice by Assuming countable and dependent choice, countable products of arbitrary probability spaces; the exponential law assumes Countable Choice by Exponential and Weibull survival specifications define probability laws.

Initialization. Set $t=0$, $x=x_0$, $n=0$, internal times $A_j=0$, threshold indices $m_j=1$, and next thresholds $S_j=E_{j,1}$ for each channel.

Procedure. At each state $x$:

1. Compute $a_j(x)$ for every channel. If $\lambda (x)=0$, return the constant path through $T$ with status absorbed.
2. If $n=B$, return the path prefix with status budget-exhausted. For each $j$, set ${\mathrm{\Delta }}_j=(S_j-A_j)\mathrm{/}{a}_j(x)$ when $a_j(x)>0$ and ${\mathrm{\Delta }}_j=+\mathrm{\infty }$ when $a_j(x)=0$.
3. Let $\mathrm{\Delta }={\min }_j{\mathrm{\Delta }}_j$. If $t+\mathrm{\Delta }>T$, return the path held at $x$ through $T$ with status horizon.
4. Let $J$ be the least minimizing channel (ties have probability zero). For every channel set $A_j\leftarrow A_j+a_j(x)\mathrm{\Delta }$. Set $t\leftarrow t+\mathrm{\Delta }$, $x\leftarrow x+{\nu }_J$, append the marked event, then set $m_J\leftarrow m_J+1$ and $S_J\leftarrow S_J+E_{J,m_J}$; finally set $n\leftarrow n+1$.

On the returned time interval (through $T$ unless the budget is exhausted), the internal time is $A_j(t)={\int }_0^t{a}_j(X_{s-})ds$, and almost surely the random-time-change representation is $X_t=X_0+{\sum }_{j=1}^R{\nu }_j{Y}_j(A_j(t)),$ where $S_{j,k}={\sum }_{q=1}^k{E}_{j,q}$ and $Y_j(u)=\mathrm{\#}\{k:S_{j,k}\le u\}$. An event at exactly $T$ is recorded before returning. If the loop reaches $t=T$, return the path through $T$ with status horizon. With unlimited budget, Finite-state Gillespie and next-reaction methods have the specified CTMC law ↗ proves the Poisson threshold-clock laws and equality with the direct method's reaction path law. The implementation scans all $R$ channels at each event; no logarithmic update-tree cost is claimed.