ExampleConstruction: AI-adaptedVerification: 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.

Absorbing gambler's-ruin chain

Statement

Assume Choice. Fix $N \geq 1$ and $p \in [0, 1]$ , put $q = 1 - p$ , and take $S = {0, 1, \dots, N}$ . The gambler's-ruin transition matrix is $P (0, 0) = P (N, N) = 1, P (x, x + 1) = p, P (x, x - 1) = q (0 < x < N),$ with all other entries zero. It is an absorbed kernel on $D = {0, N}$ , and first entrance into $D$ is a hitting time. After a finite hit, the chain restarts at—and remains at—the boundary point hit.

Facts & Assumptions

Given: $N, p, q, S, D$ as displayed and a chain with this transition matrix.

[F1]

Absorption on $D$ replaces every row at $x \in D$ by $δ_{x}$ and leaves the rows on $D^{c}$ unchanged. (Killed and absorbed transition kernels)

[F2]

The absorbed construction is a probability kernel. (Killed and absorbed kernels are probability kernels)

[F3]

At a measurable hitting time, the conditional future path law is the canonical chain law started from the hit state. (The post-hitting chain restarts from the hit state)

Verification

1.1F1F2

For $0 < x < N$ , the only row masses are $p$ and $q$ , which are nonnegative and [F1, F2] sum to one. At $0$ and $N$ the rows are the corresponding Dirac masses. Thus these rows are exactly [F1] applied to any base kernel having the displayed interior transitions, and [F2] verifies the kernel. When $N = 1$ there are no interior rows; when $p = 0$ or $p = 1$ the interior motion is deterministic.

1.2given

Define [given] $τ_{D} = \inf {n \geq 0 : X_{n} \in {0, N}} .$ Then ${τ_{D} \leq n} = ⋃_{k = 0}^{n} {X_{k} \in D} \in F_{n}$ , so it is a hitting time. If $X_{0} \in D$ , then $τ_{D} = 0$ ; otherwise it may be infinite in the general eventwise formulation.

2.1F3step 1.1step 1.2∎

By [F3], on ${τ_{D} < \infty}$ the conditional future is the chain started [F3, step 1.1, step 1.2] from $X_{τ_{D}}$ . Step 1.1 gives $P (X_{τ_{D}}, X_{τ_{D}}) = 1$ , so every subsequent coordinate equals the same boundary state. Constants zero and one give respectively zero and the finite-hit event in the eventwise formula. Choice is used only through [F3].

Remarks

The first graph illustrates the transition rule for $N = 4$ ; only interior states have arrows to neighbors. The second shows the boundary case $N = 1$ . Arrow labels are transition probabilities, and an arrow labelled zero is omitted from the transition graph: thus $p = 0$ leaves only leftward interior moves, and $p = 1$ leaves only rightward interior moves. The loops of weight one show absorption. These graphs describe one-step transitions, without asserting that a boundary is hit on every path; the verification above is independent of the illustration.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

8 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

Levin, Peres, Wilmer, Markov Chains and Mixing Times, Section 2.1 (standard reference, not scraped)