LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Competing exponential clocks give the reaction event law

Statement

Assume Countable Choice. Let $R \geq 1$ , let $r_{1}, \dots, r_{R} \geq 0$ , and set $r_{0} = \sum_{j = 1}^{R} r_{j}$ . On a common probability space let $E_{1}, \dots, E_{R}$ be independent random variables, each with the unit exponential law $Exp (1)$ , whose survival at $t \geq 0$ is $e^{- t}$ . If $r_{0} > 0$ , define $T_{*} : = \min_{j : r_{j} > 0} \frac{E_{j}}{r_{j}}, J_{*} : = {argmin}_{j : r_{j} > 0} \frac{E_{j}}{r_{j}} .$ Then ties have probability zero, $T_{*} \sim Exp (r_{0})$ , $J_{*}$ is independent of $T_{*}$ , and $P (J_{*} = j) = \frac{r_{j}}{r_{0}} .$ If $r_{0} = 0$ , every $r_{j} = 0$ and no finite reaction clock is active.

Facts & Assumptions

Given: Countable Choice, finite nonnegative rates $r_{1}, \dots, r_{R}$ , and independent unit exponential random variables $E_{1}, \dots, E_{R}$ .

[F1]

Under Countable Choice, $Exp (θ)$ has density $θ e^{- θ t}$ on $t > 0$ and survival $e^{- θ t}$ for $t \geq 0$ ; the law is unique. (Exponential and Weibull survival specifications define probability laws)

[F2]

Independence of the generated sigma-algebras gives the product formula for every measurable rectangle in a finite product of real lines. The inverse image of each such rectangle under the coordinate tuple is a finite intersection of coordinate preimages, hence measurable; since the rectangles generate the finite product sigma-algebra, the tuple is a random element there. Iterating the sigma-finite product-measure theorem gives the finite product law of the marginals. It and the joint law agree on the generating pi-system of elementary rectangles, which contains the whole space with mass one, so the measure-uniqueness theorem identifies these laws. (Independent random elements, Independent sigma-algebras and independent events, The product sigma-algebra and its finite iterates, For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique, Measures agreeing on a generating pi-system are equal under an increasing finite-measure exhaustion from that pi-system)

[A1]

Countable Choice is assumed in [F1] for the exponential probability law. (The Axiom of Countable Choice ( ${A C}_{ω}$ ))

Proof

1.1givenalgebra

If $r_{0} = 0$ , nonnegativity of the finite sum implies every $r_{j} = 0$ , so the set of active clocks is empty and no finite candidate time is defined.

1.2A1F1F2givenalgebra

Suppose $r_{0} > 0$ . For $t \geq 0$ , independence in [F2] and the unit exponential survival in [F1] give $P (T_{*} > t) = \prod_{j : r_{j} > 0} P (E_{j} > r_{j} t) = \prod_{j : r_{j} > 0} e^{- r_{j} t} = e^{- r_{0} t} .$ Thus $T_{*}$ has the unique law $Exp (r_{0})$ specified in [F1].

2.1A1F1F2step 1.2algebra

For a channel $j$ with $r_{j} > 0$ , the scaled clock $E_{j} / r_{j}$ has density $r_{j} e^{- r_{j} t}$ on $t > 0$ by change of variables in [F1]. Independence [F2] therefore gives the joint density that channel $j$ rings first at time $t$ as $r_{j} e^{- r_{j} t} \prod_{k \neq j : r_{k} > 0} e^{- r_{k} t} = r_{j} e^{- r_{0} t} .$ Integrating over $t > 0$ yields $P (J_{*} = j) = r_{j} / r_{0}$ , and this joint density factors as $r_{0} e^{- r_{0} t} (r_{j} / r_{0})$ , proving independence of $T_{*}$ and $J_{*}$ .

3.1F1F2step 1.2step 2.1∎

For distinct active $i, j$ , the independent scaled clocks have continuous densities, so their equality has probability zero: conditioning on $E_{i} / r_{i}$ leaves the independent variable $E_{j} / r_{j}$ with zero probability at each singleton. A finite union over pairs shows the minimum is unique almost surely. Together with steps 1.2 and 2.1 this proves all assertions.

Depends on

Used by

Dependency tree · two levels

55 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Daniel T. Gillespie, Exact Stochastic Simulation of Coupled Chemical Reactions (standard reference, not scraped)
David F. Anderson, Introduction to Stochastic Processes with Applications to Biology, Chapters 6–7 (standard reference, not scraped)
David F. Anderson and Thomas G. Kurtz, Continuous Time Markov Chain Models for Chemical Reaction Networks (standard reference, not scraped)