ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generated

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.

Three-state birth-death chain with a certified Poisson tail

Example

On states $0, 1, 2$ , take birth rates $1$ from $0$ to $1$ and from $1$ to $2$ , and death rates $1$ from $1$ to $0$ and $2$ from $2$ to $1$ . Starting from $e_{0}$ , the generator and a uniformization rate are

$Q = (\begin{array}{ccc} - 1 & 1 & 0 \\ 1 & - 2 & 2 \\ 0 & 1 & - 2 \end{array}), ν = 2.$

At $t = 1 / 2$ , the Poisson parameter is $ν t = 1$ . Truncating after $K = 4$ gives

$u_{4} = \frac{1}{e} (\begin{array}{c} 703 / 384 \\ 277 / 384 \\ 5 / 32 \end{array}), ∥ p (1 / 2) - u_{4} ∥_{1} = 1 - \frac{65}{24 e} \leq \frac{1}{100 e} .$

The exact omitted-mass identity is mathematical, while the upper bound is the certified geometric tail used by the algorithm.

Facts & Assumptions

Given: The three-state rates in the Example, initial vector $e_{0} = (1, 0, 0)^{T}$ , time $t = 1 / 2$ , uniformization rate $ν = 2$ , and truncation index $K = 4$ .

[F1]

Finite column generator: $Q_{i j}$ is the rate from source column $j$ to destination row $i$ , and a finite generator has nonnegative off-diagonal entries and zero column sums.

[F2]

Finite master equation and uniformization formula: $p (t) = \sum_{k \geq 0} e^{- ν t} (ν t)^{k} P^{k} e_{0} / k!$ .

[F3]

A geometric upper bound for a Poisson right tail: when $μ < K + 2$ , $P (Pois (μ) > K) \leq G_{K} (μ)$ .

[F4]

The scalar Poisson count law and Normalization, moments, and generating function of the Poisson count law: the Poisson weight at $k$ for parameter $1$ is $e^{- 1} / k!$ , and the full set of weights sums to one.

Verification

technique · compute a finite matrix-power prefix and use the explicit geometric tail majorant

1.1givenF1algebra

The off-diagonal entries of $Q$ are nonnegative and its columns sum to zero; its exit rates are $1, 2, 2$ . Thus [F1] holds, $ν = 2$ dominates every exit rate, and $P = I + Q / 2 = (\begin{array}{ccc} 1 / 2 & 1 / 2 & 0 \\ 1 / 2 & 0 & 1 \\ 0 & 1 / 2 & 0 \end{array})$ .

2.1givenstep 1.1algebra

Starting from $e_{0}$ , successive multiplication by this $P$ gives $P e_{0} = (1 / 2, 1 / 2, 0)^{T}$ , $P^{2} e_{0} = (1 / 2, 1 / 4, 1 / 4)^{T}$ , $P^{3} e_{0} = (3 / 8, 1 / 2, 1 / 8)^{T}$ , and $P^{4} e_{0} = (7 / 16, 5 / 16, 1 / 4)^{T}$ . Each vector is obtained by multiplying the preceding vector by the displayed matrix.

3.1givenF2F4step 2.1algebra

By [F4], the first five Poisson weights at parameter $1$ are $e^{- 1} (1, 1, 1 / 2, 1 / 6, 1 / 24)$ . Weighting the five vectors from $e_{0}$ through $P^{4} e_{0}$ and adding coordinatewise gives $u_{4} = e^{- 1} (703 / 384, 277 / 384, 5 / 32)^{T}$ and total retained mass $65 / (24 e)$ . By normalization [F4], the exact omitted mass is $1 - 65 / (24 e) = P (Pois (1) > 4)$ . This subtraction is an exact identity, not a floating-point tail-estimation rule.

4.1givenF3step 3.1algebra∎

Applying [F3] with $μ = 1$ and $K = 4$ gives $P (Pois (1) > 4) \leq e^{- 1} / (5! (1 - 1 / 6)) = 1 / (100 e)$ . This upper bound is computed from a positive geometric majorant and does not use a floating-point subtraction.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

26 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

Bennett L. Fox and Peter W. Glynn, Computing Poisson Probabilities (standard reference, not scraped)