ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-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.

Gambler's ruin probability for a biased walk

Statement

Assume AC. Let $N$ and $i$ be integers with $0 < i < N$ , set $S_{0} = i$ , and let the independent increments $ξ_{k} = S_{k} - S_{k - 1}$ be $+ 1$ with probability $p$ and $- 1$ with probability $q = 1 - p$ , where $0 < p < 1$ and $p \neq q$ . Use the natural filtration $F_{n} = σ (ξ_{1}, \dots, ξ_{n})$ , with $F_{0}$ trivial. For $τ = \inf {n : S_{n} \in {0, N}}$ , $P (S_{τ} = N) = \frac{1 - (q / p)^{i}}{1 - (q / p)^{N}} .$

Facts & Assumptions

Given: The hypotheses, objects, and conventions in the Statement.

[F1]

First hitting time of an adapted process is a stopping time makes $τ$ stopping.

[F2]

Conditioning a known variable and an independent variable verifies the exponential martingale.

[F3]

Optional stopping with a dominating integrable variable applies to its bounded stopped values.

[F4]

The Axiom of Choice is inherited from conditional expectation and optional stopping.

Proof

1.1F2

Put $r = q / p$ , so $r > 0$ and $r \neq 1$ . Independence of the next increment and $p r + q / r = q + p = 1$ give $E [r^{S_{n + 1}} ∣ F_{n}] = r^{S_{n}} (p r + q / r) = r^{S_{n}} .$ Thus $r^{S_{n}}$ is a martingale.

1.2F1

The same block argument as for symmetric ruin works because an all-up block of $N$ increments has positive probability $p^{N}$ : conditional on survival, it forces exit. Hence $P (τ > m N) \leq (1 - p^{N})^{m} \to 0$ . F1 gives stopping and this bound gives almost-sure finiteness.

2.1F3F4step 1.1step 1.2∎

Before exit, $S_{τ \land n} \in [0, N]$ , so $r^{S_{τ \land n}}$ is bounded by $\max (1, r^{N})$ . F3 gives $r^{i} = E r^{S_{τ}} = 1 \cdot P (S_{τ} = 0) + r^{N} P (S_{τ} = N) .$ Writing the first probability as one minus the second and solving yields $(r^{i} - 1) / (r^{N} - 1)$ , equal to the displayed formula. AC has exactly the role in F4.

Remarks

The diagram shows the local transition rule for the stopped walk $S_{n \land τ}$ at any interior state $1 \leq k \leq N - 1$ , and its two absorbing states separately. It starts at $S_{0} = i$ ; at $τ$ it first reaches either $0$ or $N$ . The upper-exit event in the Statement is $S_{τ} = N$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

14 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

Durrett, Probability: Theory and Examples, 5th ed., gambler's ruin and optional stopping in §4.8 (standard reference, not scraped)