Dominating thinning for bounded time-varying propensities

Inputs. A finite or countable state set $E\subseteq {\mathbb{Z}}^d$, finitely many time-dependent propensities $a_j(t,x)$ from Finite-channel reaction propensity systems and their generator, a finite horizon $T>0$, initial state $x_0\in E$, optional candidate budget $B\in {\mathbb{N}}_0\cup \{\mathrm{\infty }\}$ defaulting to $\mathrm{\infty }$ (where ${\mathbb{N}}_0:=\{0,1,2,\dots \}$), and a deterministic envelope $\mathrm{\Lambda }<\mathrm{\infty }$ with an admissibility certificate establishing $0\le \lambda (t,x):={\sum }_{j=1}^R{a}_j(t,x)\le \mathrm{\Lambda }(0\le t\le T,x\in E)\mathrm{.}$ The global inequality is a precondition; the procedure does not verify the certificate exhaustively. The random source supplies independent $E_n\sim \mathrm{Exp}(1)$ and $U_n\sim \mathrm{Unif}[0,1]$ sequences. Their countable product model uses Countable Choice and Dependent Choice; the unit exponential law is as in Exponential and Weibull survival specifications define probability laws. For the uniform law, Assuming countable choice, $\mathcal{L}({\mathbb{R}}^n)$ is a sigma-algebra containing every elementary set and ${\lambda }_n$ is a complete measure extending elementary volume makes the set function in Lebesgue measurable sets, the family $\mathcal{L}({\mathbb{R}}^n)$, and the restricted set function ${\lambda }_n$ a measure, and A box in ${\mathbb{R}}^n$ with parameters $a_i\le b_i$ is Lebesgue measurable of measure ${\prod }_{i<n}(b_i-a_i)$, whichever of its faces are included gives its restriction to $[0,1]$ mass one and interval probabilities equal to interval lengths.

Procedure. Set $t=0$, $x=x_0$, and candidate counter $n=0$. If $\mathrm{\Lambda }=0$, return the constant path through $T$ with status absorbed. Otherwise, while $t<T$:

1. If $n=B$, return the path prefix with status budget-exhausted.
2. Set $\tau =E_{n+1}\mathrm{/}\mathrm{\Lambda }$. If $t+\tau \ge T$, return the state held through $T$ with status horizon.
3. Set $t\leftarrow t+\tau$ and evaluate $\lambda (t,x)$. If $\lambda (t,x)>\mathrm{\Lambda }$ at this candidate, stop with status invalid-envelope; this pointwise runtime check detects only violations at candidate times and states that are actually evaluated. The algorithm does not continue by clipping the rate.
4. If $U_{n+1}\ge \lambda (t,x)\mathrm{/}\mathrm{\Lambda }$, reject this candidate and leave $x$ unchanged; set $n\leftarrow n+1$ and continue. Otherwise choose the first $J$ such that $U_{n+1}\mathrm{\Lambda }<{\sum }_{j=1}^J{a}_j(t,x),$ set $x\leftarrow x+{\nu }_J$, append the marked event $(t,J,x)$, set $n\leftarrow n+1$, and continue.

A time-dependent propensity without a certified finite envelope is outside this algorithm; integrated-hazard inversion is a separate method and is not used here. If the loop reaches $t=T$, return status horizon. If the global precondition is false, the procedure need not detect that failure: status invalid-envelope is returned only when the pointwise check in step 3 encounters a violation. No path law is claimed under a false global envelope.