ExampleConstruction: Literature-sourcedVerification: AI-generatedPipeline-generatedprecheck pass

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.

Gillespie simulation of a finite birth-death reaction network

Statement

Assume Countable Choice and Dependent Choice. Let $E = {0, 1, 2}$ with a birth channel $ν_{+} = 1$ , $a_{+} (x) = 2 - x$ , and a death channel $ν_{-} = - 1$ , $a_{-} (x) = x$ . From every state the total rate is $2$ . Starting at $1$ , the first holding time is $E_{1} / 2$ ; the event is a birth if $U_{1} < 1 / 2$ and a death otherwise. With unlimited event budget, the direct method generates the exact finite-state reaction path law on every finite horizon.

Facts & Assumptions

Given: Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )), Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain), the finite state set, two reaction channels, initial state $1$ , unlimited event budget, and independent exact exponential and uniform inputs.

[F1]

Each active channel must have its poststate in $E$ , and the generator is the finite rate-weighted increment sum on bounded functions. (Finite-channel reaction propensity systems and their generator)

[F2]

Assuming Countable Choice and Dependent Choice, the direct and next-reaction methods with fixed initial state and unlimited event budgets have the recursively specified finite-state CTMC law; the generator is the reaction rate sum. (Finite-state Gillespie and next-reaction methods have the specified CTMC law)

Proof

technique · direct

1.1F1givenalgebra

For $x < 2$ , the birth rate $2 - x$ is positive and $x + 1 \in E$ ; at $x = 2$ its rate is zero. For $x > 0$ , the death rate $x$ is positive and $x - 1 \in E$ ; at $x = 0$ its rate is zero. Thus both channels are admissible, and $a_{+} (x) + a_{-} (x) = 2$ for all $x \in E$ .

2.1F2step 1.1givenalgebra

At state $1$ the two propensities are each $1$ . The direct method's waiting time is $E_{1} / 2$ , and its cumulative selection rule makes the first event a birth exactly when $0 \leq U_{1} < 1 / 2$ ; after each event the same calculation applies at the new state.

3.1F1F2step 1.1step 2.1algebra∎

The generator is $Q f (0) = 2 (f (1) - f (0))$ , $Q f (1) = f (2) - 2 f (1) + f (0)$ , and $Q f (2) = 2 (f (1) - f (2))$ , obtained from the active channels without evaluating $f$ outside $E$ . The rates are bounded by $Λ = 2$ , so the finite-state theorem identifies the direct method with the exact path law and gives $E N (T) \leq 2 T$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

31 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

David F. Anderson, Introduction to Stochastic Processes with Applications to Biology (standard reference, not scraped)