ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30

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.

Green kernel of a biased integer walk

Example

Assume AC (The Axiom of Choice). Let $p > q > 0$ with $p + q = 1$ , put $r = q / p$ , and on $E = Z$ with its full power-set sigma-algebra define the kernel

K (z, \cdot) = p δ_{z + 1} + q δ_{z - 1} .

For each $x \in Z$ , let $P_{x}$ be the canonical law with $X_{0} = x$ . Write $P (z, w) = K (z, {w})$ and $P^{(n)} (z, w) = K^{n} (z, {w})$ ; these are the transition matrix and its iterates from Transition matrices and n-step probabilities. Let $T_{y} = \inf {n \geq 0 : X_{n} = y}$ and $G (x, y) = \sum_{n \geq 0} P^{(n)} (x, y)$ , using Hitting, return, and visit times and Green kernel of a transient chain. Then for every $x, y \in Z$ ,

G (x, y) = {\begin{cases} \frac{1}{p - q}, & y \geq x, \\ \frac{r^{x - y}}{p - q}, & y < x . \end{cases}

Durrett’s birth–death scale calculation supplies the finite-difference route used below, and LPW’s finite-path formula gives the same finite-interval gambler’s-ruin value. Durrett’s stopped-martingale argument invokes almost-sure exit without proving it; the uniform path-block estimate below supplies that step. LPW §21.1 Example 21.2 likewise uses finite-interval exit in its escape calculation. Its displayed equality between the return-escape probability from $0$ and the no-hit probability from $1$ appears to omit the initial-step factor under the stated transition convention; no step here relies on that equality. The local computation gives the exact positive-return probability.

Verification

Given: $p > q > 0$ , $p + q = 1$ , and the kernel and Green series specified in the Example.

[A1] AC is the principle that every family of nonempty sets has a choice function. (The Axiom of Choice)

[F1] $Z$ is at most countable; an explicit enumeration is $0, 1, - 1, 2, - 2, \dots$ . “At most countable” means finite or in bijection with $N$ . (Finite, countably infinite, countable, uncountable)

[F2] A Dirac measure is a probability measure, and finite nonnegative weighted sums of measures are measures. The maps $z \mapsto z + 1$ and $z \mapsto z - 1$ are measurable on the full power set; since $p + q = 1$ , $K$ is a probability kernel. (A Dirac set function is a probability measure, Nonnegative scalar multiples and countable weighted sums of measures are measures, A measurable function between measurable spaces, Measure kernel and probability kernel)

[F3] Under AC, each probability kernel and initial probability law has a canonical path-space Markov-chain law. For initial law $δ_{x}$ this is $P_{x}$ , and $X_{0} = x$ almost surely. (Canonical Markov chain on path space, Initial distribution of a Markov chain)

[F4] The matrix entries and iterates are $P (z, w) = K (z, {w})$ and $P^{(n)} (z, w) = K^{n} (z, {w})$ . (Transition matrices and n-step probabilities)

[F15] Hitting and positive-return times use $T_{A} = \inf {n \geq 0 : X_{n} \in A}$ and $T_{y}^{+} = \inf {n \geq 1 : X_{n} = y}$ , with the stated empty-infimum convention. (Hitting, return, and visit times)

[F16] A measure is countably additive on every pairwise disjoint measurable sequence, with the union measured by the nonnegative extended sum. (Measures on sigma-algebras)

[F5] If a finite-state chain hits a boundary set almost surely from every state, then the expected bounded boundary payoff is the unique bounded solution of its boundary and harmonic equations. (Bounded Dirichlet problem for hitting probabilities)

[F6] For every bounded measurable future-path functional $H$ , its conditional expectation given $F_{n}$ is the canonical expectation from the current state $X_{n}$ . (Markov property for bounded future path functionals)

[F7] Under AC and deterministic start $z$ , $P_{z} (X_{m} = w) = P^{(m)} (z, w)$ for every $m \geq 0$ . (Finite-dimensional laws of a Markov chain)

[F8] The state $y$ is transient when $P_{y} (T_{y}^{+} < \infty) < 1$ . (Recurrent and transient states)

[F9] If $y$ is transient and $ρ_{y} = P_{y} (T_{y}^{+} < \infty)$ , then $\sum_{m \geq 0} P^{(m)} (y, y) = E_{y} N_{y} = 1 / (1 - ρ_{y})$ . (Equivalent criteria for recurrence and transience)

[F10] The Green kernel is the extended nonnegative series $G (z, w) = \sum_{m \geq 0} P^{(m)} (z, w)$ . (Green kernel of a transient chain)

[F11] Probabilities of increasing events converge to the probability of their union. (Continuity from below for measures)

[F12] If $0 \leq s < 1$ , then $s^{n} \to 0$ as $n \to \infty$ . (For $∣ r ∣ < 1$ the sequence $r^{k}$ is null, and for $∣ r ∣ > 1$ the sequence $∣ r ∣^{k}$ diverges to $+ \infty$ )

[F13] At a stopping time $τ$ , bounded measurable future-path functionals satisfy the strong Markov conditional identity on ${τ < \infty}$ , with the shifted value set to zero on ${τ = \infty}$ . (Discrete strong Markov property)

[F14] For a nonnegative double series, the summation order may be interchanged and both iterated sums equal the supremum of finite rectangular sums. (Tonelli's theorem for double series of nonnegative extended real numbers)

Proof technique: establish finite-interval absorption directly, solve its harmonic boundary problem, take monotone boundary limits, then factor the Green series at the first hit using bounded strong Markov tests.

1.1A1F1F2F3given

The enumeration in [F1] makes $E$ countable. For each fixed $z$ , [F2] shows that $K (z, \cdot)$ is a probability measure of total mass $p + q = 1$ ; the row evaluation $z \mapsto K (z, A) = p 1_{A} (z + 1) + q 1_{A} (z - 1)$ is measurable for every $A \subseteq E$ , so it is a probability kernel. With $δ_{x}$ as initial law, [A1] and [F3] give the canonical deterministic-start chain for every $x$ . Also $0 < r < 1$ and $0 < p < 1$ , since $0 < q < p$ and $p + q = 1$ .

2.1F2F3F6F12step 1.1given

Fix integers $a < b$ and put $D = {a, b}$ . On the finite set $E_{a, b} = {a, a + 1, \dots, b}$ , define an absorbed kernel $K_{a, b}$ by $K_{a, b} (a, \cdot) = δ_{a}$ , $K_{a, b} (b, \cdot) = δ_{b}$ , and $K_{a, b} (i, \cdot) = p δ_{i + 1} + q δ_{i - 1}$ for $a < i < b$ . If $b = a + 1$ , there are no interior states and the endpoint exit is immediate. The same finite-mixture argument as in step 1.1 makes this a probability kernel; take its canonical chain. Let $L = b - a$ . Define a measurable future-path event $H$ which is certain from an endpoint and, from each interior $i$ , requires the successive right moves $i \to i + 1 \to \dots \to b$ . Its probability from $i$ is $p^{b - i} \geq p^{L}$ . If $A_{k} = {T_{D} > k L}$ , then $X_{k L}$ is interior on $A_{k}$ . By [F6], conditional on $F_{k L}$ the event $H$ has probability at least $p^{L}$ on $A_{k}$ ; whenever $H$ occurs, $D$ is hit by time $(k + 1) L$ . Consequently $P_{x} (T_{D} > (k + 1) L) \leq (1 - p^{L}) P_{x} (T_{D} > k L)$ , so $P_{x} (T_{D} > k L) \leq (1 - p^{L})^{k} \to 0$ by [F12]. Thus every start in $E_{a, b}$ hits $D$ almost surely, including endpoint starts where $T_{D} = 0$ .

2.2F2F4given

The assumptions $p > q > 0$ and $p + q = 1$ imply $0 < r < 1$ , make every displayed denominator positive, and exclude zero right/left weights, deterministic motion, and the unbiased case $p = q$ . By [F4], $P (z, w) = K (z, {w})$ ; since the kernel in [F2] is supported on ${z - 1, z + 1}$ , all entries away from those neighbors are zero, as also follows from step 1.1.

3.1F15F5step 2.1given

Put $ϕ (i) = (1 - r^{i - a}) / (1 - r^{b - a})$ for $a \leq i \leq b$ . The denominator is positive, $0 \leq ϕ \leq 1$ , and $ϕ (a) = 0$ , $ϕ (b) = 1$ . For each interior $i$ , $ϕ (i + 1) - ϕ (i) = ((1 - r) r^{i - a}) / (1 - r^{b - a}) = r (ϕ (i) - ϕ (i - 1))$ . Since $p r = q$ , this is equivalent to $p ϕ (i + 1) + q ϕ (i - 1) = ϕ (i)$ . The almost-sure exit in step 2.1 and [F5], applied to boundary payoff $f (b) = 1$ , $f (a) = 0$ , identify $P_{i} (T_{b} < T_{a}) = ϕ (i) = (1 - r^{i - a}) / (1 - r^{b - a})$ for $a < i < b$ . The endpoints also have the displayed boundary values by the time-zero hitting convention in [F15].

4.1F15F11F12step 3.1given

If $x < y$ , choose integers $M$ with $- M < x$ and use step 3.1 on $[- M, y]$ ; then $P_{x} (T_{y} < T_{- M}) = (1 - r^{x + M}) / (1 - r^{y + M})$ . As $M$ increases these events increase, and their union is ${T_{y} < \infty}$ : every finite path segment ending at its first visit to $y$ has a finite minimum, so a sufficiently distant lower boundary is not reached first. By [F11] and [F12], the probabilities converge to $1$ . If $x > y$ , use $[y, M]$ with $M > x$ ; step 3.1 gives $P_{x} (T_{y} < T_{M}) = 1 - (1 - r^{x - y}) / (1 - r^{M - y}) = (r^{x - y} - r^{M - y}) / (1 - r^{M - y})$ . These events increase to ${T_{y} < \infty}$ because each finite path segment has a finite maximum, and [F11] and [F12] give the limit $r^{x - y}$ . When $x = y$ , $T_{y} = 0$ and the hitting probability is $1$ . Hence $P_{x} (T_{y} < \infty) = 1$ for $x \leq y$ and $r^{x - y}$ for $x > y$ .

5.1F15F6F7F8F9F10step 4.1given

From $y$ , the first step goes to $y + 1$ with probability $p$ or to $y - 1$ with probability $q$ , and there is no holding transition. The bounded future Markov identity [F6], applied to the event of ever hitting $y$ from the shifted path after time one, and the one-time marginal in [F7] together with step 4.1 give $ρ_{y} : = P_{y} (T_{y}^{+} < \infty) = p P_{y + 1} (T_{y} < \infty) + q P_{y - 1} (T_{y} < \infty) = p r + q = 2 q$ . Since $p > q$ and $p + q = 1$ , $2 q < 1$ and $y$ is transient by [F8]. The Green criterion [F9] and [F10] now give $G (y, y) = \sum_{m \geq 0} P^{(m)} (y, y) = 1 / (1 - 2 q) = 1 / (p - q) < \infty$ .

6.1F4F15F16F7F10F13F14step 4.1step 5.1given

Fix $x, y$ and put $a_{k} = P_{x} (T_{y} = k)$ and $b_{m} = P^{(m)} (y, y)$ . For every $n \geq 0$ , the disjoint events ${T_{y} = k, X_{n} = y}$ for $0 \leq k \leq n$ partition ${X_{n} = y}$ , and finite additivity follows from [F16]. The events ${T_{y} = k}$ partition ${T_{y} < \infty}$ , so countable additivity [F16] gives $\sum_{k} a_{k} = P_{x} (T_{y} < \infty)$ . For $m = n - k$ , apply [F13] at $T_{y}$ to the bounded path functional $H_{m} (ω) = 1_{{ω_{m} = y}}$ . On ${T_{y} = k}$ the stopped state is $y$ , and [F7] identifies the post-hit probability with $b_{m}$ ; thus $P_{x} (T_{y} = k, X_{k + m} = y) = a_{k} b_{m}$ . Summing the finite partition and then over $n$ , [F7] and [F14] give $G (x, y) = \sum_{n \geq 0} P_{x} (X_{n} = y) = \sum_{k, m \geq 0} a_{k} b_{m}$ . The rectangular partial sums factor as $(\sum_{k \leq K} a_{k}) (\sum_{m \leq M} b_{m})$ and converge to the product of their finite limits: $\sum_{k} a_{k} = P_{x} (T_{y} < \infty) \leq 1$ and $\sum_{m} b_{m} = G (y, y) = 1 / (p - q)$ by step 4.1. Therefore $G (x, y) = P_{x} (T_{y} < \infty) G (y, y)$ . Substitution of step 4.1 and the diagonal value from step 5.1 proves the stated two cases. This argument counts the time-zero visit when $x = y$ and uses the nonnegative Green series throughout, so no subtraction of extended values occurs.

7.1F15step 2.1step 3.1step 4.1step 6.1

The state space is the fixed infinite set $Z$ , so empty and one-state spaces cannot instantiate the Example. In the auxiliary interval $a < b$ ; if $b = a + 1$ , both states are absorbing endpoints and there is no interior equation, and step 3.1 uses its formula only when $a < i < b$ . Endpoint starts have $T_{D} = 0$ by steps 2.1–3.1, while $T_{y} = 0$ for $x = y$ and $T_{y}^{+}$ requires a strictly positive return [F15]. Step 6.1 includes the time-zero visit in the Green series.

8.1A1F3F5F6F7F9F13given∎

AC [A1] is used for canonical path laws [F3] and through the conditional Markov, finite-Dirichlet, finite-dimensional-law, recurrence-criterion and strong-Markov results [F5], [F6], [F7], [F9], [F13]; the explicit kernel, interval-path and difference-equation calculations are choice-free. The claim is a formula, not an iff statement.

Depends on

Used by

A transient chain can return with positive probability Counterexample

Dependency tree · two levels

85 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, fifth edition (standard reference, not scraped)
Levin, Peres and Wilmer, Markov Chains and Mixing Times, second edition (standard reference, not scraped)